# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1499208787 -32400
# Node ID 1503af5d744012e379bc8896f1b6234f849708f0
# Parent  449025d1327f089049ebee8845874d08f26f234f
id of Functor F

diff -r 449025d1327f -r 1503af5d7440 freyd2.agda
--- a/freyd2.agda	Tue Jul 04 11:03:37 2017 +0900
+++ b/freyd2.agda	Wed Jul 05 07:53:07 2017 +0900
@@ -399,8 +399,29 @@
            ; ≈-cong = cong1
         } 
       }  where
+        id1comm : {a : Obj B} → B [ B [ FMap U (arrow (initial (In a) (ηf a a (id1 B a)))) o hom (i a) ]
+                ≈ B [ hom (i a) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a)))) ] ]
+        id1comm {a} = let open ≈-Reasoning B in begin
+                FMap U (arrow (initial (In a) (ηf a a (id1 B a)))) o hom (i a) 
+             ≈⟨ comm (initial (In a) (ηf a a (id1 B a))) ⟩
+                hom (ηf a a (id1 B a)) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a))))
+             ≈⟨ idR ⟩
+                hom (ηf a a (id1 B a)) 
+             ≈⟨⟩
+                hom (i a) o id1 B a
+             ≈⟨ idR ⟩
+                hom (i a) 
+             ≈↑⟨ idR ⟩
+                hom (i a) o FMap (K B A a) (arrow (initial (In a) (ηf a a (id1 B a))))
+             ∎  
         identity1 : {a : Obj B} → A [ arrow (initial (In a) (ηf a a (id1 B a))) ≈ id1 A (obj (i a)) ]
-        identity1 = {!!}
+        identity1 {a} = let open ≈-Reasoning A in begin
+                arrow (initial (In a) (ηf a a (id1 B a)))
+             ≈⟨ uniqueness (In a) (record { arrow = arrow (initial (In a) (ηf a a (id1 B a))); comm = id1comm }) ⟩
+                arrow (initial (In a) (i a))
+             ≈↑⟨ uniqueness (In a) (id1 ( K B A a ↓ U) (i a) ) ⟩
+                id1 A (obj (i a)) 
+             ∎  
         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)) ] ]
@@ -422,9 +443,7 @@
 
    nat-η : NTrans B B identityFunctor (U ○ F)
    nat-η = record { TMap = λ y →  tmap-η y ; isNTrans = record { commute = comm1 } } where
-       comm1 : {a b : Obj B} {f : Hom B a b}
-          → B [ B [ FMap (U ○ F) f o tmap-η a ]
-                ≈ B [ tmap-η b o f ] ]
+       comm1 : {a b : Obj B} {f : Hom B a b} → B [ B [ FMap (U ○ F) f o tmap-η a ] ≈ B [ tmap-η b o f ] ]
        comm1 {a} {b} {f} = let open ≈-Reasoning B in begin
                FMap (U ○ F) f o tmap-η a 
              ≈⟨⟩