Mercurial > hg > Members > kono > Proof > category
diff comparison-em.agda @ 122:f8fbd5ecec97
no yellow on em-category
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 02 Aug 2013 08:21:32 +0900 |
parents | 324511654f23 |
children | 44c58c27d12d |
line wrap: on
line diff
--- a/comparison-em.agda Thu Aug 01 18:14:42 2013 +0900 +++ b/comparison-em.agda Fri Aug 02 08:21:32 2013 +0900 @@ -24,9 +24,9 @@ { 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 ) } + { μ^K : NTrans A A (( U^K ○ F^K ) ○ ( U^K ○ F^K )) ( U^K ○ F^K ) } ( Adj^K : Adjunction A B U^K F^K η^K ε^K ) - ( RK : MResolution A B T U^K F^K {η^K} {ε^K} {μ^K'} AdjK ) + ( RK : MResolution A B T U^K F^K {η^K} {ε^K} {μ^K} Adj^K ) where open import adj-monad @@ -36,17 +36,13 @@ M : Monad A (U^K ○ F^K ) η^K μ^K M = Adj2Monad A B {U^K} {F^K} {η^K} {ε^K} Adj^K -K : Eilenberg-MooreCategory A (U^K ○ F^K ) η^K μ^K M -K = record {} - -open import nat {c₁} {c₂} {ℓ} {A} { U^K ○ F^K } { η^K } { μ^K } { M } { K } +open import em-category {c₁} {c₂} {ℓ} {A} { U^K ○ F^K } { η^K } { μ^K } { M } open Functor open NTrans -open Eilenberg-MooreCategory -open EMHom open Adjunction open MResolution +open Eilenberg-Moore-Hom emkobj : Obj B -> EMObj emkobj b = record { @@ -58,7 +54,7 @@ eval1 = ? emkmap : {a b : Obj B} (f : Hom B a b) -> EMHom (emkobj a) (emkobj b) -emkmap {a} {b} f = record { EMap = FMap U f ; homomorphism = homomorphism1 +emkmap {a} {b} f = record { EMap = FMap U^K f ; homomorphism = homomorphism1 } where homomorphism1 : ? homomorphism1 = ? @@ -73,24 +69,24 @@ ; distr = distr1 } } where - identity : {a : Obj A} → B [ emkmap (K-id {a}) ≈ id1 B (FObj F^K a) ] + identity : {a : Obj A} → B [ emkmap (EM-id {a}) ≈ id1 B (FObj F^K a) ] identity {a} = let open ≈-Reasoning (B) in begin - emkmap (K-id {a}) + emkmap (EM-id {a}) ≈⟨ ? ⟩ id1 B (FObj F^K a) ∎ - ≈-cong : {a b : Obj A} -> {f g : EMHom a b} → A [ KMap f ≈ KMap g ] → B [ emkmap f ≈ emkmap g ] + ≈-cong : {a b : Obj A} -> {f g : EMHom a b} → A [ EMap f ≈ EMap g ] → B [ emkmap f ≈ emkmap g ] ≈-cong {a} {b} {f} {g} f≈g = let open ≈-Reasoning (B) in begin emkmap f ≈⟨ ? ⟩ emkmap g ∎ - distr1 : {a b c : Obj A} {f : EMHom a b} {g : EMHom b c} → B [ emkmap (g * f) ≈ (B [ emkmap g o emkmap f ] )] + distr1 : {a b c : Obj A} {f : EMHom a b} {g : EMHom b c} → B [ emkmap (g ∙ f) ≈ (B [ emkmap g o emkmap f ] )] distr1 {a} {b} {c} {f} {g} = let open ≈-Reasoning (B) in begin - emkmap (g * f) + emkmap (g ∙ f) ≈⟨ ? ⟩ emkmap g o emkmap f ∎