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

comparison ordinal-definable.agda @ 111:1daa1d24348c

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 20 Jun 2019 13:18:18 +0900
parents dab56d357fa3
children c42352a7ee07
comparison
equal deleted inserted replaced
109:dab56d357fa3 111:1daa1d24348c
64 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x 64 oiso : {n : Level} {x : OD {n}} → ord→od ( od→ord x ) ≡ x
65 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x 65 diso : {n : Level} {x : Ordinal {n}} → od→ord ( ord→od x ) ≡ x
66 -- supermum as Replacement Axiom 66 -- supermum as Replacement Axiom
67 sup-o : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} 67 sup-o : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n}
68 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ 68 sup-o< : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → ∀ {x : Ordinal {n}} → ψ x o< sup-o ψ
69 -- a property of supermum required in Power Set Axiom 69 -- contra-position of mimimulity of supermum required in Power Set Axiom
70 sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n} 70 sup-x : {n : Level } → ( Ordinal {n} → Ordinal {n}) → Ordinal {n}
71 sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ)) 71 sup-lb : {n : Level } → { ψ : Ordinal {n} → Ordinal {n}} → {z : Ordinal {n}} → z o< sup-o ψ → z o< osuc (ψ (sup-x ψ))
72 -- sup-lb : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → ( ∀ {x : Ordinal {n}} → ψx o< z ) → z o< osuc ( sup-o ψ ) 72 -- sup-lb : {n : Level } → ( ψ : Ordinal {n} → Ordinal {n}) → ( ∀ {x : Ordinal {n}} → ψx o< z ) → z o< osuc ( sup-o ψ )
73 73
74 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n 74 _∋_ : { n : Level } → ( a x : OD {n} ) → Set n
112 ... | t with t (case2 (s< s<refl ) ) 112 ... | t with t (case2 (s< s<refl ) )
113 c3 lx (OSuc .lx x₁) d not | t | () 113 c3 lx (OSuc .lx x₁) d not | t | ()
114 114
115 transitive : {n : Level } { z y x : OD {suc n} } → z ∋ y → y ∋ x → z ∋ x 115 transitive : {n : Level } { z y x : OD {suc n} } → z ∋ y → y ∋ x → z ∋ x
116 transitive {n} {z} {y} {x} z∋y x∋y with ordtrans ( c<→o< {suc n} {x} {y} x∋y ) ( c<→o< {suc n} {y} {z} z∋y ) 116 transitive {n} {z} {y} {x} z∋y x∋y with ordtrans ( c<→o< {suc n} {x} {y} x∋y ) ( c<→o< {suc n} {y} {z} z∋y )
117 ... | t = lemma0 (lemma t) where 117 ... | t = otrans z z∋y (c<→o< {suc n} {x} {y} x∋y )
118 lemma : ( od→ord x ) o< ( od→ord z ) → def ( ord→od ( od→ord z )) ( od→ord x)
119 lemma xo<z = {!!} -- o<→c< xo<z
120 lemma0 : def ( ord→od ( od→ord z )) ( od→ord x) → def z (od→ord x)
121 lemma0 dz = def-subst {suc n} { ord→od ( od→ord z )} { od→ord x} dz (oiso) refl
122 118
123 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where 119 record Minimumo {n : Level } (x : Ordinal {n}) : Set (suc n) where
124 field 120 field
125 mino : Ordinal {n} 121 mino : Ordinal {n}
126 min<x : mino o< x 122 min<x : mino o< x
160 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x 156 >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x
161 157
162 c≤-refl : {n : Level} → ( x : OD {n} ) → x c≤ x 158 c≤-refl : {n : Level} → ( x : OD {n} ) → x c≤ x
163 c≤-refl x = case1 refl 159 c≤-refl x = case1 refl
164 160
165 o<→o> : {n : Level} → { x y : OD {n} } → (x == y) → (od→ord x ) o< ( od→ord y) → ⊥
166 o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case1 lt) with
167 yx (def-subst {n} {ord→od (od→ord y)} {od→ord x} {!!} oiso refl )
168 ... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx )
169 ... | ()
170 o<→o> {n} {x} {y} record { eq→ = xy ; eq← = yx } (case2 lt) with
171 yx (def-subst {n} {ord→od (od→ord y)} {od→ord x} {!!} oiso refl )
172 ... | oyx with o<¬≡ (od→ord x) (od→ord x) refl (c<→o< oyx )
173 ... | ()
174
175 ==→o≡ : {n : Level} → { x y : Ordinal {suc n} } → ord→od x == ord→od y → x ≡ y
176 ==→o≡ {n} {x} {y} eq with trio< {n} x y
177 ==→o≡ {n} {x} {y} eq | tri< a ¬b ¬c = ⊥-elim ( o<→o> eq (o<-subst a (sym ord-iso) (sym ord-iso )))
178 ==→o≡ {n} {x} {y} eq | tri≈ ¬a b ¬c = b
179 ==→o≡ {n} {x} {y} eq | tri> ¬a ¬b c = ⊥-elim ( o<→o> (eq-sym eq) (o<-subst c (sym ord-iso) (sym ord-iso )))
180
181 ≡-def : {n : Level} → { x : Ordinal {suc n} } → x ≡ od→ord (Ord x)
182 ≡-def {n} {x} = ==→o≡ {n} (subst (λ k → ord→od x == k ) (sym oiso) lemma ) where
183 lemma : ord→od x == record { def = λ z → z o< x }
184 eq→ lemma {w} z = subst₂ (λ k j → k o< j ) diso refl (subst (λ k → (od→ord ( ord→od w)) o< k ) diso t ) where
185 t : (od→ord ( ord→od w)) o< (od→ord (ord→od x))
186 t = c<→o< {suc n} {ord→od w} {ord→od x} (def-subst {suc n} {_} {_} {ord→od x} {_} z refl (sym diso))
187 eq← lemma {w} z = def-subst {suc n} {_} {_} {ord→od x} {w} {!!} refl refl
188
189 od≡-def : {n : Level} → { x : Ordinal {suc n} } → ord→od x ≡ record { def = λ z → z o< x }
190 od≡-def {n} {x} = subst (λ k → ord→od x ≡ k ) oiso (cong ( λ k → ord→od k ) (≡-def {n} {x} ))
191
192 ==→o≡1 : {n : Level} → { x y : OD {suc n} } → x == y → od→ord x ≡ od→ord y
193 ==→o≡1 eq = ==→o≡ (subst₂ (λ k j → k == j ) (sym oiso) (sym oiso) eq )
194
195 ==-def-l : {n : Level } {x y : Ordinal {suc n} } { z : OD {suc n} }→ (ord→od x == ord→od y) → def z x → def z y
196 ==-def-l {n} {x} {y} {z} eq z>x = subst ( λ k → def z k ) (==→o≡ eq) z>x
197
198 ==-def-r : {n : Level } {x y : OD {suc n} } { z : Ordinal {suc n} }→ (x == y) → def x z → def y z
199 ==-def-r {n} {x} {y} {z} eq z>x = subst (λ k → def k z ) (subst₂ (λ j k → j ≡ k ) oiso oiso (cong (λ k → ord→od k) (==→o≡1 eq))) z>x
200
201 ∋→o< : {n : Level} → { a x : OD {suc n} } → a ∋ x → od→ord x o< od→ord a 161 ∋→o< : {n : Level} → { a x : OD {suc n} } → a ∋ x → od→ord x o< od→ord a
202 ∋→o< {n} {a} {x} lt = t where 162 ∋→o< {n} {a} {x} lt = t where
203 t : (od→ord x) o< (od→ord a) 163 t : (od→ord x) o< (od→ord a)
204 t = c<→o< {suc n} {x} {a} lt 164 t = c<→o< {suc n} {x} {a} lt
205
206 o<∋→ : {n : Level} → { a x : OD {suc n} } → od→ord x o< od→ord a → a ∋ x
207 o<∋→ {n} {a} {x} lt = subst₂ (λ k j → def k j ) oiso refl t where
208 t : def (ord→od (od→ord a)) (od→ord x)
209 t = {!!} -- o<→c< {suc n} {od→ord x} {od→ord a} lt
210 165
211 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n} 166 o∅≡od∅ : {n : Level} → ord→od (o∅ {suc n}) ≡ od∅ {suc n}
212 o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} )) 167 o∅≡od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (od∅ {suc n} ))
213 o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where 168 o∅≡od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
214 lemma : o∅ {suc n } o< (od→ord (od∅ {suc n} )) → ⊥ 169 lemma : o∅ {suc n } o< (od→ord (od∅ {suc n} )) → ⊥
220 ord-od∅ : {n : Level} → o∅ {suc n} ≡ od→ord (Ord (o∅ {suc n})) 175 ord-od∅ : {n : Level} → o∅ {suc n} ≡ od→ord (Ord (o∅ {suc n}))
221 ord-od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (Ord (o∅ {suc n}))) 176 ord-od∅ {n} with trio< {n} (o∅ {suc n}) (od→ord (Ord (o∅ {suc n})))
222 ord-od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where 177 ord-od∅ {n} | tri< a ¬b ¬c = ⊥-elim (lemma a) where
223 lemma : o∅ {suc n } o< (od→ord (Ord (o∅ {suc n}))) → ⊥ 178 lemma : o∅ {suc n } o< (od→ord (Ord (o∅ {suc n}))) → ⊥
224 lemma lt with o<→c< lt 179 lemma lt with o<→c< lt
225 lemma lt | t = o<¬≡ _ _ refl t 180 lemma lt | t = o<¬≡ refl t
226 ord-od∅ {n} | tri≈ ¬a b ¬c = b 181 ord-od∅ {n} | tri≈ ¬a b ¬c = b
227 ord-od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c) 182 ord-od∅ {n} | tri> ¬a ¬b c = ⊥-elim (¬x<0 c)
228 183
229
230 o<→¬== : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (x == y )
231 o<→¬== {n} {x} {y} lt eq = o<→o> eq lt
232
233 o<→¬c> : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (y c< x ) 184 o<→¬c> : {n : Level} → { x y : OD {n} } → (od→ord x ) o< ( od→ord y) → ¬ (y c< x )
234 o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where 185 o<→¬c> {n} {x} {y} olt clt = o<> olt (c<→o< clt ) where
235 186
236 o≡→¬c< : {n : Level} → { x y : OD {n} } → (od→ord x ) ≡ ( od→ord y) → ¬ x c< y 187 o≡→¬c< : {n : Level} → { x y : OD {n} } → (od→ord x ) ≡ ( od→ord y) → ¬ x c< y
237 o≡→¬c< {n} {x} {y} oeq lt = o<¬≡ (od→ord x) (od→ord y) (orefl oeq ) (c<→o< lt) 188 o≡→¬c< {n} {x} {y} oeq lt = o<¬≡ (orefl oeq ) (c<→o< lt)
238
239 tri-c< : {n : Level} → Trichotomous _==_ (_c<_ {suc n})
240 tri-c< {n} x y with trio< {n} (od→ord x) (od→ord y)
241 tri-c< {n} x y | tri< a ¬b ¬c = tri< (def-subst {!!} oiso refl) (o<→¬== a) ( o<→¬c> a )
242 tri-c< {n} x y | tri≈ ¬a b ¬c = tri≈ (o≡→¬c< b) (ord→== b) (o≡→¬c< (sym b))
243 tri-c< {n} x y | tri> ¬a ¬b c = tri> ( o<→¬c> c) (λ eq → o<→¬== c (eq-sym eq ) ) (def-subst {!!} oiso refl)
244
245 c<> : {n : Level } { x y : OD {suc n}} → x c< y → y c< x → ⊥
246 c<> {n} {x} {y} x<y y<x with tri-c< x y
247 c<> {n} {x} {y} x<y y<x | tri< a ¬b ¬c = ¬c y<x
248 c<> {n} {x} {y} x<y y<x | tri≈ ¬a b ¬c = o<→o> b ( c<→o< x<y )
249 c<> {n} {x} {y} x<y y<x | tri> ¬a ¬b c = ¬a x<y
250 189
251 ∅0 : {n : Level} → record { def = λ x → Lift n ⊥ ; otrans = λ () } == od∅ {n} 190 ∅0 : {n : Level} → record { def = λ x → Lift n ⊥ ; otrans = λ () } == od∅ {n}
252 eq→ ∅0 {w} (lift ()) 191 eq→ ∅0 {w} (lift ())
253 eq← ∅0 {w} (case1 ()) 192 eq← ∅0 {w} (case1 ())
254 eq← ∅0 {w} (case2 ()) 193 eq← ∅0 {w} (case2 ())
255 194
256 ∅< : {n : Level} → { x y : OD {n} } → def x (od→ord y ) → ¬ ( x == od∅ {n} ) 195 ∅< : {n : Level} → { x y : OD {n} } → def x (od→ord y ) → ¬ ( x == od∅ {n} )
257 ∅< {n} {x} {y} d eq with eq→ (eq-trans eq (eq-sym ∅0) ) d 196 ∅< {n} {x} {y} d eq with eq→ (eq-trans eq (eq-sym ∅0) ) d
258 ∅< {n} {x} {y} d eq | lift () 197 ∅< {n} {x} {y} d eq | lift ()
259 198
260 ∅6 : {n : Level} → { x : OD {suc n} } → ¬ ( x ∋ x ) -- no Russel paradox 199 -- ∅6 : {n : Level} → { x : OD {suc n} } → ¬ ( x ∋ x ) -- no Russel paradox
261 ∅6 {n} {x} x∋x = c<> {n} {x} {x} x∋x x∋x 200 -- ∅6 {n} {x} x∋x = c<> {n} {x} {x} x∋x x∋x
262 201
263 def-iso : {n : Level} {A B : OD {n}} {x y : Ordinal {n}} → x ≡ y → (def A y → def B y) → def A x → def B x 202 def-iso : {n : Level} {A B : OD {n}} {x y : Ordinal {n}} → x ≡ y → (def A y → def B y) → def A x → def B x
264 def-iso refl t = t 203 def-iso refl t = t
265
266 is-∋ : {n : Level} → ( x y : OD {suc n} ) → Dec ( x ∋ y )
267 is-∋ {n} x y with tri-c< x y
268 is-∋ {n} x y | tri< a ¬b ¬c = no ¬c
269 is-∋ {n} x y | tri≈ ¬a b ¬c = no ¬c
270 is-∋ {n} x y | tri> ¬a ¬b c = yes c
271 204
272 is-o∅ : {n : Level} → ( x : Ordinal {suc n} ) → Dec ( x ≡ o∅ {suc n} ) 205 is-o∅ : {n : Level} → ( x : Ordinal {suc n} ) → Dec ( x ≡ o∅ {suc n} )
273 is-o∅ {n} record { lv = Zero ; ord = (Φ .0) } = yes refl 206 is-o∅ {n} record { lv = Zero ; ord = (Φ .0) } = yes refl
274 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () ) 207 is-o∅ {n} record { lv = Zero ; ord = (OSuc .0 ord₁) } = no ( λ () )
275 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ()) 208 is-o∅ {n} record { lv = (Suc lv₁) ; ord = ord } = no (λ())
294 L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n} 227 L : {n : Level} → (α : Ordinal {suc n}) → OD {suc n}
295 L {n} record { lv = Zero ; ord = (Φ .0) } = od∅ 228 L {n} record { lv = Zero ; ord = (Φ .0) } = od∅
296 L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) ) 229 L {n} record { lv = lx ; ord = (OSuc lv ox) } = Def ( L {n} ( record { lv = lx ; ord = ox } ) )
297 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α ) 230 L {n} record { lv = (Suc lx) ; ord = (Φ (Suc lx)) } = -- Union ( L α )
298 record { def = λ y → osuc y o< (od→ord (L {n} (record { lv = lx ; ord = Φ lx }) )) ; otrans = {!!} } 231 record { def = λ y → osuc y o< (od→ord (L {n} (record { lv = lx ; ord = Φ lx }) )) ; otrans = {!!} }
232
233 omega : { n : Level } → Ordinal {n}
234 omega = record { lv = Suc Zero ; ord = Φ 1 }
299 235
300 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n} 236 OD→ZF : {n : Level} → ZF {suc (suc n)} {suc n}
301 OD→ZF {n} = record { 237 OD→ZF {n} = record {
302 ZFSet = OD {suc n} 238 ZFSet = OD {suc n}
303 ; _∋_ = _∋_ 239 ; _∋_ = _∋_
306 ; _,_ = _,_ 242 ; _,_ = _,_
307 ; Union = Union 243 ; Union = Union
308 ; Power = Power 244 ; Power = Power
309 ; Select = Select 245 ; Select = Select
310 ; Replace = Replace 246 ; Replace = Replace
311 ; infinite = ord→od ( record { lv = Suc Zero ; ord = Φ 1 } ) 247 ; infinite = Ord omega
312 ; isZF = isZF 248 ; isZF = isZF
313 } where 249 } where
314 Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n} 250 Replace : OD {suc n} → (OD {suc n} → OD {suc n} ) → OD {suc n}
315 Replace X ψ = sup-od ψ 251 Replace X ψ = sup-od ψ
316 Select : OD {suc n} → (OD {suc n} → Set (suc n) ) → OD {suc n} 252 Select : (X : OD {suc n} ) → ((x : OD {suc n} ) → X ∋ x → Set (suc n) ) → OD {suc n}
317 Select X ψ = record { def = λ x → ( def X x ∧ ψ ( Ord x )) ; otrans = {!!} } 253 Select X ψ = record { def = λ x → ( (d : def X x ) → ψ (ord→od x) (subst (λ k → def X k ) (sym diso) d)) ; otrans = lemma } where
254 lemma : {x y : Ordinal} → ((d : def X x) → ψ (ord→od x) (subst (def X) (sym diso) d)) →
255 y o< x → (d : def X y) → ψ (ord→od y) (subst (def X) (sym diso) d)
256 lemma {x} {y} f y<x d = {!!}
318 _,_ : OD {suc n} → OD {suc n} → OD {suc n} 257 _,_ : OD {suc n} → OD {suc n} → OD {suc n}
319 x , y = Ord (omax (od→ord x) (od→ord y)) 258 x , y = Ord (omax (od→ord x) (od→ord y))
320 Union : OD {suc n} → OD {suc n} 259 Union : OD {suc n} → OD {suc n}
321 Union U = record { def = λ y → osuc y o< (od→ord U) ; otrans = {!!} } 260 Union U = record { def = λ y → osuc y o< (od→ord U) ; otrans = {!!} }
322 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x ) 261 -- power : ∀ X ∃ A ∀ t ( t ∈ A ↔ ( ∀ {x} → t ∋ x → X ∋ x )
326 _∈_ : ( A B : ZFSet ) → Set (suc n) 265 _∈_ : ( A B : ZFSet ) → Set (suc n)
327 A ∈ B = B ∋ A 266 A ∈ B = B ∋ A
328 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n) 267 _⊆_ : ( A B : ZFSet ) → ∀{ x : ZFSet } → Set (suc n)
329 _⊆_ A B {x} = A ∋ x → B ∋ x 268 _⊆_ A B {x} = A ∋ x → B ∋ x
330 _∩_ : ( A B : ZFSet ) → ZFSet 269 _∩_ : ( A B : ZFSet ) → ZFSet
331 A ∩ B = Select (A , B) ( λ x → ( A ∋ x ) ∧ (B ∋ x) ) 270 A ∩ B = Select (A , B) ( λ x d → ( A ∋ x ) ∧ (B ∋ x) )
332 -- _∪_ : ( A B : ZFSet ) → ZFSet 271 -- _∪_ : ( A B : ZFSet ) → ZFSet
333 -- A ∪ B = Select (A , B) ( λ x → (A ∋ x) ∨ ( B ∋ x ) ) 272 -- A ∪ B = Select (A , B) ( λ x → (A ∋ x) ∨ ( B ∋ x ) )
334 ｛_｝ : ZFSet → ZFSet 273 ｛_｝ : ZFSet → ZFSet
335 ｛ x ｝ = ( x , x ) 274 ｛ x ｝ = ( x , x )
336 275
337 infixr 200 _∈_ 276 infixr 200 _∈_
338 -- infixr 230 _∩_ _∪_ 277 -- infixr 230 _∩_ _∪_
339 infixr 220 _⊆_ 278 infixr 220 _⊆_
340 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (ord→od ( record { lv = Suc Zero ; ord = Φ 1} )) 279 isZF : IsZF (OD {suc n}) _∋_ _==_ od∅ _,_ Union Power Select Replace (Ord omega)
341 isZF = record { 280 isZF = record {
342 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans } 281 isEquivalence = record { refl = eq-refl ; sym = eq-sym; trans = eq-trans }
343 ; pair = pair 282 ; pair = pair
344 ; union-u = λ _ z _ → csuc z 283 ; union-u = λ _ z _ → csuc z
345 ; union→ = union→ 284 ; union→ = union→
377 minsup = ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) 316 minsup = ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x)))))
378 lemma-t : csuc minsup ∋ t 317 lemma-t : csuc minsup ∋ t
379 lemma-t = {!!} -- o<→c< (o<-subst (sup-lb (o<-subst (c<→o< P∋t) refl diso )) refl refl ) 318 lemma-t = {!!} -- o<→c< (o<-subst (sup-lb (o<-subst (c<→o< P∋t) refl diso )) refl refl )
380 lemma-s : ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) ∋ x 319 lemma-s : ZFSubset A ( ord→od ( sup-x (λ x → od→ord ( ZFSubset A (ord→od x))))) ∋ x
381 lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) refl diso ) 320 lemma-s with osuc-≡< ( o<-subst (c<→o< lemma-t ) refl diso )
382 lemma-s | case1 eq = def-subst ( ==-def-r (o≡→== eq) (subst (λ k → def k (od→ord x)) (sym oiso) t∋x ) ) oiso refl 321 lemma-s | case1 eq = def-subst {!!} oiso refl
383 lemma-s | case2 lt = transitive {n} {minsup} {t} {x} (def-subst {!!} oiso refl ) t∋x 322 lemma-s | case2 lt = transitive {n} {minsup} {t} {x} (def-subst {!!} oiso refl ) t∋x
384 -- 323 --
385 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t 324 -- we have t ∋ x → A ∋ x means t is a subset of A, that is ZFSubset A t == t
386 -- Power A is a sup of ZFSubset A t, so Power A ∋ t 325 -- Power A is a sup of ZFSubset A t, so Power A ∋ t
387 -- 326 --
391 lemma-eq : ZFSubset A t == t 330 lemma-eq : ZFSubset A t == t
392 eq→ lemma-eq {z} w = proj2 w 331 eq→ lemma-eq {z} w = proj2 w
393 eq← lemma-eq {z} w = record { proj2 = w ; 332 eq← lemma-eq {z} w = record { proj2 = w ;
394 proj1 = def-subst {suc n} {_} {_} {A} {z} ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso } 333 proj1 = def-subst {suc n} {_} {_} {A} {z} ( t→A (def-subst {suc n} {_} {_} {t} {od→ord (ord→od z)} w refl (sym diso) )) refl diso }
395 lemma1 : od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t 334 lemma1 : od→ord (ZFSubset A (ord→od (od→ord t))) ≡ od→ord t
396 lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) (==→o≡1 (lemma-eq)) 335 lemma1 = subst (λ k → od→ord (ZFSubset A k) ≡ od→ord t ) (sym oiso) {!!}
397 lemma : od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x))) 336 lemma : od→ord (ZFSubset A (ord→od (od→ord t)) ) o< sup-o (λ x → od→ord (ZFSubset A (ord→od x)))
398 lemma = sup-o< 337 lemma = sup-o<
399 union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → csuc z ∋ z 338 union-lemma-u : {X z : OD {suc n}} → (U>z : Union X ∋ z ) → csuc z ∋ z
400 union-lemma-u {X} {z} U>z = lemma <-osuc where 339 union-lemma-u {X} {z} U>z = lemma <-osuc where
401 lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz 340 lemma : {oz ooz : Ordinal {suc n}} → oz o< ooz → def (ord→od ooz) oz
410 union→ X y u xx | tri> ¬a ¬b c = ordtrans {suc n} {osuc ( od→ord y )} {od→ord u} {od→ord X} c ( c<→o< (proj1 xx )) 349 union→ X y u xx | tri> ¬a ¬b c = ordtrans {suc n} {osuc ( od→ord y )} {od→ord u} {od→ord X} c ( c<→o< (proj1 xx ))
411 union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ csuc z) ∧ (csuc z ∋ z ) 350 union← : (X z : OD) (X∋z : Union X ∋ z) → (X ∋ csuc z) ∧ (csuc z ∋ z )
412 union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} {!!} oiso (sym diso) ; proj2 = union-lemma-u X∋z } 351 union← X z X∋z = record { proj1 = def-subst {suc n} {_} {_} {X} {od→ord (csuc z )} {!!} oiso (sym diso) ; proj2 = union-lemma-u X∋z }
413 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y 352 ψiso : {ψ : OD {suc n} → Set (suc n)} {x y : OD {suc n}} → ψ x → x ≡ y → ψ y
414 ψiso {ψ} t refl = t 353 ψiso {ψ} t refl = t
415 selection : {ψ : OD → Set (suc n)} {X y : OD} → ((X ∋ y) ∧ ψ y) ⇔ (Select X ψ ∋ y) 354 selection : {X : OD } {ψ : (x : OD ) → x ∈ X → Set (suc n)} {y : OD} → ((d : X ∋ y ) → ψ y d ) ⇔ (Select X ψ ∋ y)
416 selection {ψ} {X} {y} = record { 355 selection {ψ} {X} {y} = {!!}
417 proj1 = λ cond → record { proj1 = proj1 cond ; proj2 = {!!} } -- ψiso {ψ} (proj2 cond) (sym oiso) }
418 ; proj2 = λ select → record { proj1 = proj1 select ; proj2 = ψiso {ψ} (proj2 select) {!!} }
419 }
420 replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x 356 replacement : {ψ : OD → OD} (X x : OD) → Replace X ψ ∋ ψ x
421 replacement {ψ} X x = sup-c< ψ {x} 357 replacement {ψ} X x = sup-c< ψ {x}
422 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅) 358 ∅-iso : {x : OD} → ¬ (x == od∅) → ¬ ((ord→od (od→ord x)) == od∅)
423 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq 359 ∅-iso {x} neq = subst (λ k → ¬ k) (=-iso {n} ) neq
424 minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n} 360 minimul : (x : OD {suc n} ) → ¬ (x == od∅ )→ OD {suc n}
425 minimul x not = {!!} 361 minimul x not = {!!}
426 regularity : (x : OD) (not : ¬ (x == od∅)) → 362 regularity : (x : OD) (not : ¬ (x == od∅)) →
427 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅) 363 (x ∋ minimul x not) ∧ (Select (minimul x not) (λ x₁ d → (minimul x not ∋ x₁) ∧ (x ∋ x₁)) == od∅)
428 proj1 (regularity x not ) = {!!} 364 proj1 (regularity x not ) = {!!}
429 proj2 (regularity x not ) = record { eq→ = reg ; eq← = {!!} } where 365 proj2 (regularity x not ) = record { eq→ = reg ; eq← = {!!} } where
430 reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y 366 reg : {y : Ordinal} → def (Select (minimul x not) (λ x₂ d → (minimul x not ∋ x₂) ∧ (x ∋ x₂))) y → def od∅ y
431 reg {y} t with proj1 t 367 reg {y} t = {!!}
432 ... | x∈∅ = {!!}
433 extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B 368 extensionality : {A B : OD {suc n}} → ((z : OD) → (A ∋ z) ⇔ (B ∋ z)) → A == B
434 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d 369 eq→ (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {A} {B} (sym diso) (proj1 (eq (ord→od x))) d
435 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d 370 eq← (extensionality {A} {B} eq ) {x} d = def-iso {suc n} {B} {A} (sym diso) (proj2 (eq (ord→od x))) d
436 xx-union : {x : OD {suc n}} → (x , x) ≡ record { def = λ z → z o< osuc (od→ord x) } 371 xx-union : {x : OD {suc n}} → (x , x) ≡ record { def = λ z → z o< osuc (od→ord x) }
437 xx-union {x} = cong ( λ k → Ord k ) (omxx (od→ord x)) 372 xx-union {x} = cong ( λ k → Ord k ) (omxx (od→ord x))
438 xxx-union : {x : OD {suc n}} → (x , (x , x)) ≡ record { def = λ z → z o< osuc (osuc (od→ord x))} 373 xxx-union : {x : OD {suc n}} → (x , (x , x)) ≡ record { def = λ z → z o< osuc (osuc (od→ord x))}
439 xxx-union {x} = cong ( λ k → Ord k ) lemma where 374 xxx-union {x} = cong ( λ k → Ord k ) lemma where
440 lemma1 : {x : OD {suc n}} → od→ord x o< od→ord (x , x) 375 lemma1 : {x : OD {suc n}} → od→ord x o< od→ord (x , x)
441 lemma1 {x} = c<→o< ( proj1 (pair x x ) ) 376 lemma1 {x} = c<→o< ( proj1 (pair x x ) )
442 lemma2 : {x : OD {suc n}} → od→ord (x , x) ≡ osuc (od→ord x) 377 lemma2 : {x : OD {suc n}} → od→ord (x , x) ≡ osuc (od→ord x)
443 lemma2 = trans ( cong ( λ k → od→ord k ) xx-union ) (sym ≡-def) 378 lemma2 = trans ( cong ( λ k → od→ord k ) xx-union ) {!!}
444 lemma : {x : OD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x)) 379 lemma : {x : OD {suc n}} → omax (od→ord x) (od→ord (x , x)) ≡ osuc (osuc (od→ord x))
445 lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) lemma1 ) ) ( cong ( λ k → osuc k ) lemma2 ) 380 lemma {x} = trans ( sym ( omax< (od→ord x) (od→ord (x , x)) lemma1 ) ) ( cong ( λ k → osuc k ) lemma2 )
446 uxxx-union : {x : OD {suc n}} → Union (x , (x , x)) ≡ record { def = λ z → osuc z o< osuc (osuc (od→ord x)) } 381 uxxx-union : {x : OD {suc n}} → Union (x , (x , x)) ≡ record { def = λ z → osuc z o< osuc (osuc (od→ord x)) }
447 uxxx-union {x} = cong ( λ k → record { def = λ z → osuc z o< k ; otrans = {!!} } ) lemma where 382 uxxx-union {x} = cong ( λ k → record { def = λ z → osuc z o< k ; otrans = {!!} } ) lemma where
448 lemma : od→ord (x , (x , x)) ≡ osuc (osuc (od→ord x)) 383 lemma : od→ord (x , (x , x)) ≡ osuc (osuc (od→ord x))
449 lemma = trans ( cong ( λ k → od→ord k ) xxx-union ) (sym ≡-def ) 384 lemma = trans ( cong ( λ k → od→ord k ) xxx-union ) {!!}
450 uxxx-2 : {x : OD {suc n}} → record { def = λ z → osuc z o< osuc (osuc (od→ord x)) } == record { def = λ z → z o< osuc (od→ord x) } 385 uxxx-2 : {x : OD {suc n}} → record { def = λ z → osuc z o< osuc (osuc (od→ord x)) } == record { def = λ z → z o< osuc (od→ord x) }
451 eq→ ( uxxx-2 {x} ) {m} lt = proj1 (osuc2 m (od→ord x)) lt 386 eq→ ( uxxx-2 {x} ) {m} lt = proj1 (osuc2 m (od→ord x)) lt
452 eq← ( uxxx-2 {x} ) {m} lt = proj2 (osuc2 m (od→ord x)) lt 387 eq← ( uxxx-2 {x} ) {m} lt = proj2 (osuc2 m (od→ord x)) lt
453 uxxx-ord : {x : OD {suc n}} → od→ord (Union (x , (x , x))) ≡ osuc (od→ord x) 388 uxxx-ord : {x : OD {suc n}} → od→ord (Union (x , (x , x))) ≡ osuc (od→ord x)
454 uxxx-ord {x} = trans (cong (λ k → od→ord k ) uxxx-union) (==→o≡ (subst₂ (λ j k → j == k ) (sym oiso) (sym od≡-def ) uxxx-2 )) 389 uxxx-ord {x} = trans (cong (λ k → od→ord k ) uxxx-union) {!!}
455 omega = record { lv = Suc Zero ; ord = Φ 1 }
456 infinite : OD {suc n} 390 infinite : OD {suc n}
457 infinite = ord→od ( omega ) 391 infinite = Ord omega
458 infinity∅ : ord→od ( omega ) ∋ od∅ {suc n} 392 infinity∅ : Ord omega ∋ od∅ {suc n}
459 infinity∅ = def-subst {suc n} {_} {o∅} {infinite} {od→ord od∅} 393 infinity∅ = {!!}
460 {!!} refl (subst ( λ k → ( k ≡ od→ord od∅ )) diso (cong (λ k → od→ord k) o∅≡od∅ ))
461 infinite∋x : (x : OD) → infinite ∋ x → od→ord x o< omega
462 infinite∋x x lt = subst (λ k → od→ord x o< k ) diso t where
463 t : od→ord x o< od→ord (ord→od (omega))
464 t = ∋→o< {n} {infinite} {x} lt
465 infinite∋uxxx : (x : OD) → osuc (od→ord x) o< omega → infinite ∋ Union (x , (x , x ))
466 infinite∋uxxx x lt = o<∋→ t where
467 t : od→ord (Union (x , (x , x))) o< od→ord (ord→od (omega))
468 t = subst (λ k → od→ord (Union (x , (x , x))) o< k ) (sym diso ) ( subst ( λ k → k o< omega ) ( sym (uxxx-ord {x} ) ) lt )
469 infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x )) 394 infinity : (x : OD) → infinite ∋ x → infinite ∋ Union (x , (x , x ))
470 infinity x lt = infinite∋uxxx x ( lemma (od→ord x) (infinite∋x x lt )) where 395 infinity x lt = {!!} where
471 lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega 396 lemma : (ox : Ordinal {suc n} ) → ox o< omega → osuc ox o< omega
472 lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n) 397 lemma record { lv = Zero ; ord = (Φ .0) } (case1 (s≤s x)) = case1 (s≤s z≤n)
473 lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n) 398 lemma record { lv = Zero ; ord = (OSuc .0 ord₁) } (case1 (s≤s x)) = case1 (s≤s z≤n)
474 lemma record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } (case1 (s≤s ())) 399 lemma record { lv = (Suc lv₁) ; ord = (Φ .(Suc lv₁)) } (case1 (s≤s ()))
475 lemma record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } (case1 (s≤s ())) 400 lemma record { lv = (Suc lv₁) ; ord = (OSuc .(Suc lv₁) ord₁) } (case1 (s≤s ()))