Mercurial > hg > Members > kono > Proof > ZF-in-agda

comparison HOD.agda @ 130:3849614bef18

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
new replacement axiom
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 02 Jul 2019 15:59:07 +0900
parents 2a5519dcc167
children b52683497a27
comparison
equal deleted inserted replaced
129:2a5519dcc167 130:3849614bef18
340 ; minimul = minimul 340 ; minimul = minimul
341 ; regularity = regularity 341 ; regularity = regularity
342 ; infinity∅ = infinity∅ 342 ; infinity∅ = infinity∅
343 ; infinity = λ _ → infinity 343 ; infinity = λ _ → infinity
344 ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y} 344 ; selection = λ {X} {ψ} {y} → selection {X} {ψ} {y}
345 ; replacement = replacement 345 ; reverse = ?
346 ; reverse-∈ = ?
347 ; replacement← = ?
348 ; replacement→ = ?
346 } where 349 } where
347 350
348 pair : (A B : HOD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B) 351 pair : (A B : HOD {suc n} ) → ((A , B) ∋ A) ∧ ((A , B) ∋ B)
349 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B) 352 proj1 (pair A B ) = omax-x {n} (od→ord A) (od→ord B)
350 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B) 353 proj2 (pair A B ) = omax-y {n} (od→ord A) (od→ord B)
373 sp = sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))) 376 sp = sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))
374 minsup : HOD 377 minsup : HOD
375 minsup = ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))) 378 minsup = ZFSubset (Ord a) ( ord→od ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))))
376 Ltx : {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x 379 Ltx : {n : Level} → {x t : HOD {suc n}} → t ∋ x → Ord (od→ord t) ∋ x
377 Ltx {n} {x} {t} lt = c<→o< lt 380 Ltx {n} {x} {t} lt = c<→o< lt
381 -- lemma1 hold because minsup is Ord (minα a sp)
378 lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t) 382 lemma1 : od→ord (Ord (od→ord t)) o< od→ord minsup → minsup ∋ Ord (od→ord t)
379 lemma1 lt with OrdSubset a ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x)))) 383 lemma1 lt with OrdSubset a ( sup-x (λ x → od→ord ( ZFSubset (Ord a) (ord→od x))))
380 ... | eq with subst ( λ k → ZFSubset (Ord a) k ≡ Ord (minα a sp)) Ord-ord eq 384 ... | eq with subst ( λ k → ZFSubset (Ord a) k ≡ Ord (minα a sp)) Ord-ord eq
381 ... | eq1 = def-subst {suc n} {_} {_} {minsup} {od→ord (Ord (od→ord t))} (o<→c< lt) lemma2 (sym ord-Ord) where 385 ... | eq1 = def-subst {suc n} {_} {_} {minsup} {od→ord (Ord (od→ord t))} (o<→c< lt) lemma2 (sym ord-Ord) where
382 lemma2 : Ord (od→ord (ZFSubset (Ord a) (ord→od sp))) ≡ minsup 386 lemma2 : Ord (od→ord (ZFSubset (Ord a) (ord→od sp))) ≡ minsup
389 ≡⟨ cong (λ k → Ord k) diso ⟩ 393 ≡⟨ cong (λ k → Ord k) diso ⟩
390 Ord (minα a sp) 394 Ord (minα a sp)
391 ≡⟨ sym eq1 ⟩ 395 ≡⟨ sym eq1 ⟩
392 minsup 396 minsup
393 ∎ 397 ∎
394
395 -- 398 --
396 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t 399 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
397 -- Power A is a sup of ZFSubset A t, so Power A ∋ t 400 -- Power A is a sup of ZFSubset A t, so Power A ∋ t
398 -- 401 --
399 ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t 402 ord-power← : (a : Ordinal ) (t : HOD) → ({x : HOD} → (t ∋ x → (Ord a) ∋ x)) → Def (Ord a) ∋ t
408 → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t 411 → (eq : ZFSubset (Ord a) t == t) → od→ord (ZFSubset (Ord a) (ord→od (od→ord t))) ≡ od→ord t
409 lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq )) 412 lemma1 {n} {a} {t} eq = subst (λ k → od→ord (ZFSubset (Ord a) k) ≡ od→ord t ) (sym oiso) (cong (λ k → od→ord k ) (===-≡ eq ))
410 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x))) 413 lemma : od→ord (ZFSubset (Ord a) (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset (Ord a) (ord→od x)))
411 lemma = sup-o< 414 lemma = sup-o<
412 415
416 -- Power A = Replace (Def (Ord (od→ord A))) ( λ x → A ∩ x )
413 power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x 417 power→ : ( A t : HOD) → Power A ∋ t → {x : HOD} → t ∋ x → A ∋ x
414 power→ = {!!} 418 power→ = {!!}
415 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t 419 power← : (A t : HOD) → ({x : HOD} → (t ∋ x → A ∋ x)) → Power A ∋ t
416 power← = {!!} 420 power← A t t→A = def-subst {suc n} {Replace (Def (Ord a)) ψ} {_} {Power A} {od→ord t} (sup-c< ψ {t}) lemma2 lemma1 where
421 a = od→ord A
422 ψ : HOD → HOD
423 ψ y = Def (Ord a) ∩ y
424 lemma1 : od→ord (Def (Ord a) ∩ t) ≡ od→ord t
425 lemma1 = {!!}
426 lemma2 : Ord ( sup-o ( λ x → od→ord (ψ (ord→od x )))) ≡ Power A
427 lemma2 = {!!}
417 428
418 union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n} 429 union-u : {X z : HOD {suc n}} → (U>z : Union X ∋ z ) → HOD {suc n}
419 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) ) 430 union-u {X} {z} U>z = Ord ( osuc ( od→ord z ) )
420 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z 431 union→ : (X z u : HOD) → (X ∋ u) ∧ (u ∋ z) → Union X ∋ z
421 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z )) 432 union→ X z u xx with trio< ( od→ord u ) ( osuc ( od→ord z ))