# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1472457723 -32400
# Node ID ef37decef1ca60abd51f4180e163ea98ed50f2be
# Parent  9f014f34b988cb2f86de56a32ab92c1089b0d4da
initialFullSubCategory

diff -r 9f014f34b988 -r ef37decef1ca freyd.agda
--- a/freyd.agda	Sun Aug 28 18:59:40 2016 +0900
+++ b/freyd.agda	Mon Aug 29 17:02:03 2016 +0900
@@ -16,9 +16,8 @@
            : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
    field
       ≈→≡ : {a b : Obj A } →  { x y : Hom A (FObj F a) (FObj F b) } → 
-                (x≈y : A [ FMap F x ≈ FMap F y  ]) → FMap F x ≡ FMap F y   -- co-comain of FMap is local small
+                (x≈y : A [ FMap F x ≈ FMap F y  ]) → FMap F x ≡ FMap F y   -- codomain of FMap is local small
       full→ : { a b : Obj A } { x : Hom A (FObj F a) (FObj F b) } → A [ FMap F ( FMap← x ) ≈ x ]
-      full← : { a b : Obj A } { x : Hom A a b } → A [ FMap← ( FMap F x ) ≈ x ]
 
 -- pre-initial
 
@@ -47,7 +46,8 @@
       (lim : ( Γ : Functor A A ) → { a0 : Obj A } { u : NTrans A A ( K A A a0 ) Γ } → Limit A A Γ a0 u ) -- completeness
       ( 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 }
+      (PI : PreInitial A F ) → { a0 : Obj A } → 
+      { u : (a : Obj A) → NTrans A A (K A A a) F }  -- Does it exist?
           → HasInitialObject A a0
 initialFromPreInitialFullSubcategory A F  FMap← lim equ SFS PI {a0} {u} = record {
       initial = initialArrow ; 
@@ -55,16 +55,12 @@
     } where
       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 )  ] 
-      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) 
-             ≈⟨ {!!} ⟩
-                 f
-             ∎  )
+      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
+      open Equalizer
+      kfuc=1 : {k1 c : 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} = {!!}
       -- 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 ]
@@ -87,4 +83,14 @@
                ≈⟨ idR ⟩
                 g
             ∎
+      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 {!!} {!!} {!!} (kfuc=1 {{!!}} {{!!}} ) ⟩
+                 f
+             ∎  )