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

comparison HOD.agda @ 117:a4c97390d312

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
minimum assuption
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 26 Jun 2019 08:38:33 +0900
parents 47541e86c6ac
children 78fe704c3543
comparison
equal deleted inserted replaced
116:47541e86c6ac 117:a4c97390d312
66 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ 66 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ
67 -- contra-position of mimimulity of supermum required in Power Set Axiom 67 -- contra-position of mimimulity of supermum required in Power Set Axiom
68 sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} 68 sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n}
69 sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) 69 sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
70 -- sup-lb : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → ( ∀ {x : Ordinal {n}} → ψx o< z ) → z o< osuc ( sup-o ψ ) 70 -- sup-lb : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → ( ∀ {x : Ordinal {n}} → ψx o< z ) → z o< osuc ( sup-o ψ )
71 minimul : {n : Level } → (x : HOD {suc n} ) → ¬ (x == od∅ )→ HOD {suc n}
72 -- this should be ¬ (x == od∅ )→ ∃ ox → x ∋ Ord ox ( minimum of x )
73 x∋minimul : {n : Level } → (x : HOD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → def x ( od→ord ( minimul x ne ) )
74 minimul-1 : {n : Level } → (x : HOD {suc n} ) → ( ne : ¬ (x == od∅ ) ) → (y : HOD {suc n}) → ¬ ( def (minimul x ne) (od→ord y)) ∧ (def x (od→ord y) )
71 75
72 _∋_ : { n : Level } → ( a x : HOD {n} ) → Set n 76 _∋_ : { n : Level } → ( a x : HOD {n} ) → Set n
73 _∋_ {n} a x = def a ( od→ord x ) 77 _∋_ {n} a x = def a ( od→ord x )
74 78
75 _c<_ : { n : Level } → ( x a : HOD {n} ) → Set n 79 _c<_ : { n : Level } → ( x a : HOD {n} ) → Set n
354 ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord y} (proj2 s ) refl diso } } where 358 ; proj2 = def-subst {suc n} {_} {_} {X} {od→ord y} (proj2 s ) refl diso } } where
355 replacement : {ψ : HOD → HOD} (X x : HOD) → Replace X ψ ∋ ψ x 359 replacement : {ψ : HOD → HOD} (X x : HOD) → Replace X ψ ∋ ψ x
356 replacement {ψ} X x = sup-c< ψ {x} 360 replacement {ψ} X x = sup-c< ψ {x}
357 ∅-iso : {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 361 ∅-iso : {x : HOD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
358 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq 362 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq
359 minimul : (x : HOD {suc n} ) → ¬ (x == od∅ )→ HOD {suc n}
360 minimul x not = {!!}
361 regularity : (x : HOD) (not : ¬ (x == od∅)) → 363 regularity : (x : HOD) (not : ¬ (x == od∅)) →
362 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) 364 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
363 proj1 (regularity x not ) = {!!} 365 proj1 (regularity x not ) = x∋minimul x not
364 proj2 (regularity x not ) = record { eq→ = reg ; eq← = {!!} } where 366 proj2 (regularity x not ) = record { eq→ = lemma1 ; eq← = λ {y} d → lemma2 {y} d } where
365 reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y 367 lemma1 : {x₁ : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁ → def od∅ x₁
366 reg {y} t = {!!} 368 lemma1 {x₁} s = ⊥-elim ( minimul-1 x not (ord→od x₁) lemma3 ) where
369 lemma3 : def (minimul x not) (od→ord (ord→od x₁)) ∧ def x (od→ord (ord→od x₁))
370 lemma3 = proj1 s x₁ (proj2 s)
371 lemma2 : {x₁ : Ordinal} → def od∅ x₁ → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) x₁
372 lemma2 {y} d = ⊥-elim (empty (ord→od y) (def-subst {suc n} {_} {_} {od∅} {od→ord (ord→od y)} d refl (sym diso) ))
367 extensionality : {A B : HOD {suc n}} → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A == B 373 extensionality : {A B : HOD {suc n}} → ((z : HOD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
368 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d 374 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
369 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d 375 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
370 xx-union : {x : HOD {suc n}} → (x , x) ≡ record { def = λ z → z o< osuc (od→ord x) } 376 xx-union : {x : HOD {suc n}} → (x , x) ≡ record { def = λ z → z o< osuc (od→ord x) }
371 xx-union {x} = cong ( λ k → Ord k ) (omxx (od→ord x)) 377 xx-union {x} = cong ( λ k → Ord k ) (omxx (od→ord x))