# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1472488856 -32400
# Node ID bc0682b86b916b98ae0488ebe6814e46c722f05c
# Parent  ce9edc8088e8934053bfab26d9ee22a3d459f8ef
equ

diff -r ce9edc8088e8 -r bc0682b86b91 freyd.agda
--- a/freyd.agda	Tue Aug 30 00:19:10 2016 +0900
+++ b/freyd.agda	Tue Aug 30 01:40:56 2016 +0900
@@ -47,9 +47,11 @@
       ( equ : {a b c : Obj A} → (f g : Hom A a b)  → {e : Hom A c a }  → Equalizer A e f g )
       (SFS : SmallFullSubcategory A F FMap← ) → 
       (PI : PreInitial A F ) → { a0 : Obj A } → 
-      { u : (a : Obj A) → NTrans A A (K A A a) F }  -- Does it exist?
+      { ee : {a b : Obj A} → {f g : Hom A a b}  → Obj A }
+      { ep :  {a b : Obj A} → {f g : Hom A a b}  → Hom A (ee {a} {b} {f} {g} ) a }
+      { u : (a : Obj A) → NTrans A A (K A A a) F }  
           → HasInitialObject A a0
-initialFromPreInitialFullSubcategory A F  FMap← lim equ SFS PI {a0} {u} = record {
+initialFromPreInitialFullSubcategory A F  FMap← lim equ SFS PI {a0} {ee} {ep} {u} = record {
       initial = initialArrow ; 
       uniqueness  = λ a f → lemma1 a f
     } where
@@ -72,13 +74,12 @@
               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) ] ] ]  
+      kfuc=uc : {c k1 : Obj A} ->  {p : Hom A k1 a0} -> A [ A [ TMap (u a0)  c  o  
+              A [ p 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}  = e=id kfuc=uc
+      kfuc=1 : {k1 : Obj A} ->  {p : Hom A k1 a0} -> A [ A [ p o A [ preinitialArrow PI {k1} o TMap (u a0) (preinitialObj PI) ] ] ≈ id1 A a0 ]
+      kfuc=1 {k1} {p} = e=id ( kfuc=uc )
       -- if equalizer has right inverse, f = g
       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 ] )
@@ -102,14 +103,15 @@
                ≈⟨ idR ⟩
                 g
             ∎
-      lemma1 : (a : Obj A) (f : Hom A a0 a) → A [ f ≈ initialArrow a ]
+      lemma1 : (a : Obj A) (f' : Hom A a0 a) → A [ f' ≈ initialArrow a ]
       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' equ-fi (kfuc=1 {a} ) ⟩
+             ≈⟨ lemma2 a0 a (A [ preinitialArrow PI {a} o  limit (lim F) a0 (u a0) ]) f' {ep {a0} {a} {f'} {f'} } equ-fi 
+                      (kfuc=1 {ee} {ep} ) ⟩
                  f'
              ∎  )