Mercurial > hg > Members > kono > Proof > category

changeset 640:0d6cab67eadc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add more lemma
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 02 Jul 2017 10:17:26 +0900
parents 4cf8f982dc5b
children c65d08d85092
files freyd2.agda
diffstat 1 files changed, 13 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- 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))} ))