# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1498637837 -32400
# Node ID 5b0286e3aa323c647e00ba2e7fb82af1cf14a611
# Parent  37fa9d3fab8c0afe03835314df6ee9f17ff4ae59
fix

diff -r 37fa9d3fab8c -r 5b0286e3aa32 freyd2.agda
--- a/freyd2.agda	Wed Jun 28 08:55:11 2017 +0900
+++ b/freyd2.agda	Wed Jun 28 17:17:17 2017 +0900
@@ -299,8 +299,21 @@
       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
       preinitialEqu : {x y : Obj ( K (Sets) A * ↓ U) } → (f : Hom ( K (Sets) A * ↓ U) x y ) → 
-          IsEqualizer A ee (A [ arrow f o arrow ( piArrow x ) ] ) ( arrow ( piArrow y )  ) 
-      preinitialEqu {x} {y} f = Complete.isEqualizer comp ( A [ arrow f o arrow (piArrow x)  ] ) ( arrow ( piArrow y )) 
+          IsEqualizer A ee (A [ arrow f o arrow ( preinitialArrow PI {x}) ] ) ( arrow ( preinitialArrow PI {y}) ) 
+      preinitialEqu {x} {y} f = Complete.isEqualizer comp ( A [ arrow f o arrow (preinitialArrow PI)  ] ) ( arrow ( preinitialArrow PI )) 
+      pa : {x y : Obj ( K (Sets) A * ↓ U) } → (f : Hom ( K (Sets) A * ↓ U) x y )
+         → Hom ( K (Sets) A * ↓ U) (preinitialObj PI)
+           (ob (Complete.equalizer-p comp ( A [ arrow f o arrow (preinitialArrow PI) ] ) ( arrow ( preinitialArrow PI ))) {!!} )
+      pa {x} {y} f = piArrow (ob (Complete.equalizer-p comp ( A [ arrow f o arrow (preinitialArrow PI) ] ) ( arrow ( preinitialArrow PI ))) {!!} ) 
+        --
+        --         e             f
+        --    c  -------→ a ---------→ b
+        --    ^        .     ---------→
+        --    |      .            g
+        --    |k   .
+        --    |  . h
+        --    d
+        --
       comm13 : (a b : Obj ( K Sets A * ↓ U)) (f : Hom ( K Sets A * ↓ U) a b )  → ( K Sets A * ↓ U) [
            ( K Sets A * ↓ U) [ f o preinitialArrow PI ]  ≈ preinitialArrow PI ]   
       comm13 a b f = let open ≈-Reasoning A in begin
@@ -309,7 +322,7 @@
                 arrow f o arrow ( preinitialArrow PI {{!!}})
              ≈⟨ {!!} ⟩
                 arrow ( preinitialArrow PI {{!!}} )
-             ∎ 
+             ∎  
       comm12 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) → ( K Sets A * ↓ U) [
           FMap (SFSF SFS) ( ( K Sets A * ↓ U) [ fArrow a b f y o (piArrow (ob a y)) ] ) ≈ FMap (SFSF SFS) ( piArrow (ob b (FMap U f y ))) ] 
       comm12 a b f y = let open ≈-Reasoning ( K Sets A * ↓ U) in begin