# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1472718868 -32400
# Node ID 87600d338337413b705e4fd6799798caefa9333a
# Parent  61550782be4a0fe8e0ac1e6824fb49e19ffe970f
fix

diff -r 61550782be4a -r 87600d338337 freyd.agda
--- a/freyd.agda	Tue Aug 30 15:11:17 2016 +0900
+++ b/freyd.agda	Thu Sep 01 17:34:28 2016 +0900
@@ -12,12 +12,14 @@
 -- C is small full subcategory of A ( C is image of F )
 
 record SmallFullSubcategory {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) 
-      (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
            : 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   -- 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 ]
+      SFSF : Functor A A  
+      SFSFMap← : { a b : Obj A } → Hom A (FObj SFSF a) (FObj SFSF b ) → Hom A a b 
+      full→ : { a b : Obj A } { x : Hom A (FObj SFSF a) (FObj SFSF b) } → A [ FMap SFSF ( SFSFMap← x ) ≈ x ]
+
+      -- ≈→≡ : {a b : Obj A } →  { x y : Hom A (FObj SFSF a) (FObj SFSF b) } → 
+      --          (x≈y : A [ FMap SFSF x ≈ FMap SFSF y  ]) → FMap SFSF x ≡ FMap SFSF y   -- codomain of FMap is local small
 
 -- pre-initial
 
@@ -44,41 +46,46 @@
 open Equalizer
 
 initialFromPreInitialFullSubcategory : {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ)
-      (F : Functor A A ) ( FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b )
       (comp : Complete A A)
-      (SFS : SmallFullSubcategory A F FMap← ) → 
-      (PI : PreInitial A F ) → { a0 : Obj A } → HasInitialObject A (limit-c comp F)
-initialFromPreInitialFullSubcategory A F  FMap← comp SFS PI = record {
+      (SFS : SmallFullSubcategory A ) → 
+      (PI : PreInitial A (SFSF SFS )) → { a0 : Obj A } → HasInitialObject A (limit-c comp (SFSF SFS))
+initialFromPreInitialFullSubcategory A comp SFS PI = record {
       initial = initialArrow ; 
       uniqueness  = λ a f → lemma1 a f
     } where
+      F : Functor A A 
+      F = SFSF SFS   
+      FMap← : { a b : Obj A } → Hom A (FObj F a) (FObj F b ) → Hom A a b 
+      FMap←  = SFSFMap←  SFS
       lim : ( Γ : Functor A A ) → Limit A A Γ (limit-c comp Γ)  (limit-u comp Γ)
       lim Γ =  isLimit comp Γ 
       equ : {a b : Obj A} → (f g : Hom A a b)  → Equalizer A (equalizer-e comp f g ) f g
       equ f g = isEqualizer comp f g 
+      a0 : Obj A
       a0 = limit-c comp F
+      u : NTrans A A (K A A a0) F
       u = limit-u comp F
-      ee : {a b : Obj A} → {f g : Hom A a b}  → Obj A 
-      ee {a} {b} {f} {g} = equalizer-p comp f g
-      ep :  {a b : Obj A} → {f g : Hom A a b}  → Hom A (ee {a} {b} {f} {g} ) a 
-      ep {a} {b} {f} {g} = equalizer-e comp f g  
-      f : {a : Obj A} -> Hom A  a0 (FObj F  (preinitialObj PI {a} ) ) 
+      ep : {a b : Obj A} → {f g : Hom A a b}  → Obj A 
+      ep {a} {b} {f} {g} = equalizer-p comp f g
+      ee :  {a b : Obj A} → {f g : Hom A a b}  → Hom A (ep {a} {b} {f} {g} ) a 
+      ee {a} {b} {f} {g} = equalizer-e comp f g  
+      f : {a : Obj A} → Hom A  a0 (FObj F  (preinitialObj PI {a} ) ) 
       f {a} = TMap u (preinitialObj PI {a} ) 
       initialArrow :  ∀( a : Obj A )  →  Hom A a0 a
       initialArrow a  = A [ preinitialArrow PI {a}  o f ]
-      equ-fi : { a : Obj A} -> {f' : Hom A a0 a} -> 
-          Equalizer A ep ( A [ preinitialArrow PI {a} o  f ] ) f'
+      equ-fi : { a : Obj A} → {f' : Hom A a0 a} → 
+          Equalizer A ee ( A [ preinitialArrow PI {a} o  f ] ) f'
       equ-fi  {a} {f'} = equ ( A [ preinitialArrow PI {a} o  f ] ) f'
-      e=id : {e : Hom A a0 a0} -> ( {c : Obj A} -> A [ A [ TMap u  c o  e ]  ≈  TMap u c ] ) -> A [ e  ≈ id1 A a0 ]
+      e=id : {e : Hom A a0 a0} → ( {c : Obj A} → A [ A [ TMap u  c o  e ]  ≈  TMap u c ] ) → A [ e  ≈ id1 A a0 ]
       e=id  {e} uce=uc =  let open ≈-Reasoning (A) in
             begin
               e
-            ≈↑⟨ limit-uniqueness  (lim F) e ( \{i} -> uce=uc ) ⟩
+            ≈↑⟨ limit-uniqueness  (lim F) e ( λ {i} → uce=uc ) ⟩
               limit (lim F) a0 u 
-            ≈⟨ limit-uniqueness (lim F) (id1 A a0) ( \{i} -> idR ) ⟩
+            ≈⟨ limit-uniqueness (lim F) (id1 A a0) ( λ {i} → idR ) ⟩
               id1 A a0
             ∎
-      kfuc=uc : {c k1 : Obj A} ->  {p : Hom A k1 a0} -> A [ A [ TMap u  c  o  
+      kfuc=uc : {c k1 : Obj A} →  {p : Hom A k1 a0} → A [ A [ TMap u  c  o  
               A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ]  
                       ≈ TMap u c ]
       kfuc=uc {c} {k1} {p} =  let open ≈-Reasoning (A) in
@@ -91,18 +98,18 @@
             ≈↑⟨ car  ( full→ SFS ) ⟩
                   FMap F (FMap← (TMap u c o p o preinitialArrow PI)) o TMap u (preinitialObj PI)
             ≈⟨ nat u  ⟩
-                  TMap u c o FMap (K A A (limit-c comp F)) (FMap← (TMap u c o p o preinitialArrow PI)) 
+                  TMap u c o FMap (K A A a0) (FMap← (TMap u c o p o preinitialArrow PI)) 
             ≈⟨⟩
-                  TMap u c o id1 A (limit-c comp F)
+                  TMap u c o id1 A a0
             ≈⟨ idR ⟩
                  TMap u  c  
             ∎
-      kfuc=1 : {k1 : Obj A} ->  {p : Hom A k1 a0} -> A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (preinitialObj PI) ] ] ≈ id1 A a0 ]
+      kfuc=1 : {k1 : Obj A} →  {p : Hom A k1 a0} → A [ A [ p o A [ preinitialArrow PI {k1} o TMap u (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 ] )
-           -> A [ f ≈ g ]
+           → A [ f ≈ g ]
       lemma2 a b {c} f g {e} {e'} equ inv-e = let open ≈-Reasoning (A) in
             let open Equalizer in
             begin
@@ -128,8 +135,8 @@
                  initialArrow a
              ≈⟨⟩
                  preinitialArrow PI {a} o  f
-             ≈⟨ lemma2 a0 a (A [ preinitialArrow PI {a} o  f ]) f' {ep {a0} {a} {A [ preinitialArrow PI {a} o  f ]} {f'} } (equ-fi )
-                      (kfuc=1 {ee} {ep} ) ⟩
+             ≈⟨ lemma2 a0 a (A [ preinitialArrow PI {a} o  f ]) f' {ee {a0} {a} {A [ preinitialArrow PI {a} o  f ]} {f'} } (equ-fi )
+                      (kfuc=1 {ep} {ee} ) ⟩
                  f'
              ∎  )
  
diff -r 61550782be4a -r 87600d338337 limit-to.agda
--- a/limit-to.agda	Tue Aug 30 15:11:17 2016 +0900
+++ b/limit-to.agda	Thu Sep 01 17:34:28 2016 +0900
@@ -329,9 +329,9 @@
           ≈-cong {a} {b} {f} {g} (just eq) | just _ | just _ = eq
 
 -- indexFunctor' :  {c₁ c₂ ℓ : Level} (A : Category c₁ c₂ ℓ) (none : Nil A) ( a b : Obj A) ( f g : Hom A a b ) 
---        →  ( obj→ : Obj A -> TwoObject  {c₁}  )
---        →  ( hom→ : { a b : Obj A } -> Hom A a b -> Arrow t0 t0 (obj→ a) (obj→ b)   )
---        →  ( { x y : Obj A } { h i : Hom A x y } -> A [ h  ≈ i ]  →  hom→  h ≡ hom→  i  )
+--        →  ( obj→ : Obj A → TwoObject  {c₁}  )
+--        →  ( hom→ : { a b : Obj A } → Hom A a b → Arrow t0 t0 (obj→ a) (obj→ b)   )
+--        →  ( { x y : Obj A } { h i : Hom A x y } → A [ h  ≈ i ]  →  hom→  h ≡ hom→  i  )
 --        →  Functor A A
 --   this one does not work on fmap ( g o f )  ≈  ( fmap g o fmap f )
 --      because  g o f can be arrow-f when g is arrow-g