# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1472483950 -32400
# Node ID ce9edc8088e8934053bfab26d9ee22a3d459f8ef
# Parent  9be298a02c357788291e3144e155fcd0b1064d31
clean up

diff -r 9be298a02c35 -r ce9edc8088e8 freyd.agda
--- a/freyd.agda	Mon Aug 29 19:21:40 2016 +0900
+++ b/freyd.agda	Tue Aug 30 00:19:10 2016 +0900
@@ -62,8 +62,8 @@
       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
+      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 ) ⟩
@@ -72,16 +72,18 @@
               id1 A a0
             ∎
       open Equalizer
-      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 : {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}  = {!!}
+      kfuc=1 {k1}  = e=id kfuc=uc
       -- 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 ] )
+      lemma2 :  (a b : Obj A) {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 ]
-      lemma2 a b c f g e e' equ inv-e = let open ≈-Reasoning (A) in
+      lemma2 a b {c} f g {e} {e'} equ inv-e = let open ≈-Reasoning (A) in
             let open Equalizer in
             begin
                 f
@@ -101,13 +103,13 @@
                 g
             ∎
       lemma1 : (a : Obj A) (f : Hom A a0 a) → A [ f ≈ initialArrow a ]
-      lemma1 a f = let open ≈-Reasoning (A) in 
+      lemma1 a f' = let open ≈-Reasoning (A) in 
              sym (
              begin
                  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 {{!!}} ) ⟩
-                 f
+             ≈⟨ lemma2 a0 a (A [ preinitialArrow PI {a} o  limit (lim F) a0 (u a0) ]) f' equ-fi (kfuc=1 {a} ) ⟩
+                 f'
              ∎  )