# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1472466100 -32400
# Node ID 9be298a02c357788291e3144e155fcd0b1064d31
# Parent  ef37decef1ca60abd51f4180e163ea98ed50f2be
add rest of equation

diff -r ef37decef1ca -r 9be298a02c35 freyd.agda
--- a/freyd.agda	Mon Aug 29 17:02:03 2016 +0900
+++ b/freyd.agda	Mon Aug 29 19:21:40 2016 +0900
@@ -53,14 +53,31 @@
       initial = initialArrow ; 
       uniqueness  = λ a f → lemma1 a f
     } where
+      f : {a : Obj A} -> Hom A  a0 (FObj F  (preinitialObj PI {a} ) ) 
+      f {a} = limit (lim F {FObj F (preinitialObj PI {a} )} {u (FObj F (preinitialObj PI))} ) a0 (u a0 )  
       initialArrow :  ∀( a : Obj A )  →  Hom A a0 a
-      initialArrow a  = A [ preinitialArrow PI {a}  o limit (lim F {FObj F (preinitialObj PI)} {u (FObj F (preinitialObj PI))} ) a0 (u a0 )  ] 
-      equ-fi : { a c : Obj A} -> { p : Hom A c a0 } -> {f : Hom A a0 a} -> Equalizer A p ( A [ preinitialArrow PI {a} o  limit (lim F) a0 (u a0)  ] ) f
-      equ-fi  {a} {c} {p} {f} = equ ( A [ preinitialArrow PI {a} o  limit (lim F) a0 (u a0) ] ) f
+      initialArrow a  = A [ preinitialArrow PI {a}  o f ]
+      limit-u : Limit A A F a0 (u a0)
+      limit-u = lim F {a0} {u a0}
+      equ-fi : { a c : Obj A} -> { p : Hom A c a0 } -> {f' : Hom A a0 a} -> 
+          Equalizer A p ( A [ preinitialArrow PI {a} o  f ] ) f'
+      equ-fi  {a} {c} {p} {f'} = equ ( A [ preinitialArrow PI {a} o  limit (lim F) a0 (u a0) ] ) f'
+      e=id : (e : Hom A a0 a0) -> ( {c : Obj A} -> A [ A [ TMap (u a0)  c o  e ]  ≈  TMap (u a0) c ] ) -> A [ e  ≈ id1 A a0 ]
+      e=id  e uce=uc =  let open ≈-Reasoning (A) in
+            begin
+              e
+            ≈↑⟨ limit-uniqueness limit-u {a0} {u a0} {e} ( \{i} -> uce=uc ) ⟩
+              limit limit-u a0 (u a0)
+            ≈⟨ limit-uniqueness limit-u {a0} {u a0} {id1 A a0} ( \{i} -> idR ) ⟩
+              id1 A a0
+            ∎
       open Equalizer
-      kfuc=1 : {k1 c : Obj A} -> A [ A [ equalizer (equ-fi {a0} {k1} {{!!}} {{!!}} )  o  
+      kfuc=uc : {c k1 : Obj A} -> A [ A [ TMap (u a0)  c  o  A [ equalizer (equ-fi {a0} {k1} {{!!}} {{!!}} )  o  
+                    A [ preinitialArrow PI {k1} o TMap (u a0) (preinitialObj PI) ] ] ]  ≈ TMap (u a0) c ]
+      kfuc=uc {k1} {c} = {!!}
+      kfuc=1 : {k1 : Obj A} -> A [ A [ equalizer (equ-fi {a0} {k1} {{!!}} {{!!}} )  o  
                     A [ preinitialArrow PI {k1} o TMap (u a0) (preinitialObj PI) ] ] ≈ id1 A a0 ]
-      kfuc=1 {k1} {c} = {!!}
+      kfuc=1 {k1}  = {!!}
       -- if equalizer has right inverse, f = g
       lemma2 :  (a b c : Obj A) ( f g : Hom A a b ) (e : Hom A c a ) (e' : Hom A a c ) ( equ : Equalizer A e f g ) (inv-e : A [ A [ e o e' ] ≈ id1 A a ] )
            -> A [ f ≈ g ]
@@ -90,7 +107,7 @@
                  initialArrow a
              ≈⟨⟩
                  preinitialArrow PI {a} o  limit (lim F) a0 (u a0) 
-             ≈⟨ lemma2 a0 a {!!} (A [ preinitialArrow PI {a} o  limit (lim F) a0 (u a0) ]) f {!!} {!!} {!!} (kfuc=1 {{!!}} {{!!}} ) ⟩
+             ≈⟨ lemma2 a0 a {!!} (A [ preinitialArrow PI {a} o  limit (lim F) a0 (u a0) ]) f {!!} {!!} {!!} (kfuc=1 {{!!}} ) ⟩
                  f
              ∎  )