Mercurial > hg > Members > kono > Proof > category

comparison 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
comparison
equal deleted inserted replaced
638:a07b95e92933 639:4cf8f982dc5b
291 limitInSets Γ lim = record { 291 limitInSets Γ lim = record {
292 limit = λ a t → ψ a t 292 limit = λ a t → ψ a t
293 ; t0f=t = λ {a t i} → t0f=t0 {a} {t} {i} 293 ; t0f=t = λ {a t i} → t0f=t0 {a} {t} {i}
294 ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t 294 ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t
295 } where 295 } where
296 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}
297 → Sets [ Sets [ FMap (U ○ Γ) f o TMap t y ] ≈ Sets [ TMap t z o FMap ( K Sets I a ) f ] ]
298 tacomm0 a t x {y} {z} {f} = IsNTrans.commute ( isNTrans t ) {y} {z} {f}
299 sfcomm : Sets [ Sets [ FMap U ( arrow (FMap (SFSF SFS) (fArrow A U (FMap Γ f) (TMap t y x)))) o hom (preinitialObj PI) ]
300 ≈ 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)))) ]
301 sfcomm = ?
296 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} 302 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}
297 → A [ A [ FMap Γ f o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))})) ] ≈ 303 → A [ A [ FMap Γ f o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))})) ] ≈
298 A [ arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} )) 304 A [ arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} ))
299 o FMap (K A I (obj (preinitialObj PI))) f ] ] 305 o FMap (K A I (obj (preinitialObj PI))) f ] ]
300 tacomm a t x {y} {z} {f} = let open ≈-Reasoning A in begin 306 tacomm a t x {y} {z} {f} = let open ≈-Reasoning A in begin
303 arrow (fArrow A U (FMap Γ f) (TMap t y x )) 309 arrow (fArrow A U (FMap Γ f) (TMap t y x ))
304 o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))})) 310 o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))}))
305 ≈⟨ {!!} ⟩ 311 ≈⟨ {!!} ⟩
306 arrow (SFSFMap← SFS (FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x )) )) 312 arrow (SFSFMap← SFS (FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x )) ))
307 o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))})) 313 o arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))}))
314 ≈⟨⟩
315 arrow (( K (Sets) A * ↓ U) [ SFSFMap← SFS (FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x )) )
316 o SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))}) ] )
308 ≈⟨ {!!} ⟩ 317 ≈⟨ {!!} ⟩
309 arrow (SFSFMap← SFS (( K (Sets) A * ↓ U) [ FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x )) 318 arrow ( SFSFMap← SFS (( K (Sets) A * ↓ U) [ FMap (SFSF SFS) ( fArrow A U (FMap Γ f) (TMap t y x ))
310 o preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))} ] )) 319 o preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ y) (TMap t y x))} ] ) )
311 ≈⟨ {!!} ⟩ 320 ≈⟨ {!!} ⟩
312 arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} )) 321 arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} ))
313 ≈↑⟨ idR ⟩ 322 ≈↑⟨ idR ⟩
314 arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} )) 323 arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ z) (TMap t z x))} ))
315 o FMap (K A I (obj (preinitialObj PI))) f 324 o FMap (K A I (obj (preinitialObj PI))) f
316 ∎ 325 ∎
317 ta : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) → NTrans I A (K A I (obj (preinitialObj PI))) Γ 326 ta : (a : Obj Sets) ( t : NTrans I Sets (K Sets I a) (U ○ Γ) ) (x : a) → NTrans I A (K A I (obj (preinitialObj PI))) Γ
318 ta a t x = record { TMap = λ (a : Obj I ) → 327 ta a t x = record { TMap = λ (a : Obj I ) →
319 arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ a) (TMap t a x))} ) ) 328 arrow ( SFSFMap← SFS ( preinitialArrow PI {FObj (SFSF SFS) (ob A U (FObj Γ a) (TMap t a x))} ) )
320 ; isNTrans = record { commute = {!!} }} -- λ {a} {b} {f} → commute2 {a} {b} {f} } 329 ; isNTrans = record { commute = λ {y} {z} {f} → tacomm a t x {y} {z} {f} }}
321 ψ : (a : Obj Sets) → NTrans I Sets (K Sets I a) (U ○ Γ) → Hom Sets a (FObj U (a0 lim)) 330 ψ : (a : Obj Sets) → NTrans I Sets (K Sets I a) (U ○ Γ) → Hom Sets a (FObj U (a0 lim))
322 ψ a t x = FMap U (limit (isLimit lim) (obj (preinitialObj PI)) (ta a t x)) ( hom (preinitialObj PI) OneObj ) 331 ψ a t x = FMap U (limit (isLimit lim) (obj (preinitialObj PI)) (ta a t x)) ( hom (preinitialObj PI) OneObj )
323 t0f=t0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (U ○ Γ)} {i : Obj I} → 332 t0f=t0 : {a : Obj Sets} {t : NTrans I Sets (K Sets I a) (U ○ Γ)} {i : Obj I} →
324 Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) U) i o ψ a t ] ≈ TMap t i ] 333 Sets [ Sets [ TMap (LimitNat A I Sets Γ (a0 lim) (t0 lim) U) i o ψ a t ] ≈ TMap t i ]
325 t0f=t0 {a} {t} = {!!} 334 t0f=t0 {a} {t} = {!!}