Mercurial > hg > Members > kono > Proof > category
diff comparison-functor.agda @ 688:a5f2ca67e7c5
fix monad/adjunction definition
couniversal to limit does not work
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 11 Nov 2017 21:34:58 +0900 |
| parents | d3cd28a71b3f |
| children |
line wrap: on
line diff
--- a/comparison-functor.agda Wed Nov 08 19:57:43 2017 +0900 +++ b/comparison-functor.agda Sat Nov 11 21:34:58 2017 +0900 @@ -19,14 +19,13 @@ { T : Functor A A } { η : NTrans A A identityFunctor T } { μ : NTrans A A (T ○ T) T } - { M' : Monad A T η μ } + { M' : IsMonad A T η μ } {c₁' c₂' ℓ' : Level} ( B : Category c₁' c₂' ℓ' ) { U_K : Functor B A } { F_K : Functor A B } { η_K : NTrans A A identityFunctor ( U_K ○ F_K ) } { ε_K : NTrans B B ( F_K ○ U_K ) identityFunctor } { μ_K' : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) } - ( AdjK : Adjunction A B U_K F_K η_K ε_K ) - ( RK : MResolution A B T U_K F_K {η_K} {ε_K} {μ_K'} AdjK ) + ( AdjK : IsAdjunction A B U_K F_K η_K ε_K ) where open import adj-monad @@ -36,8 +35,8 @@ μ_K : NTrans A A (( U_K ○ F_K ) ○ ( U_K ○ F_K )) ( U_K ○ F_K ) μ_K = UεF A B U_K F_K ε_K -M : Monad A (U_K ○ F_K ) η_K μ_K -M = Adj2Monad A B {U_K} {F_K} {η_K} {ε_K} AdjK +M : IsMonad A (U_K ○ F_K ) η_K μ_K +M = Monad.isMonad ( Adj2Monad A B ( record { U = U_K; F = F_K ; η = η_K ; ε = ε_K ; isAdjunction = AdjK } ) ) open import kleisli {c₁} {c₂} {ℓ} {A} { U_K ○ F_K } { η_K } { μ_K } { M } @@ -68,7 +67,7 @@ TMap ε_K (FObj F_K a) o FMap F_K (KMap (K-id {a})) ≈⟨⟩ TMap ε_K (FObj F_K a) o FMap F_K (TMap η_K a) - ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩ + ≈⟨ IsAdjunction.adjoint2 AdjK ⟩ id1 B (FObj F_K a) ∎ ≈-cong : {a b : Obj A} → {f g : KHom a b} → A [ KMap f ≈ KMap g ] → B [ kfmap f ≈ kfmap g ] @@ -144,7 +143,7 @@ TMap ε_K (FObj F_K b) o (FMap F_K (TMap η_K b) o FMap F_K f ) ≈⟨ assoc ⟩ (TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b)) o FMap F_K f - ≈⟨ car ( IsAdjunction.adjoint2 (isAdjunction AdjK)) ⟩ + ≈⟨ car ( IsAdjunction.adjoint2 AdjK) ⟩ id1 B (FObj F_K b) o FMap F_K f ≈⟨ idL ⟩ FMap F_K f @@ -170,7 +169,7 @@ FMap K_T (record { KMap = (TMap η_K b) }) ≈⟨⟩ TMap ε_K (FObj F_K b) o FMap F_K (TMap η_K b) - ≈⟨ IsAdjunction.adjoint2 (isAdjunction AdjK) ⟩ + ≈⟨ IsAdjunction.adjoint2 AdjK ⟩ id1 B (FObj F_K b) ∎ @@ -185,7 +184,7 @@ TMap ε_K (FObj F_K (FObj T_K c)) o ( FMap F_K (TMap η_K (FObj T_K c)) o FMap F_K g ) ≈⟨ assoc ⟩ (TMap ε_K (FObj F_K (FObj T_K c)) o ( FMap F_K (TMap η_K (FObj T_K c)))) o FMap F_K g - ≈⟨ car ( IsAdjunction.adjoint2 (isAdjunction AdjK)) ⟩ + ≈⟨ car ( IsAdjunction.adjoint2 AdjK) ⟩ id1 B (FObj F_K (FObj T_K c)) o FMap F_K g ≈⟨ idL ⟩ FMap F_K g