# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1498958246 -32400
# Node ID 0d6cab67eadcab2d7be864f06191173d41ec8d02
# Parent  4cf8f982dc5b01a36888696d0ef8e49ea3bd0964
add more lemma

diff -r 4cf8f982dc5b -r 0d6cab67eadc freyd2.agda
--- a/freyd2.agda	Sun Jul 02 02:18:57 2017 +0900
+++ b/freyd2.agda	Sun Jul 02 10:17:26 2017 +0900
@@ -296,9 +296,17 @@
                tacomm0 : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) {y : Obj I} {z : Obj I} {f : Hom I y z} 
                   → Sets [ Sets [ FMap (U ○ Γ) f o TMap t y ] ≈ Sets [ TMap t z o FMap ( K Sets I a ) f ] ]
                tacomm0 a t x {y} {z} {f} = IsNTrans.commute ( isNTrans t )  {y} {z} {f}
-               sfcomm : Sets [ Sets [ FMap U ( arrow (FMap (SFSF SFS) (fArrow A U (FMap Γ f) (TMap t y x)))) o hom (preinitialObj PI) ]
-                   ≈ Sets [ hom (FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x)) o FMap ( K Sets A * ) ( arrow (FMap (SFSF SFS) (fArrow A U (FMap Γ f) (TMap t y x)))) ]
-               sfcomm = ? 
+               sfcomm : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) {y : Obj I} {z : Obj I} {f : Hom I y z} 
+                  → Sets [ Sets [ FMap U ( arrow (FMap (SFSF SFS) (fArrow A U (FMap Γ f) (TMap t y x))))
+                        o hom (FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))) ]
+                     ≈ Sets [ hom (FObj (SFSF SFS) (ob A U (FObj Γ z) (FMap U (FMap Γ f) (TMap t y x)))) o
+                          FMap ( K Sets A * ) ( arrow (FMap (SFSF SFS) (fArrow A U (FMap Γ f) (TMap t y x)))) ] ]
+               sfcomm a t x {y} {z} {f} = comm (FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x )) )
+               commacomm : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) {y : Obj I} {z : Obj I} {f : Hom I y z} 
+                  → ( K (Sets) A * ↓ U) [ ( K (Sets) A * ↓ U) [ FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x ))
+                        o preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))} ]
+                     ≈ preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (FMap U (FMap Γ f) (TMap t y x))) } ]
+               commacomm = {!!}
                tacomm : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) {y : Obj I} {z : Obj I} {f : Hom I y z} 
                   → A [ A [ FMap Γ f o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))})) ] ≈
                         A [ arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} ))
@@ -318,6 +326,8 @@
                     arrow ( SFSFMap← SFS (( K (Sets) A * ↓ U) [ FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x ))
                         o preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))} ] ) )
                  ≈⟨ {!!} ⟩
+                    arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (FMap U (FMap Γ f) (TMap t y x)))} ))
+                 ≈⟨ {!!} ⟩
                     arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} ))
                  ≈↑⟨ idR ⟩
                     arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} ))