Mercurial > hg > Members > kono > Proof > category

changeset 467:ba042c2d3ff5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 05 Mar 2017 11:14:32 +0900
parents 44bd77c80555
children c375d8f93a2c
files em-category.agda kleisli.agda limit-to.agda
diffstat 3 files changed, 32 insertions(+), 38 deletions(-) [+]
line wrap: on
line diff
--- 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
--- 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) }
--- 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 ) ⟩