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

comparison zf.agda @ 14:e11e95d5ddee

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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