# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1472537477 -32400
# Node ID 61550782be4a0fe8e0ac1e6824fb49e19ffe970f
# Parent  ff36c500962e4c51adf061d09b52708ef07a84c3
preinital full subcategory done

diff -r ff36c500962e -r 61550782be4a freyd.agda
--- a/freyd.agda	Tue Aug 30 14:22:47 2016 +0900
+++ b/freyd.agda	Tue Aug 30 15:11:17 2016 +0900
@@ -81,7 +81,22 @@
       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 {k1} {c} = {!!}
+      kfuc=uc {c} {k1} {p} =  let open ≈-Reasoning (A) in
+            begin
+                 TMap u  c  o ( p o ( preinitialArrow PI {k1} o TMap u (preinitialObj PI)  ))
+            ≈⟨ cdr assoc  ⟩
+                 TMap u c o ((p o preinitialArrow PI) o TMap u (preinitialObj PI))
+            ≈⟨ assoc ⟩
+                 (TMap u  c  o ( p o ( preinitialArrow PI {k1} ))) o TMap u (preinitialObj PI)  
+            ≈↑⟨ 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 id1 A (limit-c comp F)
+            ≈⟨ 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} {p} = e=id ( kfuc=uc )
       -- if equalizer has right inverse, f = g
@@ -98,8 +113,7 @@
                  f o  (  e o e'  ) 
                ≈⟨ assoc  ⟩
                  ( f o  e ) o e'  
-               ≈⟨ car ( fe=ge equ ) ⟩
-                 ( g o  e ) o e'  
+               ≈⟨ car ( fe=ge equ ) ⟩ ( g o  e ) o e'  
                ≈↑⟨ assoc  ⟩
                  g o  (  e o e'  ) 
                ≈⟨ cdr inv-e   ⟩