Mercurial > hg > Members > kono > Proof > category

changeset 656:18431b63893b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 06 Jul 2017 09:54:56 +0900
parents 26a28b1cee6f
children 0d029674eb59
files freyd2.agda
diffstat 1 files changed, 37 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Wed Jul 05 10:35:17 2017 +0900
+++ b/freyd2.agda	Thu Jul 06 09:54:56 2017 +0900
@@ -457,12 +457,38 @@
         distr1 : {a b c : Obj B} {f : Hom B a b} {g : Hom B b c} →
                 A [ arrow (initial (In a) (ηf a c (B [ g o f ]))) ≈
                 A [ arrow (initial (In b) (ηf b c g)) o arrow (initial (In a) (ηf a b f)) ] ]
-        distr1 = {!!}
+        distr1 {a} {b} {c} {f} {g} = unique  (
+             let open ≈-Reasoning B in begin
+               FMap U (A [ arrow (initial (In b) (ηf b c g)) o arrow (initial (In a) (ηf a b f)) ] ) o tmap-η a 
+             ≈⟨ car (IsFunctor.distr (isFunctor U )) ⟩
+               ( FMap U (arrow (initial (In b) (ηf b c g))) o FMap U (arrow (initial (In a) (ηf a b f))) )
+                  o tmap-η a 
+             ≈↑⟨ assoc ⟩
+               FMap U (arrow (initial (In b) (ηf b c g))) o
+                  (FMap U (arrow (initial (In a) (ηf a b f))) o tmap-η a )
+             ≈⟨ cdr (univ ( tmap-η b o f )) ⟩
+               FMap U (arrow (initial (In b) (ηf b c g))) o ( tmap-η b o f )
+             ≈⟨ assoc ⟩
+               (FMap U (arrow (initial (In b) (ηf b c g))) o  tmap-η b ) o f 
+             ≈⟨ car ( univ (tmap-η c o  g )) ⟩
+               (tmap-η c o  g ) o f 
+             ≈↑⟨ assoc ⟩
+               tmap-η c o ( g o f )
+             ∎  
+            )
         cong1  : {a : Obj B} {b : Obj B} {f g : Hom B a b} →
           B [ f ≈ g ] → A [ arrow (initial (In a) (ηf a b f)) ≈ arrow (initial (In a) (ηf a b g)) ]
-        cong1  = {!!}
+        cong1 {a} {b} {f} {g} f≈g  = unique (
+             let open ≈-Reasoning B in begin
+               FMap U (arrow (initial (In a) (ηf a b g))) o tmap-η a 
+             ≈⟨ univ ( tmap-η b o g ) ⟩
+               tmap-η b o g 
+             ≈↑⟨ cdr f≈g ⟩
+               tmap-η b o f 
+             ∎  
+           )
 
-   nat-ε : NTrans A A (F  ○ U) identityFunctor
+   nat-ε : NTrans A A (F ○ U) identityFunctor
    nat-ε  = record {
          TMap = λ x → arrow ( solution (id1 B (FObj U x)))
          ; isNTrans = record { commute = comm1 } } where
@@ -470,7 +496,14 @@
                 A [ A [ FMap (identityFunctor {_} {_} {_} {A}) f o
                     arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) ]
               ≈ A [ arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f ] ]
-        comm1 = {!!}
+        comm1 {a} {b} {f} = let open ≈-Reasoning A in begin
+               FMap (identityFunctor {_} {_} {_} {A}) f o
+                    arrow (initial (In (FObj U a)) (record { obj = a ; hom = id1 B (FObj U a) })) 
+             ≈↑⟨ unique {!!} ⟩
+               arrow (initial (In (FObj U a)) (record { obj = b ; hom = B [ FMap U f o id1 B (FObj U a) ] })) 
+             ≈⟨ unique {!!} ⟩
+               arrow (initial (In (FObj U b)) (record { obj = b ; hom = id1 B (FObj U b) })) o FMap (F ○ U) f 
+             ∎  
 
    nat-η : NTrans B B identityFunctor (U ○ F)
    nat-η = record { TMap = λ y →  tmap-η y ; isNTrans = record { commute = comm1 } } where