Mercurial > hg > Members > kono > Proof > category

comparison freyd2.agda @ 642:53f2a11474ee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
on going ..
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 03 Jul 2017 08:41:01 +0900
parents c65d08d85092
children 5eb746702732
comparison
equal deleted inserted replaced
641:c65d08d85092 642:53f2a11474ee
297 limitInSets Γ lim = record { 297 limitInSets Γ lim = record {
298 limit = λ a t → ψ a t 298 limit = λ a t → ψ a t
299 ; t0f=t = λ {a t i} → t0f=t0 {a} {t} {i} 299 ; t0f=t = λ {a t i} → t0f=t0 {a} {t} {i}
300 ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t 300 ; limit-uniqueness = λ {b} {t} {f} t0f=t → limit-uniqueness0 {b} {t} {f} t0f=t
301 } where 301 } where
302 revUub : (pi : FObj U (obj (preinitialObj PI)) ) → pi ≡ (hom (preinitialObj PI) OneObj)
303 revUub _ = {!!}
304 revU' : (a : Obj (K Sets A * ↓ U))
305 → Sets [ Sets [ FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ) o hom (preinitialObj PI) ] ≈ hom a ]
306 revU' a = let open ≈-Reasoning Sets in begin
307 FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) o hom (preinitialObj PI)
308 ≈⟨ comm (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ⟩
309 hom a
310 ∎
302 revU : (a : Obj (K Sets A * ↓ U)) 311 revU : (a : Obj (K Sets A * ↓ U))
303 → Sets [ FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ) ≈ ( λ upi → hom a OneObj ) ] 312 → Sets [ FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a })) ) ≈ ( λ upi → hom a OneObj ) ]
304 revU a = extensionality Sets ( λ (pi : FObj U (obj (preinitialObj PI)) ) → ( begin 313 revU a = extensionality Sets ( λ (upi : FObj U (obj (preinitialObj PI)) ) → ( begin
305 FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) pi 314 FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) upi
306 ≡⟨ {!!} ⟩ 315 ≡⟨ {!!} ⟩
307 FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) (hom (preinitialObj PI) OneObj) 316 FMap U ( arrow (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) (hom (preinitialObj PI) OneObj)
308 ≡⟨ ≡-cong ( λ k → k OneObj ) ( comm (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) ⟩ 317 ≡⟨ ≡-cong ( λ k → k OneObj ) ( comm (SFSFMap← SFS (preinitialArrow PI {FObj (SFSF SFS) a }))) ⟩
309 hom a OneObj 318 hom a OneObj
310 ∎ ) ) where 319 ∎ ) ) where