Mercurial > hg > Members > kono > Proof > category

diff freyd2.agda @ 639:4cf8f982dc5b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 02 Jul 2017 02:18:57 +0900
parents a07b95e92933
children 0d6cab67eadc
line wrap: on
line diff
--- a/freyd2.agda	Sat Jul 01 10:21:34 2017 +0900
+++ b/freyd2.agda	Sun Jul 02 02:18:57 2017 +0900
@@ -293,6 +293,12 @@
                ; t0f=t = λ {a t i} → t0f=t0 {a} {t} {i}
                ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t 
          } where
+               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 = ? 
                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))} ))
@@ -305,9 +311,12 @@
                  ≈⟨ {!!} ⟩
                     arrow (SFSFMap← SFS (FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x )) ))
                         o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))})) 
+                 ≈⟨⟩
+                    arrow (( K (Sets) A * ↓ U) [ SFSFMap← SFS (FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x )) )
+                        o SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))}) ] )
                  ≈⟨ {!!} ⟩
-                    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 (( 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) (TMap t z x))} ))
                  ≈↑⟨ idR ⟩
@@ -317,7 +326,7 @@
                ta : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) → NTrans I A (K A I (obj (preinitialObj PI))) Γ
                ta a t x = record {  TMap = λ (a : Obj I ) →
                    arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ a) (TMap t a x))} ) )
-                ; isNTrans = record { commute = {!!} }} -- λ {a} {b} {f} → commute2 {a} {b} {f} }
+                ; isNTrans = record { commute = λ {y} {z} {f} → tacomm a t x {y} {z} {f} }} 
                ψ : (a : Obj Sets) → NTrans I Sets (K Sets I a) (U ○ Γ) → Hom Sets a (FObj U (a0 lim))
                ψ a t x = FMap U (limit (isLimit lim) (obj (preinitialObj PI)) (ta a t x)) ( hom (preinitialObj PI) OneObj )
                t0f=t0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (U ○ Γ)} {i : Obj I} →