# HG changeset patch # User Shinji KONO # Date 1488680072 -32400 # Node ID ba042c2d3ff5ecd6f463327b98409c1f252a457f # Parent 44bd77c805554c4083316a109feddf40f257b782 clean up diff -r 44bd77c80555 -r ba042c2d3ff5 em-category.agda --- a/em-category.agda Sat Mar 04 16:57:58 2017 +0900 +++ b/em-category.agda Sun Mar 05 11:14:32 2017 +0900 @@ -230,10 +230,10 @@ Lemma-EM8 f = Category.Cat.refl (Lemma-EM7 f) η^T : NTrans A A identityFunctor ( U^T ○ F^T ) -η^T = record { TMap = λ x → TMap η x ; isNTrans = isNTrans1 } where - commute1 : {a b : Obj A} {f : Hom A a b} +η^T = record { TMap = λ x → TMap η x ; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }} where + commute : {a b : Obj A} {f : Hom A a b} → A [ A [ ( FMap ( U^T ○ F^T ) f ) o ( TMap η a ) ] ≈ A [ (TMap η b ) o f ] ] - commute1 {a} {b} {f} = let open ≈-Reasoning (A) in + commute {a} {b} {f} = let open ≈-Reasoning (A) in begin ( FMap ( U^T ○ F^T ) f ) o ( TMap η a ) ≈⟨ sym (resp refl-hom (Lemma-EM7 f)) ⟩ @@ -241,8 +241,6 @@ ≈⟨ nat η ⟩ TMap η b o f ∎ - isNTrans1 : IsNTrans A A identityFunctor ( U^T ○ F^T ) (λ a → TMap η a) - isNTrans1 = record { commute = commute1 } Lemma-EM9 : (a : EMObj) → A [ A [ (φ a) o FMap T (φ a) ] ≈ A [ (φ a) o (φ (FObj ( F^T ○ U^T ) a)) ] ] Lemma-EM9 a = let open ≈-Reasoning (A) in @@ -258,10 +256,10 @@ emap-ε a = record { EMap = φ a ; homomorphism = Lemma-EM9 a } ε^T : NTrans Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor -ε^T = record { TMap = λ a → emap-ε a; isNTrans = isNTrans1 } where - commute1 : {a b : EMObj } {f : EMHom a b} +ε^T = record { TMap = λ a → emap-ε a; isNTrans = record { commute = λ {a} {b} {f} → commute {a} {b} {f} }} where + commute : {a b : EMObj } {f : EMHom a b} → (f ∙ ( emap-ε a ) ) ≗ (( emap-ε b ) ∙( FMap (F^T ○ U^T) f ) ) - commute1 {a} {b} {f} = let open ≈-Reasoning (A) in + commute {a} {b} {f} = let open ≈-Reasoning (A) in sym ( begin EMap (( emap-ε b ) ∙ ( FMap (F^T ○ U^T) f )) ≈⟨⟩ @@ -271,9 +269,7 @@ ≈⟨⟩ EMap (f ∙ ( emap-ε a )) ∎ ) - isNTrans1 : IsNTrans Eilenberg-MooreCategory Eilenberg-MooreCategory ( F^T ○ U^T ) identityFunctor (λ a → emap-ε a ) - isNTrans1 = record { commute = λ {a} {b} {f} → commute1 {a} {b} {f} } - + -- -- μ = U^T ε U^F -- @@ -282,10 +278,10 @@ emap-μ a = FMap U^T ( TMap ε^T ( FObj F^T a )) μ^T : NTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T ) -μ^T = record { TMap = emap-μ ; isNTrans = isNTrans1 } where - commute1 : {a b : Obj A} {f : Hom A a b} +μ^T = record { TMap = emap-μ ; isNTrans = record { commute = commute }} where + commute : {a b : Obj A} {f : Hom A a b} → A [ A [ (FMap (U^T ○ F^T) f) o ( emap-μ a) ] ≈ A [ ( emap-μ b ) o FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f) ] ] - commute1 {a} {b} {f} = let open ≈-Reasoning (A) in + commute {a} {b} {f} = let open ≈-Reasoning (A) in sym ( begin ( emap-μ b ) o FMap (U^T ○ F^T) ( FMap (U^T ○ F^T) f) ≈⟨⟩ @@ -297,8 +293,6 @@ ≈⟨⟩ (FMap (U^T ○ F^T) f) o ( emap-μ a) ∎ ) - isNTrans1 : IsNTrans A A (( U^T ○ F^T ) ○ ( U^T ○ F^T )) ( U^T ○ F^T ) emap-μ - isNTrans1 = record { commute = commute1 } Lemma-EM10 : {x : Obj A } → A [ TMap μ^T x ≈ FMap U^T ( TMap ε^T ( FObj F^T x ) ) ] Lemma-EM10 {x} = let open ≈-Reasoning (A) in diff -r 44bd77c80555 -r ba042c2d3ff5 kleisli.agda --- a/kleisli.agda Sat Mar 04 16:57:58 2017 +0900 +++ b/kleisli.agda Sun Mar 05 11:14:32 2017 +0900 @@ -209,11 +209,13 @@ record KleisliHom { c₁ c₂ ℓ : Level} { A : Category c₁ c₂ ℓ } { T : Functor A A } (a : Obj A) (b : Obj A) - : Set c₂ where - field - KMap : Hom A a ( FObj T b ) + : Set c₂ where + field + KMap : Hom A a ( FObj T b ) + +open KleisliHom -open KleisliHom +-- we need this to make agda check stop KHom = λ (a b : Obj A) → KleisliHom {c₁} {c₂} {ℓ} {A} {T} a b K-id : {a : Obj A} → KHom a a @@ -420,10 +422,10 @@ -- nat-η : NTrans A A identityFunctor ( U_T ○ F_T ) -nat-η = record { TMap = λ x → TMap η x ; isNTrans = isNTrans1 } where - commute1 : {a b : Obj A} {f : Hom A a b} +nat-η = record { TMap = λ x → TMap η x ; isNTrans = record { commute = commute } } where + commute : {a b : Obj A} {f : Hom A a b} → A [ A [ ( FMap ( U_T ○ F_T ) f ) o ( TMap η a ) ] ≈ A [ (TMap η b ) o f ] ] - commute1 {a} {b} {f} = let open ≈-Reasoning (A) in + commute {a} {b} {f} = let open ≈-Reasoning (A) in begin ( FMap ( U_T ○ F_T ) f ) o ( TMap η a ) ≈⟨ sym (resp refl-hom (Lemma11-1 f)) ⟩ @@ -431,8 +433,6 @@ ≈⟨ nat η ⟩ TMap η b o f ∎ - isNTrans1 : IsNTrans A A identityFunctor ( U_T ○ F_T ) (λ a → TMap η a) - isNTrans1 = record { commute = commute1 } tmap-ε : (a : Obj A) → KHom (FObj T a) a tmap-ε a = record { KMap = id1 A (FObj T a) } diff -r 44bd77c80555 -r ba042c2d3ff5 limit-to.agda --- a/limit-to.agda Sat Mar 04 16:57:58 2017 +0900 +++ b/limit-to.agda Sun Mar 05 11:14:32 2017 +0900 @@ -66,37 +66,37 @@ A [ fmap (T [ g o f ]) ≈ A [ fmap g o fmap f ] ] distr1 {t0} {t0} {t0} {id-t0 } { id-t0 } = let open ≈-Reasoning A in sym-hom idL distr1 {t1} {t1} {t1} { id-t1 } { id-t1 } = let open ≈-Reasoning A in begin - id1 A b + id b ≈↑⟨ idL ⟩ - id1 A b o id1 A b + id b o id b ∎ distr1 {t0} {t0} {t1} { id-t0 } { arrow-f } = let open ≈-Reasoning A in begin fmap (T [ arrow-f o id-t0 ] ) ≈⟨⟩ fmap arrow-f ≈↑⟨ idR ⟩ - fmap arrow-f o id1 A a + fmap arrow-f o id a ∎ distr1 {t0} {t0} {t1} { id-t0 } { arrow-g } = let open ≈-Reasoning A in begin fmap (T [ arrow-g o id-t0 ] ) ≈⟨⟩ fmap arrow-g ≈↑⟨ idR ⟩ - fmap arrow-g o id1 A a + fmap arrow-g o id a ∎ distr1 {t0} {t1} {t1} { arrow-f } { id-t1 } = let open ≈-Reasoning A in begin fmap (T [ id-t1 o arrow-f ] ) ≈⟨⟩ fmap arrow-f ≈↑⟨ idL ⟩ - id1 A b o fmap arrow-f + id b o fmap arrow-f ∎ distr1 {t0} {t1} {t1} { arrow-g } { id-t1 } = let open ≈-Reasoning A in begin fmap (T [ id-t1 o arrow-g ] ) ≈⟨⟩ fmap arrow-g ≈↑⟨ idL ⟩ - id1 A b o fmap arrow-g + id b o fmap arrow-g ∎ --- Nat for Limit @@ -127,28 +127,28 @@ commute1 {t0} {t1} {arrow-f} d h fh=gh = let open ≈-Reasoning A in begin f o h ≈↑⟨ idR ⟩ - (f o h ) o id1 A d + (f o h ) o id d ∎ commute1 {t0} {t1} {arrow-g} d h fh=gh = let open ≈-Reasoning A in begin g o h ≈↑⟨ fh=gh ⟩ f o h ≈↑⟨ idR ⟩ - (f o h ) o id1 A d + (f o h ) o id d ∎ commute1 {t0} {t0} {id-t0} d h fh=gh = let open ≈-Reasoning A in begin - id1 A a o h + id a o h ≈⟨ idL ⟩ h ≈↑⟨ idR ⟩ - h o id1 A d + h o id d ∎ commute1 {t1} {t1} {id-t1} d h fh=gh = let open ≈-Reasoning A in begin - id1 A b o ( f o h ) + id b o ( f o h ) ≈⟨ idL ⟩ f o h ≈↑⟨ idR ⟩ - ( f o h ) o id1 A d + ( f o h ) o id d ∎ @@ -206,7 +206,7 @@ uniq-nat {t1} d h k' fh=gh ek'=h = let open ≈-Reasoning A in begin TMap (limit-u comp Γ) t1 o k' ≈↑⟨ car (idR) ⟩ - ( TMap (limit-u comp Γ) t1 o id1 A c ) o k' + ( TMap (limit-u comp Γ) t1 o id c ) o k' ≈⟨⟩ ( TMap (limit-u comp Γ) t1 o FMap (K A I c) arrow-f ) o k' ≈↑⟨ car ( nat1 (limit-u comp Γ) arrow-f ) ⟩