Mercurial > hg > Members > kono > Proof > ZF-in-agda
changeset 21:6d9fdd1dfa79
add transfinite
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 16 May 2019 16:47:27 +0900 |
| parents | 31626f36cd94 |
| children | 3da2c00bd24d |
| files | constructible-set.agda |
| diffstat | 1 files changed, 26 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/constructible-set.agda Thu May 16 16:08:34 2019 +0900 +++ b/constructible-set.agda Thu May 16 16:47:27 2019 +0900 @@ -35,6 +35,31 @@ open import Relation.Binary open import Relation.Binary.Core +o∅ : Ordinal +o∅ = record { lv = Zero ; ord = Φ } + +TransFinite : ( ψ : Ordinal → Set n ) + → ( ∀ (lx : Nat ) → ψ ( record { lv = Suc lx ; ord = ℵ lx } )) + → ( ∀ (lx : Nat ) → ψ ( record { lv = lx ; ord = Φ } ) ) + → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ψ ( record { lv = lx ; ord = x } ) → ψ ( record { lv = lx ; ord = OSuc x } ) ) + → ∀ (x : Ordinal) → ψ x +TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = Φ } = caseΦ lv +TransFinite ψ caseℵ caseΦ caseOSuc record { lv = lv ; ord = OSuc ord₁ } = caseOSuc lv ord₁ + ( TransFinite ψ caseℵ caseΦ caseOSuc (record { lv = lv ; ord = ord₁ } )) +TransFinite ψ caseℵ caseΦ caseOSuc record { lv = Suc lv₁ ; ord = ℵ lv₁ } = caseℵ lv₁ + +record SupR (ψ : Ordinal → Ordinal ) : Set n where + field + sup : Ordinal + smax : { x : Ordinal } → ψ x o< sup + +open SupR + +Sup : (ψ : Ordinal → Ordinal ) → SupR ψ +sup (Sup ψ) = {!!} +smax (Sup ψ) = {!!} + + ≡→¬d< : {lv : Nat} → {x : OrdinalD lv } → x d< x → ⊥ ≡→¬d< {lx} {OSuc y} (s< t) = ≡→¬d< t @@ -145,7 +170,7 @@ ZFSet = ConstructibleSet ; _∋_ = λ a b → Lift (suc (suc n)) ( a ∋ b ) ; _≈_ = _≡_ - ; ∅ = record {α = record { lv = Zero ; ord = Φ } ; constructible = λ x → Lift (suc n) ⊥ } + ; ∅ = record {α = o∅ ; constructible = λ x → Lift (suc n) ⊥ } ; _,_ = _,_ ; Union = Union ; Power = {!!}