Mercurial > hg > Members > kono > Proof > ZF-in-agda
comparison 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 |
comparison
equal
deleted
inserted
replaced
11:2df90eb0896c | 14:e11e95d5ddee |
---|---|
119 | 119 |
120 -- russel : Select ( λ x → x ∋ x ) ≈ ∅ | 120 -- russel : Select ( λ x → x ∋ x ) ≈ ∅ |
121 -- russel with Select ( λ x → x ∋ x ) | 121 -- russel with Select ( λ x → x ∋ x ) |
122 -- ... | s = {!!} | 122 -- ... | s = {!!} |
123 | 123 |
124 module constructible-set where | |
125 | |
126 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ) | |
127 | |
128 open import Relation.Binary.PropositionalEquality | |
129 | |
130 data Ordinal {n : Level } : Set n where | |
131 Φ : {lv : Nat} → Ordinal {n} lv | |
132 T-suc : {lv : Nat} → Ordinal {n} lv → Ordinal lv | |
133 ℵ_ : (lv : Nat) → Ordinal (Suc lv) | |
134 | |
135 data _o<_ {n : Level } : Ordinal {n} → Ordinal {n} → Set n where | |
136 l< : {lx ly : Nat } → {x : Ordinal {n} lx } → {y : Ordinal {n} ly } → lx < ly → x o< y | |
137 Φ< : {lx : Nat} → {x : Ordinal {n} lx} → Φ {n} {lx} o< T-suc {n} {lx} x | |
138 s< : {lx : Nat} → {x : Ordinal {n} lx} → x o< T-suc {n} {lx} x | |
139 ℵΦ< : {lx : Nat} → {x : Ordinal {n} lx } → Φ {n} {lx} o< (ℵ lx) | |
140 ℵ< : {lx : Nat} → {x : Ordinal {n} lx } → T-suc {n} {lx} x o< (ℵ lx) | |
141 | |
142 _o≈_ : {n : Level } {lv : Nat } → Rel ( Ordinal {n} lv ) n | |
143 _o≈_ = {!!} | |
144 | |
145 triO : {n : Level } → {lx ly : Nat} → Trichotomous _o≈_ ( _o<_ {n} {lx} {ly} ) | |
146 triO {n} {lv} Φ y = {!!} | |
147 triO {n} {lv} (T-suc x) y = {!!} | |
148 triO {n} {.(Suc lv)} (ℵ lv) y = {!!} | |
149 | |
150 | |
151 max = Data.Nat._⊔_ | |
152 | |
153 maxα : {n : Level } → { lx ly : Nat } → Ordinal {n} lx → Ordinal {n} ly → Ordinal {n} (max lx ly) | |
154 maxα x y with x o< y | |
155 ... | t = {!!} | |
156 | |
157 -- X' = { x ∈ X | ψ x } ∪ X , Mα = ( ∪ (β < α) Mβ ) ' | |
158 | |
159 data Constructible {n : Level } {lv : Nat} ( α : Ordinal {n} lv ) : Set (suc n) where | |
160 fsub : ( ψ : Ordinal {n} lv → Set n ) → Constructible α | |
161 xself : Ordinal {n} lv → Constructible α | |
162 | |
163 record ConstructibleSet {n : Level } : Set (suc n) where | |
164 field | |
165 level : Nat | |
166 α : Ordinal {n} level | |
167 constructible : Constructible α | |
168 | |
169 open ConstructibleSet | |
170 | |
171 data _c∋_ {n : Level } : {lv lv' : Nat} {α : Ordinal {n} lv } {α' : Ordinal {n} lv' } → | |
172 Constructible {n} {lv} α → Constructible {n} {lv'} α' → Set n where | |
173 c> : {lv lv' : Nat} {α : Ordinal {n} lv } {α' : Ordinal {n} lv' } | |
174 (ta : Constructible {n} {lv} α ) ( tx : Constructible {n} {lv'} α' ) → α' o< α → ta c∋ tx | |
175 xself-fsub : {lv : Nat} {α : Ordinal {n} lv } | |
176 (ta : Ordinal {n} lv ) ( ψ : Ordinal {n} lv → Set n ) → _c∋_ {n} {_} {_} {α} {α} (xself ta ) ( fsub ψ) | |
177 fsub-fsub : {lv lv' : Nat} {α : Ordinal {n} lv } | |
178 ( ψ : Ordinal {n} lv → Set n ) ( ψ₁ : Ordinal {n} lv → Set n ) → | |
179 ( ∀ ( x : Ordinal {n} lv ) → ψ x → ψ₁ x ) → _c∋_ {n} {_} {_} {α} {α} ( fsub ψ ) ( fsub ψ₁) | |
180 | |
181 _∋_ : {n : Level} → (ConstructibleSet {n}) → (ConstructibleSet {n} ) → Set n | |
182 a ∋ x = constructible a c∋ constructible x | |
183 | |
184 data _c≈_ {n : Level } : {lv lv' : Nat} {α : Ordinal {n} lv } {α' : Ordinal {n} lv' } → | |
185 Constructible {n} {lv} α → Constructible {n} {lv'} α' → Set n where | |
186 crefl : {lv : Nat} {α : Ordinal {n} lv } → _c≈_ {n} {_} {_} {α} {α} (xself α ) (xself α ) | |
187 feq : {lv : Nat} {α : Ordinal {n} lv } | |
188 → ( ψ : Ordinal {n} lv → Set n ) ( ψ₁ : Ordinal {n} lv → Set n ) | |
189 → (∀ ( x : Ordinal {n} lv ) → ψ x ⇔ ψ₁ x ) → _c≈_ {n} {_} {_} {α} {α} ( fsub ψ ) ( fsub ψ₁) | |
190 | |
191 _≈_ : {n : Level} → (ConstructibleSet {n}) → (ConstructibleSet {n} ) → Set n | |
192 a ≈ x = constructible a c≈ constructible x | |
193 | |
194 | |
195 ConstructibleSet→ZF : {n : Level } → ZF {suc n} {n} | |
196 ConstructibleSet→ZF {n} = record { | |
197 ZFSet = ConstructibleSet | |
198 ; _∋_ = _∋_ | |
199 ; _≈_ = _≈_ | |
200 ; ∅ = record { level = Zero ; α = Φ ; constructible = xself Φ } | |
201 ; _×_ = {!!} | |
202 ; Union = {!!} | |
203 ; Power = {!!} | |
204 ; Select = {!!} | |
205 ; Replace = {!!} | |
206 ; infinite = {!!} | |
207 ; isZF = {!!} | |
208 } where |