Mercurial > hg > Members > kono > Proof > category

comparison limit-to.agda @ 495:633df882db86

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fryed1 done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Mar 2017 13:08:03 +0900
parents c257347a27f3
children 3ce21b2a671a
comparison
equal deleted inserted replaced
494:ba6a67523523 495:633df882db86
224 uniquness : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) → 224 uniquness : (d : Obj A ) (h : Hom A d a ) → ( fh=gh : A [ A [ f o h ] ≈ A [ g o h ] ] ) →
225 ( k' : Hom A d c ) 225 ( k' : Hom A d c )
226 → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ] 226 → A [ A [ e o k' ] ≈ h ] → A [ k h fh=gh ≈ k' ]
227 uniquness d h fh=gh k' ek'=h = let open ≈-Reasoning A in begin 227 uniquness d h fh=gh k' ek'=h = let open ≈-Reasoning A in begin
228 k h fh=gh 228 k h fh=gh
229 ≈⟨ limit-uniqueness (isLimit lim) k' ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩ 229 ≈⟨ limit-uniqueness (isLimit lim) ( λ{i} → uniq-nat {i} d h k' fh=gh ek'=h ) ⟩
230 k' 230 k'
231 ∎ 231 ∎
232 232
233 233
234 --- Product from Limit ( given Discrete->A functor Γ and pnat : K ->　Γ) 234 --- Product from Limit ( given Discrete->A functor Γ and pnat : K ->　Γ)
288 pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( iproduct qi ) ] ≈ (qi i) ] 288 pif=q : {q : Obj A} → ( qi : (i : I) → Hom A q (ai i) ) → ∀ { i : I } → A [ A [ ( pi i ) o ( iproduct qi ) ] ≈ (qi i) ]
289 pif=q {q} qi {i} = t0f=t (isLimit lim) {q} {pnat A S Γ qi } {i} 289 pif=q {q} qi {i} = t0f=t (isLimit lim) {q} {pnat A S Γ qi } {i}
290 ipu : {i : Obj D} → (q : Obj A) (h : Hom A q p ) → A [ A [ TMap (limit-u comp Γ) i o h ] ≈ A [ pi i o h ] ] 290 ipu : {i : Obj D} → (q : Obj A) (h : Hom A q p ) → A [ A [ TMap (limit-u comp Γ) i o h ] ≈ A [ pi i o h ] ]
291 ipu {i} q h = let open ≈-Reasoning A in refl-hom 291 ipu {i} q h = let open ≈-Reasoning A in refl-hom
292 ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ] 292 ip-uniqueness : {q : Obj A} { h : Hom A q p } → A [ iproduct ( λ (i : I) → A [ (pi i) o h ] ) ≈ h ]
293 ip-uniqueness {q} {h} = limit-uniqueness (isLimit lim) {q} {pnat A S Γ (λ i → A [ pi i o h ] )} h (ipu q h) 293 ip-uniqueness {q} {h} = limit-uniqueness (isLimit lim) {q} {pnat A S Γ (λ i → A [ pi i o h ] )} (ipu q h)
294 ipc : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } 294 ipc : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
295 → (i : I ) → A [ qi i ≈ qi' i ] → 295 → (i : I ) → A [ qi i ≈ qi' i ] →
296 A [ A [ TMap (limit-u comp Γ) i o iproduct qi' ] ≈ TMap (pnat A S Γ qi) i ] 296 A [ A [ TMap (limit-u comp Γ) i o iproduct qi' ] ≈ TMap (pnat A S Γ qi) i ]
297 ipc {q} {qi} {qi'} i qi=qi' = let open ≈-Reasoning A in begin 297 ipc {q} {qi} {qi'} i qi=qi' = let open ≈-Reasoning A in begin
298 TMap (limit-u comp Γ) i o iproduct qi' 298 TMap (limit-u comp Γ) i o iproduct qi'
307 ≈⟨⟩ 307 ≈⟨⟩
308 TMap (pnat A S Γ qi) i 308 TMap (pnat A S Γ qi) i
309 ∎ 309 ∎
310 ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) } 310 ip-cong : {q : Obj A} → { qi : (i : I) → Hom A q (ai i) } → { qi' : (i : I) → Hom A q (ai i) }
311 → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ] 311 → ( ∀ (i : I ) → A [ qi i ≈ qi' i ] ) → A [ iproduct qi ≈ iproduct qi' ]
312 ip-cong {q} {qi} {qi'} qi=qi' = limit-uniqueness (isLimit lim) {q} {pnat A S Γ qi} (iproduct qi' ) (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i)) 312 ip-cong {q} {qi} {qi'} qi=qi' = limit-uniqueness (isLimit lim) {q} {pnat A S Γ qi} (λ {i} → ipc {q} {qi} {qi'} i (qi=qi' i))