Mercurial > hg > Members > kono > Proof > category

changeset 643:5eb746702732

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 Mon, 03 Jul 2017 12:20:26 +0900
parents 53f2a11474ee
children 8e35703ef116
files freyd2.agda
diffstat 1 files changed, 8 insertions(+), 15 deletions(-) [+]
line wrap: on
line diff
--- a/freyd2.agda	Mon Jul 03 08:41:01 2017 +0900
+++ b/freyd2.agda	Mon Jul 03 12:20:26 2017 +0900
@@ -299,26 +299,19 @@
                ; 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
-               revUub : (pi : FObj U (obj (preinitialObj PI)) ) → pi ≡ (hom (preinitialObj PI) OneObj)
-               revUub _ = {!!}
-               revU' : (a : Obj (K Sets A * ↓ U)) 
+               lim-t0 : (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} 
+                  → NTrans I A (K A I (a0 lim)) Γ
+               lim-t0 a t x {y} {z} {f} = t0 lim
+               lim-t0-comm : (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 TMap (t0 lim) y ] ≈ A [ TMap (t0 lim) z o FMap (K A I (a0 lim)) f ] ]
+               lim-t0-comm a t x {y} {z} {f} = IsNTrans.commute (isNTrans (t0 lim))
+               revU : (a : Obj (K Sets A * ↓ U)) 
                   → Sets [ Sets [ FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ) o hom (preinitialObj PI) ] ≈ hom a ]
-               revU' a  =  let open ≈-Reasoning Sets in begin
+               revU a  =  let open ≈-Reasoning Sets in begin
                      FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) o hom (preinitialObj PI)
                   ≈⟨ comm (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ⟩
                      hom a
                   ∎ 
-               revU : (a : Obj (K Sets A * ↓ U)) 
-                  → Sets [ FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ) ≈ ( λ upi → hom a OneObj ) ]
-               revU a  = extensionality Sets ( λ (upi : FObj U (obj (preinitialObj PI)) ) → ( begin 
-                     FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) upi  
-                  ≡⟨ {!!} ⟩
-                     FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) (hom (preinitialObj PI) OneObj)
-                  ≡⟨ ≡-cong ( λ k → k OneObj ) ( comm (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) ⟩
-                     hom a OneObj
-                ∎  ) ) where
-                  open  import  Relation.Binary.PropositionalEquality
-                  open ≡-Reasoning
                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}