# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1498481935 -32400
# Node ID 7be3eb96310cbf006b0d054541dc8f8fc497498c
# Parent  d2fc6fb58e0ebc5a7187902ae055c44c84099133
introduce fArrow

diff -r d2fc6fb58e0e -r 7be3eb96310c freyd2.agda
--- a/freyd2.agda	Mon Jun 26 21:23:24 2017 +0900
+++ b/freyd2.agda	Mon Jun 26 21:58:55 2017 +0900
@@ -268,7 +268,36 @@
       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 )
+      piArrow b =  SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) b} )
+      fArrowComm1 : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → (y : * ) → FMap U f ( ub a x y ) ≡ ub b (FMap U f x) y
+      fArrowComm1 a b f x OneObj = begin
+               FMap U f ( ub a x OneObj ) 
+             ≡⟨⟩
+               FMap U f x
+             ≡⟨⟩
+               ub b (FMap U f x) OneObj
+             ∎  where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+      fArrowComm : (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → 
+         Sets [ Sets [ FMap U f o hom (ob a x) ] ≈ Sets [ hom (ob b (FMap U f x)) o FMap (K Sets A *) f ] ]
+      fArrowComm a b f x = extensionality Sets ( λ y → begin 
+                ( Sets [ FMap U f o hom (ob a x) ] ) y 
+             ≡⟨⟩
+                FMap U f ( hom (ob a x) y )
+             ≡⟨⟩
+                FMap U f ( ub a x y )
+             ≡⟨ fArrowComm1 a b f x y ⟩
+                ub b (FMap U f x) y
+             ≡⟨⟩
+                hom (ob b (FMap U f x)) y
+             ≡⟨⟩
+                ( Sets [ hom (ob b (FMap U f x)) o FMap (K Sets A *) f ] ) y
+             ∎ ) where
+                  open  import  Relation.Binary.PropositionalEquality
+                  open ≡-Reasoning
+      fArrow :  (a b : Obj A) (f : Hom A a b) (x : FObj U a ) → Hom ( K Sets A * ↓ U) ( ob a x ) (ob b (FMap U f x) )
+      fArrow a b f x = record { arrow = f ; comm = fArrowComm a b f x }
       tmap1 :  (b : Obj A) → Hom Sets (FObj U b) (FObj (Yoneda A (obj pi)) b)
       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 ]
@@ -281,6 +310,10 @@
                ( Sets [ FMap (Yoneda A (obj (preinitialObj PI))) f o ( λ x → arrow (piArrow (ob a x))) ] ) y   
              ≡⟨⟩
                  A [ f o arrow (piArrow (ob a y)) ]
+             ≡⟨⟩
+                 A [ arrow ( fArrow a b f y )  o arrow (piArrow (ob a y)) ]
+             ≡⟨⟩
+                arrow ( ( K Sets A * ↓ U) [ ( fArrow a b f y )  o (piArrow (ob a y)) ] )
              ≡⟨ {!!} ⟩
                 arrow (piArrow (ob b (FMap U f y) ))
              ≡⟨⟩