# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1388996293 -32400
# Node ID d1af69c4aaf88461abf8b8fef58c92e886a0b392
# Parent  d72730946ba5bf21f623601c3ec7e2a018afca9a
on going...

diff -r d72730946ba5 -r d1af69c4aaf8 freyd.agda
--- a/freyd.agda	Mon Jan 06 00:46:48 2014 +0900
+++ b/freyd.agda	Mon Jan 06 17:18:13 2014 +0900
@@ -25,15 +25,14 @@
 record PreInitial {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
       (F : Functor A A )  : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
    field
-      preinitial : ∀{  a : Obj A } → { b : Obj A } →  Hom A ( FObj F b ) a 
-      uniqueness  : ∀{  a : Obj A } → { b : Obj A } →  ( f : Hom A ( FObj F b ) a ) →
-          A [ f  ≈  preinitial {a} {b} ]
+      preinitialObj : ∀{  a : Obj A } →  Obj A 
+      preinitialArrow : ∀{  a : Obj A } →  Hom A ( FObj F (preinitialObj {a} )) a 
 
 -- initial object
 
 record HasInitialObject {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (i : Obj A) : Set  (suc ℓ ⊔ (suc c₁ ⊔ suc c₂)) where
    field
-      initial :  ( a : Obj A ) →  Hom A i a
+      initial :  ∀( a : Obj A ) →  Hom A i a
       uniqueness  : ( a : Obj A ) →  ( f : Hom A i a ) → A [ f ≈  initial a ]
 
 
@@ -51,28 +50,22 @@
       (PI : PreInitial A F ) → { a0 : Obj A } → { u : (a : Obj A) → NTrans A A (K A A a) F }
           → HasInitialObject A a0
 initialFromPreInitialFullSubcategory A F  FMap← lim SFS PI {a0} {u} = record {
-      initial = λ a → limit (lim F {a} {u a} ) a0 (u a0) ; 
+      initial = initialArrow ; 
       uniqueness  = λ a f → lemma1 a f
     } where
-      lemma1 : (a : Obj A) (f : Hom A a0 a) → A [ f ≈ limit (lim F) 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 )  ] 
+      lemma1 : (a : Obj A) (f : Hom A a0 a) → A [ f ≈ initialArrow a ]
       lemma1 a f = let open ≈-Reasoning (A) in 
              begin
                  f
-             ≈↑⟨ limit-uniqueness (lim F) ( λ {i} →
-             begin
-                  TMap (u a) i o f 
-             ≈⟨ cdr {!!} ⟩
-                  TMap (u a) i o ( preinitial PI {a} {i} o (limit (lim F {FObj F i } {u {!!} }) a0 ( u a0 ) ) )
-             ≈⟨ cdr {!!} ⟩
-                  TMap (u a) i o ( preinitial PI {a} {i} o TMap (u a0) i )
-             ≈⟨ assoc  ⟩
-                  ( TMap (u a) i o  preinitial PI {a} {i} ) o TMap (u a0) i 
+             ≈↑⟨ idR ⟩
+                 f o id1 A a0
              ≈⟨ {!!} ⟩
-                  id1 A (FObj F i) o TMap (u a0) i 
-             ≈⟨ idL  ⟩
-                  TMap (u a0) i
-             ∎ 
-             )⟩
-                 limit (lim F) a0 (u a0)
+                 ( preinitialArrow PI {a} o  limit (lim F) a0 (u a0)) o id1 A a0
+             ≈⟨ idR ⟩
+                 preinitialArrow PI {a} o  limit (lim F) a0 (u a0) 
+             ≈⟨⟩
+                 initialArrow a
              ∎