Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison HOD.agda @ 170:c96f28c3c387
...
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Fri, 19 Jul 2019 07:04:13 +0900 |
parents | acbcbd98d588 |
children | 729b80df8a8a |
comparison
equal
deleted
inserted
replaced
169:acbcbd98d588 | 170:c96f28c3c387 |
---|---|
16 record OD {n : Level} : Set (suc n) where | 16 record OD {n : Level} : Set (suc n) where |
17 field | 17 field |
18 def : (x : Ordinal {n} ) → Set n | 18 def : (x : Ordinal {n} ) → Set n |
19 | 19 |
20 open OD | 20 open OD |
21 open import Data.Unit | |
22 | 21 |
23 open Ordinal | 22 open Ordinal |
24 open _∧_ | 23 open _∧_ |
25 | 24 |
26 record _==_ {n : Level} ( a b : OD {n} ) : Set n where | 25 record _==_ {n : Level} ( a b : OD {n} ) : Set n where |
234 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α ) | 233 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α ) |
235 cseq ( Ord (od→ord (L {n} (record { lv = lx ; ord = Φ lx })))) | 234 cseq ( Ord (od→ord (L {n} (record { lv = lx ; ord = Φ lx })))) |
236 | 235 |
237 -- L0 : {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α | 236 -- L0 : {n : Level} → (α : Ordinal {suc n}) → L (osuc α) ∋ L α |
238 -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x | 237 -- L1 : {n : Level} → (α β : Ordinal {suc n}) → α o< β → ∀ (x : OD {suc n}) → L α ∋ x → L β ∋ x |
238 | |
239 -- another form of regularity | |
240 -- | |
241 {-# TERMINATING #-} | |
242 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} | |
243 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) | |
244 → (x : OD {suc n} ) → ψ x | |
245 ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc) where | |
246 ε-induction-ord : ( ox : Ordinal {suc n} ) {oy : Ordinal {suc n} } → oy o< ox → ψ (ord→od oy) | |
247 ε-induction-ord record { lv = Zero ; ord = (Φ 0) } (case1 ()) | |
248 ε-induction-ord record { lv = Zero ; ord = (Φ 0) } (case2 ()) | |
249 ε-induction-ord record { lv = lx ; ord = (OSuc lx ox) } {oy} y<x = | |
250 ind {ord→od oy} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord (record { lv = lx ; ord = ox} ) (lemma y lt ))) where | |
251 lemma : (y : OD) → ord→od oy ∋ y → od→ord y o< record { lv = lx ; ord = ox } | |
252 lemma y lt with osuc-≡< y<x | |
253 lemma y lt | case1 refl = o<-subst (c<→o< lt) refl diso | |
254 lemma y lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1 | |
255 ε-induction-ord record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } {record { lv = ly ; ord = oy }} (case1 (s≤s x)) with <-cmp lx ly | |
256 ... | tri< a ¬b ¬c = ⊥-elim (lemma a x ) where | |
257 lemma : {lx ly : Nat} → Suc lx ≤ ly → ly ≤ lx → ⊥ | |
258 lemma (s≤s lt1) (s≤s lt2) = lemma lt1 lt2 | |
259 ... | tri≈ ¬a refl ¬c = ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso ? | |
260 ... | tri> ¬a ¬b c = ε-induction-ord record { lv = lx ; ord = (Φ lx) } (case1 c) | |
261 | |
239 | 262 |
240 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} | 263 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} |
241 OD→ZF {n} = record { | 264 OD→ZF {n} = record { |
242 ZFSet = OD {suc n} | 265 ZFSet = OD {suc n} |
243 ; _∋_ = _∋_ | 266 ; _∋_ = _∋_ |
465 choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD | 488 choice-func : (X : OD {suc n} ) → {x : OD } → ¬ ( x == od∅ ) → ( X ∋ x ) → OD |
466 choice-func X {x} not X∋x = minimul x not | 489 choice-func X {x} not X∋x = minimul x not |
467 choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A | 490 choice : (X : OD {suc n} ) → {A : OD } → ( X∋A : X ∋ A ) → (not : ¬ ( A == od∅ )) → A ∋ choice-func X not X∋A |
468 choice X {A} X∋A not = x∋minimul A not | 491 choice X {A} X∋A not = x∋minimul A not |
469 | 492 |
470 -- another form of regularity | |
471 -- | |
472 ε-induction : {n m : Level} { ψ : OD {suc n} → Set m} | |
473 → ( {x : OD {suc n} } → ({ y : OD {suc n} } → x ∋ y → ψ y ) → ψ x ) | |
474 → (x : OD {suc n} ) → ψ x | |
475 ε-induction {n} {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (osuc (od→ord x)) <-osuc) where | |
476 ε-induction-ord : ( ox : Ordinal {suc n} ) {oy : Ordinal {suc n} } → oy o< ox → ψ (ord→od oy) | |
477 ε-induction-ord ox = TransFinite {suc n} {suc n ⊔ m} {λ z → {oy : Ordinal {suc n} } → oy o< z → ψ (ord→od oy) } lemma1 lemma2 ox where | |
478 lemma1 : (lx : Nat) {oy : Ordinal} → oy o< record { lv = lx ; ord = Φ lx } → ψ (ord→od oy) | |
479 lemma1 Zero {oy} (case1 ()) | |
480 lemma1 Zero {oy} (case2 ()) | |
481 lemma1 (Suc lx) {record { lv = Zero ; ord = Φ 0 }} (case1 (s≤s z≤n)) = {!!} | |
482 lemma1 (Suc lx) {record { lv = Zero ; ord = OSuc 0 oy }} (case1 (s≤s z≤n)) = {!!} | |
483 lemma1 (Suc (Suc lx)) {record { lv = Suc ly ; ord = Φ (Suc ly) }} (case1 (s≤s (s≤s x))) = {!!} | |
484 lemma1 (Suc (Suc lx)) {record { lv = Suc ly ; ord = OSuc (Suc ly) oy }} (case1 (s≤s (s≤s x))) = {!!} | |
485 lemma2 : (lx : Nat) (x₁ : OrdinalD lx) → | |
486 ({oy : Ordinal} → oy o< record { lv = lx ; ord = x₁ } → ψ (ord→od oy)) → | |
487 {oy : Ordinal} → oy o< record { lv = lx ; ord = OSuc lx x₁ } → ψ (ord→od oy) | |
488 lemma2 lx x1 p lt = ind ( λ {y} lty → subst (λ k → ψ k) oiso (p {!!} )) | |
489 |