# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1498479804 -32400
# Node ID d2fc6fb58e0ebc5a7187902ae055c44c84099133
# Parent  693020c766d211fcfe31af851b3775f418f68c9b
fix

diff -r 693020c766d2 -r d2fc6fb58e0e freyd2.agda
--- a/freyd2.agda	Mon Jun 26 17:41:02 2017 +0900
+++ b/freyd2.agda	Mon Jun 26 21:23:24 2017 +0900
@@ -261,25 +261,30 @@
    } where
       pi : Obj ( K (Sets) A * ↓ U) 
       pi = preinitialObj PI
+      pihom : Hom Sets (FObj (K Sets A *) (obj pi)) (FObj U (obj pi))
+      pihom = hom pi
       ub : (b : Obj A) (x : FObj U b ) → Hom Sets (FObj (K Sets A *) b) (FObj U b)
       ub b x OneObj = x
+      ob : (b : Obj A) (x : FObj U b ) → Obj ( K Sets A * ↓ U)
+      ob b x = record { obj = b ; hom = ub b x}
+      piArrow : (b : Obj ( K Sets A * ↓ U)) → Hom ( K Sets A * ↓ U) pi b
+      piArrow b =  SFSFMap← SFS ( preinitialArrow PI )
       tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj pi)) b)
-      tmap1 b x =  arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))  
-      tmap2 :  (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b)
-      tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) OneObj )
+      tmap1 b x =  arrow ( piArrow ( ob b x ) )
+      preinitComm : (a : Obj A ) ( x : FObj U a ) → Sets [ Sets [ FMap U (arrow (piArrow (ob a x))) o hom pi ]
+         ≈ Sets [ ub a x  o FMap (K Sets A *) (arrow (piArrow (ob a x))) ] ]
+      preinitComm a x = comm (piArrow (ob a x ))
       comm11 : (a b : Obj A) (f : Hom A a b) (y : FObj U a ) →
-         ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o
-             ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a x}) } ))) ] ) y   
-           ≡ (Sets [ ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))) o FMap U f ] ) y
+         ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow (ob a x))) ] ) y   
+           ≡ (Sets [ ( λ x → arrow (piArrow (ob b x))) o FMap U f ] ) y
       comm11 a b f y = begin
-               ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o
-                 ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a x}) } ))) ] ) y   
+               ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow (ob a x))) ] ) y   
              ≡⟨⟩
-                 A [ f o arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a y}) } )) ]
+                 A [ f o arrow (piArrow (ob a y)) ]
              ≡⟨ {!!} ⟩
-                arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b (FMap U f y) } ) } ) )
+                arrow (piArrow (ob b (FMap U f y) ))
              ≡⟨⟩
-                (Sets [ ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))) o FMap U f ] ) y
+                (Sets [ ( λ x → arrow (piArrow (ob b x))) o FMap U f ] ) y
              ∎  where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
@@ -287,9 +292,9 @@
       comm1 {a} {b} {f} = let open ≈-Reasoning Sets in begin
                 FMap (Yoneda A (obj (preinitialObj PI))) f o tmap1 a 
              ≈⟨⟩
-                FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = a ; hom = ub a x}) } )))  
+                FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow ( ob a x )))  
              ≈⟨ extensionality Sets ( λ y → comm11 a b f y ) ⟩
-                ( λ x → arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (record { obj = b ; hom = ub b x}) } ))) o FMap U f 
+                ( λ x → arrow (piArrow (ob b x))) o FMap U f 
              ≈⟨⟩
                 tmap1 b o FMap U f 
              ∎ 
@@ -303,6 +308,8 @@
              ∎  where
                   open  import  Relation.Binary.PropositionalEquality
                   open ≡-Reasoning
+      tmap2 :  (b : Obj A) → Hom Sets (FObj (Yoneda A (obj (preinitialObj PI))) b) (FObj U b)
+      tmap2 b x = ( FMap U x ) ( hom ( preinitialObj PI ) OneObj )
       comm2 : {a b : Obj A} {f : Hom A a b} → Sets [ Sets [ FMap U f o tmap2 a ] ≈
         Sets [ tmap2 b o FMap (Yoneda A (obj (preinitialObj PI))) f ] ]
       comm2 {a} {b} {f} = let open ≈-Reasoning Sets in begin