Mercurial > hg > Members > kono > Proof > ZF-in-agda
diff zf.agda @ 14:e11e95d5ddee
separete constructible set
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Tue, 14 May 2019 03:38:26 +0900 |
parents | 2df90eb0896c |
children | 627a79e61116 |
line wrap: on
line diff
--- a/zf.agda Mon May 13 20:51:45 2019 +0900 +++ b/zf.agda Tue May 14 03:38:26 2019 +0900 @@ -121,88 +121,3 @@ -- russel with Select ( λ x → x ∋ x ) -- ... | s = {!!} -module constructible-set where - - open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ) - - open import Relation.Binary.PropositionalEquality - - data Ordinal {n : Level } : Set n where - Φ : {lv : Nat} → Ordinal {n} lv - T-suc : {lv : Nat} → Ordinal {n} lv → Ordinal lv - ℵ_ : (lv : Nat) → Ordinal (Suc lv) - - data _o<_ {n : Level } : Ordinal {n} → Ordinal {n} → Set n where - l< : {lx ly : Nat } → {x : Ordinal {n} lx } → {y : Ordinal {n} ly } → lx < ly → x o< y - Φ< : {lx : Nat} → {x : Ordinal {n} lx} → Φ {n} {lx} o< T-suc {n} {lx} x - s< : {lx : Nat} → {x : Ordinal {n} lx} → x o< T-suc {n} {lx} x - ℵΦ< : {lx : Nat} → {x : Ordinal {n} lx } → Φ {n} {lx} o< (ℵ lx) - ℵ< : {lx : Nat} → {x : Ordinal {n} lx } → T-suc {n} {lx} x o< (ℵ lx) - - _o≈_ : {n : Level } {lv : Nat } → Rel ( Ordinal {n} lv ) n - _o≈_ = {!!} - - triO : {n : Level } → {lx ly : Nat} → Trichotomous _o≈_ ( _o<_ {n} {lx} {ly} ) - triO {n} {lv} Φ y = {!!} - triO {n} {lv} (T-suc x) y = {!!} - triO {n} {.(Suc lv)} (ℵ lv) y = {!!} - - - max = Data.Nat._⊔_ - - maxα : {n : Level } → { lx ly : Nat } → Ordinal {n} lx → Ordinal {n} ly → Ordinal {n} (max lx ly) - maxα x y with x o< y - ... | t = {!!} - - -- X' = { x ∈ X | ψ x } ∪ X , Mα = ( ∪ (β < α) Mβ ) ' - - data Constructible {n : Level } {lv : Nat} ( α : Ordinal {n} lv ) : Set (suc n) where - fsub : ( ψ : Ordinal {n} lv → Set n ) → Constructible α - xself : Ordinal {n} lv → Constructible α - - record ConstructibleSet {n : Level } : Set (suc n) where - field - level : Nat - α : Ordinal {n} level - constructible : Constructible α - - open ConstructibleSet - - data _c∋_ {n : Level } : {lv lv' : Nat} {α : Ordinal {n} lv } {α' : Ordinal {n} lv' } → - Constructible {n} {lv} α → Constructible {n} {lv'} α' → Set n where - c> : {lv lv' : Nat} {α : Ordinal {n} lv } {α' : Ordinal {n} lv' } - (ta : Constructible {n} {lv} α ) ( tx : Constructible {n} {lv'} α' ) → α' o< α → ta c∋ tx - xself-fsub : {lv : Nat} {α : Ordinal {n} lv } - (ta : Ordinal {n} lv ) ( ψ : Ordinal {n} lv → Set n ) → _c∋_ {n} {_} {_} {α} {α} (xself ta ) ( fsub ψ) - fsub-fsub : {lv lv' : Nat} {α : Ordinal {n} lv } - ( ψ : Ordinal {n} lv → Set n ) ( ψ₁ : Ordinal {n} lv → Set n ) → - ( ∀ ( x : Ordinal {n} lv ) → ψ x → ψ₁ x ) → _c∋_ {n} {_} {_} {α} {α} ( fsub ψ ) ( fsub ψ₁) - - _∋_ : {n : Level} → (ConstructibleSet {n}) → (ConstructibleSet {n} ) → Set n - a ∋ x = constructible a c∋ constructible x - - data _c≈_ {n : Level } : {lv lv' : Nat} {α : Ordinal {n} lv } {α' : Ordinal {n} lv' } → - Constructible {n} {lv} α → Constructible {n} {lv'} α' → Set n where - crefl : {lv : Nat} {α : Ordinal {n} lv } → _c≈_ {n} {_} {_} {α} {α} (xself α ) (xself α ) - feq : {lv : Nat} {α : Ordinal {n} lv } - → ( ψ : Ordinal {n} lv → Set n ) ( ψ₁ : Ordinal {n} lv → Set n ) - → (∀ ( x : Ordinal {n} lv ) → ψ x ⇔ ψ₁ x ) → _c≈_ {n} {_} {_} {α} {α} ( fsub ψ ) ( fsub ψ₁) - - _≈_ : {n : Level} → (ConstructibleSet {n}) → (ConstructibleSet {n} ) → Set n - a ≈ x = constructible a c≈ constructible x - - - ConstructibleSet→ZF : {n : Level } → ZF {suc n} {n} - ConstructibleSet→ZF {n} = record { - ZFSet = ConstructibleSet - ; _∋_ = _∋_ - ; _≈_ = _≈_ - ; ∅ = record { level = Zero ; α = Φ ; constructible = xself Φ } - ; _×_ = {!!} - ; Union = {!!} - ; Power = {!!} - ; Select = {!!} - ; Replace = {!!} - ; infinite = {!!} - ; isZF = {!!} - } where