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

comparison ordinal.agda @ 224:afc864169325

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
recover ε-induction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 10 Aug 2019 12:31:25 +0900
parents 59771eb07df0
children e06b76e5b682
comparison
equal deleted inserted replaced
223:2e1f19c949dc 224:afc864169325
27 open Ordinal 27 open Ordinal
28 28
29 _o<_ : {n : Level} ( x y : Ordinal ) → Set n 29 _o<_ : {n : Level} ( x y : Ordinal ) → Set n
30 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y ) 30 _o<_ x y = (lv x < lv y ) ∨ ( ord x d< ord y )
31 31
32 o<-dom : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal
33 o<-dom {n} {x} _ = x
34
35 o<-cod : {n : Level} { x y : Ordinal {n}} → x o< y → Ordinal
36 o<-cod {n} {_} {y} _ = y
37
38 s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x 32 s<refl : {n : Level } {lx : Nat } { x : OrdinalD {n} lx } → x d< OSuc lx x
39 s<refl {n} {lv} {Φ lv} = Φ< 33 s<refl {n} {lv} {Φ lv} = Φ<
40 s<refl {n} {lv} {OSuc lv x} = s< s<refl 34 s<refl {n} {lv} {OSuc lv x} = s< s<refl
41 35
42 trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥ 36 trio<> : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → y d< x → x d< y → ⊥
64 58
65 ordinal-cong : {n : Level} {x y : Ordinal {n}} → 59 ordinal-cong : {n : Level} {x y : Ordinal {n}} →
66 lv x ≡ lv y → ord x ≅ ord y → x ≡ y 60 lv x ≡ lv y → ord x ≅ ord y → x ≡ y
67 ordinal-cong refl refl = refl 61 ordinal-cong refl refl = refl
68 62
69 ordinal-lv : {n : Level} {x y : Ordinal {n}} → x ≡ y → lv x ≡ lv y
70 ordinal-lv refl = refl
71
72 ordinal-d : {n : Level} {x y : Ordinal {n}} → x ≡ y → ord x ≅ ord y
73 ordinal-d refl = refl
74
75 ≡→¬d< : {n : Level} → {lv : Nat} → {x : OrdinalD {n} lv } → x d< x → ⊥ 63 ≡→¬d< : {n : Level} → {lv : Nat} → {x : OrdinalD {n} lv } → x d< x → ⊥
76 ≡→¬d< {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t 64 ≡→¬d< {n} {lx} {OSuc lx y} (s< t) = ≡→¬d< t
77 65
78 trio<≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → x d< y → ⊥ 66 trio<≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → x d< y → ⊥
79 trio<≡ refl = ≡→¬d< 67 trio<≡ refl = ≡→¬d<
80 68
81 trio>≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → y d< x → ⊥ 69 trio>≡ : {n : Level} → {lx : Nat} {x : OrdinalD {n} lx } { y : OrdinalD lx } → x ≡ y → y d< x → ⊥
82 trio>≡ refl = ≡→¬d< 70 trio>≡ refl = ≡→¬d<
83
84 triO : {n : Level} → {lx ly : Nat} → OrdinalD {n} lx → OrdinalD {n} ly → Tri (lx < ly) ( lx ≡ ly ) ( lx > ly )
85 triO {n} {lx} {ly} x y = <-cmp lx ly
86 71
87 triOrdd : {n : Level} → {lx : Nat} → Trichotomous _≡_ ( _d<_ {n} {lx} {lx} ) 72 triOrdd : {n : Level} → {lx : Nat} → Trichotomous _≡_ ( _d<_ {n} {lx} {lx} )
88 triOrdd {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d< 73 triOrdd {_} {lv} (Φ lv) (Φ lv) = tri≈ ≡→¬d< refl ≡→¬d<
89 triOrdd {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< ) 74 triOrdd {_} {lv} (Φ lv) (OSuc lv y) = tri< Φ< (λ ()) ( λ lt → trio<> lt Φ< )
90 triOrdd {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ< 75 triOrdd {_} {lv} (OSuc lv x) (Φ lv) = tri> (λ lt → trio<> lt Φ<) (λ ()) Φ<
97 osuc record { lv = lx ; ord = ox } = record { lv = lx ; ord = OSuc lx ox } 82 osuc record { lv = lx ; ord = ox } = record { lv = lx ; ord = OSuc lx ox }
98 83
99 <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x 84 <-osuc : {n : Level} { x : Ordinal {n} } → x o< osuc x
100 <-osuc {n} {record { lv = lx ; ord = Φ .lx }} = case2 Φ< 85 <-osuc {n} {record { lv = lx ; ord = Φ .lx }} = case2 Φ<
101 <-osuc {n} {record { lv = lx ; ord = OSuc .lx ox }} = case2 ( s< s<refl ) 86 <-osuc {n} {record { lv = lx ; ord = OSuc .lx ox }} = case2 ( s< s<refl )
102
103 osuc-lveq : {n : Level} { x : Ordinal {n} } → lv x ≡ lv ( osuc x )
104 osuc-lveq {n} = refl
105
106 osucc : {n : Level} {ox oy : Ordinal {n}} → oy o< ox → osuc oy o< osuc ox
107 osucc {n} {ox} {oy} (case1 x) = case1 x
108 osucc {n} {ox} {oy} (case2 x) with d<→lv x
109 ... | refl = case2 (s< x)
110
111 case12-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord x d< ord y → ⊥
112 case12-⊥ {x} {y} lt1 lt2 with d<→lv lt2
113 ... | refl = nat-≡< refl lt1
114
115 case21-⊥ : {n : Level} {x y : Ordinal {suc n}} → lv x < lv y → ord y d< ord x → ⊥
116 case21-⊥ {x} {y} lt1 lt2 with d<→lv lt2
117 ... | refl = nat-≡< refl lt1
118 87
119 o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy → ox o< oy → ⊥ 88 o<¬≡ : {n : Level } { ox oy : Ordinal {suc n}} → ox ≡ oy → ox o< oy → ⊥
120 o<¬≡ {_} {ox} {ox} refl (case1 lt) = =→¬< lt 89 o<¬≡ {_} {ox} {ox} refl (case1 lt) = =→¬< lt
121 o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt 90 o<¬≡ {_} {ox} {ox} refl (case2 (s< lt)) = trio<≡ refl lt
122 91
154 osuc-< {n} {x} {x} (case2 x₂) (case2 x₁) | case1 refl = ≡→¬d< x₁ 123 osuc-< {n} {x} {x} (case2 x₂) (case2 x₁) | case1 refl = ≡→¬d< x₁
155 osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case1 x₁) = nat-<> x₂ x₁ 124 osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case1 x₁) = nat-<> x₂ x₁
156 osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case2 x₁) = nat-≡< (sym (d<→lv x₁)) x₂ 125 osuc-< {n} {x} {y} y<ox (case1 x₂) | case2 (case2 x₁) = nat-≡< (sym (d<→lv x₁)) x₂
157 osuc-< {n} {x} {y} y<ox (case2 x<y) | case2 y<x = o<> (case2 x<y) y<x 126 osuc-< {n} {x} {y} y<ox (case2 x<y) | case2 y<x = o<> (case2 x<y) y<x
158 127
159 maxαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx → OrdinalD lx → OrdinalD lx
160 maxαd x y with triOrdd x y
161 maxαd x y | tri< a ¬b ¬c = y
162 maxαd x y | tri≈ ¬a b ¬c = x
163 maxαd x y | tri> ¬a ¬b c = x
164
165 minαd : {n : Level} → { lx : Nat } → OrdinalD {n} lx → OrdinalD lx → OrdinalD lx
166 minαd x y with triOrdd x y
167 minαd x y | tri< a ¬b ¬c = x
168 minαd x y | tri≈ ¬a b ¬c = y
169 minαd x y | tri> ¬a ¬b c = x
170
171 _o≤_ : {n : Level} → Ordinal → Ordinal → Set (suc n)
172 a o≤ b = (a ≡ b) ∨ ( a o< b )
173 128
174 ordtrans : {n : Level} {x y z : Ordinal {n} } → x o< y → y o< z → x o< z 129 ordtrans : {n : Level} {x y z : Ordinal {n} } → x o< y → y o< z → x o< z
175 ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ ) 130 ordtrans {n} {x} {y} {z} (case1 x₁) (case1 x₂) = case1 ( <-trans x₁ x₂ )
176 ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂ 131 ordtrans {n} {x} {y} {z} (case1 x₁) (case2 x₂) with d<→lv x₂
177 ... | refl = case1 x₁ 132 ... | refl = case1 x₁
206 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where 161 trio< record { lv = .(lv b) ; ord = x } b | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = tri≈ lemma1 refl lemma1 where
207 lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b) 162 lemma1 : ¬ (Suc (lv b) ≤ lv b) ∨ (ord b d< ord b)
208 lemma1 (case1 x) = ¬a x 163 lemma1 (case1 x) = ¬a x
209 lemma1 (case2 x) = ≡→¬d< x 164 lemma1 (case2 x) = ≡→¬d< x
210 165
211 xo<ab : {n : Level} {oa ob : Ordinal {suc n}} → ( {ox : Ordinal {suc n}} → ox o< oa → ox o< ob ) → oa o< osuc ob
212 xo<ab {n} {oa} {ob} a→b with trio< oa ob
213 xo<ab {n} {oa} {ob} a→b | tri< a ¬b ¬c = ordtrans a <-osuc
214 xo<ab {n} {oa} {ob} a→b | tri≈ ¬a refl ¬c = <-osuc
215 xo<ab {n} {oa} {ob} a→b | tri> ¬a ¬b c = ⊥-elim ( o<¬≡ refl (a→b c ) )
216
217 maxα : {n : Level} → Ordinal {suc n} → Ordinal → Ordinal
218 maxα x y with trio< x y
219 maxα x y | tri< a ¬b ¬c = y
220 maxα x y | tri> ¬a ¬b c = x
221 maxα x y | tri≈ ¬a refl ¬c = x
222
223 minα : {n : Level} → Ordinal {suc n} → Ordinal → Ordinal
224 minα {n} x y with trio< {n} x y
225 minα x y | tri< a ¬b ¬c = x
226 minα x y | tri> ¬a ¬b c = y
227 minα x y | tri≈ ¬a refl ¬c = x
228
229 min1 : {n : Level} → {x y z : Ordinal {suc n} } → z o< x → z o< y → z o< minα x y
230 min1 {n} {x} {y} {z} z<x z<y with trio< {n} x y
231 min1 {n} {x} {y} {z} z<x z<y | tri< a ¬b ¬c = z<x
232 min1 {n} {x} {y} {z} z<x z<y | tri≈ ¬a refl ¬c = z<x
233 min1 {n} {x} {y} {z} z<x z<y | tri> ¬a ¬b c = z<y
234
235 --
236 -- max ( osuc x , osuc y )
237 --
238
239 omax : {n : Level} ( x y : Ordinal {suc n} ) → Ordinal {suc n}
240 omax {n} x y with trio< x y
241 omax {n} x y | tri< a ¬b ¬c = osuc y
242 omax {n} x y | tri> ¬a ¬b c = osuc x
243 omax {n} x y | tri≈ ¬a refl ¬c = osuc x
244
245 omax< : {n : Level} ( x y : Ordinal {suc n} ) → x o< y → osuc y ≡ omax x y
246 omax< {n} x y lt with trio< x y
247 omax< {n} x y lt | tri< a ¬b ¬c = refl
248 omax< {n} x y lt | tri≈ ¬a b ¬c = ⊥-elim (¬a lt )
249 omax< {n} x y lt | tri> ¬a ¬b c = ⊥-elim (¬a lt )
250
251 omax≡ : {n : Level} ( x y : Ordinal {suc n} ) → x ≡ y → osuc y ≡ omax x y
252 omax≡ {n} x y eq with trio< x y
253 omax≡ {n} x y eq | tri< a ¬b ¬c = ⊥-elim (¬b eq )
254 omax≡ {n} x y eq | tri≈ ¬a refl ¬c = refl
255 omax≡ {n} x y eq | tri> ¬a ¬b c = ⊥-elim (¬b eq )
256
257 omax-x : {n : Level} ( x y : Ordinal {suc n} ) → x o< omax x y
258 omax-x {n} x y with trio< x y
259 omax-x {n} x y | tri< a ¬b ¬c = ordtrans a <-osuc
260 omax-x {n} x y | tri> ¬a ¬b c = <-osuc
261 omax-x {n} x y | tri≈ ¬a refl ¬c = <-osuc
262
263 omax-y : {n : Level} ( x y : Ordinal {suc n} ) → y o< omax x y
264 omax-y {n} x y with trio< x y
265 omax-y {n} x y | tri< a ¬b ¬c = <-osuc
266 omax-y {n} x y | tri> ¬a ¬b c = ordtrans c <-osuc
267 omax-y {n} x y | tri≈ ¬a refl ¬c = <-osuc
268
269 omxx : {n : Level} ( x : Ordinal {suc n} ) → omax x x ≡ osuc x
270 omxx {n} x with trio< x x
271 omxx {n} x | tri< a ¬b ¬c = ⊥-elim (¬b refl )
272 omxx {n} x | tri> ¬a ¬b c = ⊥-elim (¬b refl )
273 omxx {n} x | tri≈ ¬a refl ¬c = refl
274
275 omxxx : {n : Level} ( x : Ordinal {suc n} ) → omax x (omax x x ) ≡ osuc (osuc x)
276 omxxx {n} x = trans ( cong ( λ k → omax x k ) (omxx x )) (sym ( omax< x (osuc x) <-osuc ))
277 166
278 open _∧_ 167 open _∧_
279
280 osuc2 : {n : Level} ( x y : Ordinal {suc n} ) → ( osuc x o< osuc (osuc y )) ⇔ (x o< osuc y)
281 proj1 (osuc2 {n} x y) (case1 lt) = case1 lt
282 proj1 (osuc2 {n} x y) (case2 (s< lt)) = case2 lt
283 proj2 (osuc2 {n} x y) (case1 lt) = case1 lt
284 proj2 (osuc2 {n} x y) (case2 lt) with d<→lv lt
285 ... | refl = case2 (s< lt)
286
287 OrdTrans : {n : Level} → Transitive {suc n} _o≤_
288 OrdTrans (case1 refl) (case1 refl) = case1 refl
289 OrdTrans (case1 refl) (case2 lt2) = case2 lt2
290 OrdTrans (case2 lt1) (case1 refl) = case2 lt1
291 OrdTrans (case2 x) (case2 y) = case2 (ordtrans x y)
292
293 OrdPreorder : {n : Level} → Preorder (suc n) (suc n) (suc n)
294 OrdPreorder {n} = record { Carrier = Ordinal
295 ; _≈_ = _≡_
296 ; _∼_ = _o≤_
297 ; isPreorder = record {
298 isEquivalence = record { refl = refl ; sym = sym ; trans = trans }
299 ; reflexive = case1
300 ; trans = OrdTrans
301 }
302 }
303 168
304 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m } 169 TransFinite : {n m : Level} → { ψ : Ordinal {suc n} → Set m }
305 → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) ) 170 → ( ∀ (lx : Nat ) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x ) → ψ ( record { lv = lx ; ord = Φ lx } ) )
306 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x) → ψ y ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) ) 171 → ( ∀ (lx : Nat ) → (x : OrdinalD lx ) → ( (y : Ordinal {suc n} ) → y o< ordinal lx (OSuc lx x) → ψ y ) → ψ ( record { lv = lx ; ord = OSuc lx x } ) )
307 → ∀ (x : Ordinal) → ψ x 172 → ∀ (x : Ordinal) → ψ x
353 → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → ¬ p ) 218 → {p : Set l} ( P : { y : Ordinal {n} } → ψ y → ¬ p )
354 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) 219 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
355 → ¬ p 220 → ¬ p
356 TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 221 TransFiniteExists {n} {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
357 222
358 open import Ordinals 223 open import Ordinals
359 224
360 C-Ordinal : {n : Level } → Ordinals {suc n} 225 C-Ordinal : {n : Level} → Ordinals {suc n}
361 C-Ordinal {n} = record { 226 C-Ordinal {n} = record {
362 ord = Ordinal {suc n} 227 ord = Ordinal {suc n}
363 ; o∅ = o∅ 228 ; o∅ = o∅
364 ; osuc = osuc 229 ; osuc = osuc
365 ; _o<_ = _o<_ 230 ; _o<_ = _o<_
382 ψ (record { lv = lx ; ord = Φ lx }) 247 ψ (record { lv = lx ; ord = Φ lx })
383 caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev 248 caseΦ lx prev = lt (ordinal lx (Φ lx) ) prev
384 caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) → 249 caseOSuc : (lx : Nat) (x₁ : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x₁) → ψ y) →
385 ψ (record { lv = lx ; ord = OSuc lx x₁ }) 250 ψ (record { lv = lx ; ord = OSuc lx x₁ })
386 caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev 251 caseOSuc lx ox prev = lt (ordinal lx (OSuc lx ox)) prev
252
253 module C-Ordinal-with-choice {n : Level} where
254
255 import OD
256 -- open inOrdinal C-Ordinal
257 open OD (C-Ordinal {n})
258 open OD.OD
259
260 --
261 -- another form of regularity
262 --
263 ε-induction : {m : Level} { ψ : OD → Set m}
264 → ( {x : OD } → ({ y : OD } → x ∋ y → ψ y ) → ψ x )
265 → (x : OD ) → ψ x
266 ε-induction {m} {ψ} ind x = subst (λ k → ψ k ) oiso (ε-induction-ord (lv (osuc (od→ord x))) (ord (osuc (od→ord x))) <-osuc) where
267 ε-induction-ord : (lx : Nat) ( ox : OrdinalD {suc n} lx ) {ly : Nat} {oy : OrdinalD {suc n} ly }
268 → (ly < lx) ∨ (oy d< ox ) → ψ (ord→od (record { lv = ly ; ord = oy } ) )
269 ε-induction-ord lx (OSuc lx ox) {ly} {oy} y<x =
270 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → subst (λ k → ψ k ) oiso (ε-induction-ord lx ox (lemma y lt ))) where
271 lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → od→ord z o< record { lv = lx ; ord = ox }
272 lemma z lt with osuc-≡< y<x
273 lemma z lt | case1 refl = o<-subst (c<→o< lt) refl diso
274 lemma z lt | case2 lt1 = ordtrans (o<-subst (c<→o< lt) refl diso) lt1
275 ε-induction-ord (Suc lx) (Φ (Suc lx)) {ly} {oy} (case1 y<sox ) =
276 ind {ord→od (record { lv = ly ; ord = oy })} ( λ {y} lt → lemma y lt ) where
277 --
278 -- if lv of z if less than x Ok
279 -- else lv z = lv x. We can create OSuc of z which is larger than z and less than x in lemma
280 --
281 -- lx Suc lx (1) lz(a) <lx by case1
282 -- ly(1) ly(2) (2) lz(b) <lx by case1
283 -- lz(a) lz(b) lz(c) lz(c) <lx by case2 ( ly==lz==lx)
284 --
285 lemma0 : { lx ly : Nat } → ly < Suc lx → lx < ly → ⊥
286 lemma0 {Suc lx} {Suc ly} (s≤s lt1) (s≤s lt2) = lemma0 lt1 lt2
287 lemma1 : {ly : Nat} {oy : OrdinalD {suc n} ly} → lv (od→ord (ord→od (record { lv = ly ; ord = oy }))) ≡ ly
288 lemma1 {ly} {oy} = let open ≡-Reasoning in begin
289 lv (od→ord (ord→od (record { lv = ly ; ord = oy })))
290 ≡⟨ cong ( λ k → lv k ) diso ⟩
291 lv (record { lv = ly ; ord = oy })
292 ≡⟨⟩
293 ly
294 ∎
295 lemma : (z : OD) → ord→od record { lv = ly ; ord = oy } ∋ z → ψ z
296 lemma z lt with c<→o< {z} {ord→od (record { lv = ly ; ord = oy })} lt
297 lemma z lt | case1 lz<ly with <-cmp lx ly
298 lemma z lt | case1 lz<ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
299 lemma z lt | case1 lz<ly | tri≈ ¬a refl ¬c = -- ly(1)
300 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → lv (od→ord z) < k ) lemma1 lz<ly ) ))
301 lemma z lt | case1 lz<ly | tri> ¬a ¬b c = -- lz(a)
302 subst (λ k → ψ k ) oiso (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (<-trans lz<ly (subst (λ k → k < lx ) (sym lemma1) c))))
303 lemma z lt | case2 lz=ly with <-cmp lx ly
304 lemma z lt | case2 lz=ly | tri< a ¬b ¬c = ⊥-elim ( lemma0 y<sox a) -- can't happen
305 lemma z lt | case2 lz=ly | tri> ¬a ¬b c with d<→lv lz=ly -- lz(b)
306 ... | eq = subst (λ k → ψ k ) oiso
307 (ε-induction-ord lx (Φ lx) {_} {ord (od→ord z)} (case1 (subst (λ k → k < lx ) (trans (sym lemma1)(sym eq) ) c )))
308 lemma z lt | case2 lz=ly | tri≈ ¬a lx=ly ¬c with d<→lv lz=ly -- lz(c)
309 ... | eq = subst (λ k → ψ k ) oiso ( ε-induction-ord lx (dz oz=lx) {lv (od→ord z)} {ord (od→ord z)} (case2 (dz<dz oz=lx) )) where
310 oz=lx : lv (od→ord z) ≡ lx
311 oz=lx = let open ≡-Reasoning in begin
312 lv (od→ord z)
313 ≡⟨ eq ⟩
314 lv (od→ord (ord→od (ordinal ly oy)))
315 ≡⟨ cong ( λ k → lv k ) diso ⟩
316 lv (ordinal ly oy)
317 ≡⟨ sym lx=ly ⟩
318 lx
319 ∎
320 dz : lv (od→ord z) ≡ lx → OrdinalD lx
321 dz refl = OSuc lx (ord (od→ord z))
322 dz<dz : (z=x : lv (od→ord z) ≡ lx ) → ord (od→ord z) d< dz z=x
323 dz<dz refl = s<refl
324
325 ---
326 --- With assuption of OD is ordered, p ∨ ( ¬ p ) <=> axiom of choice
327 ---
328 record choiced ( X : OD) : Set (suc (suc n)) where
329 field
330 a-choice : OD
331 is-in : X ∋ a-choice
332
333 choice-func' : (X : OD ) → (p∨¬p : { n : Level } → ( p : Set (suc n) ) → p ∨ ( ¬ p )) → ¬ ( X == od∅ ) → choiced X
334 choice-func' X p∨¬p not = have_to_find where
335 ψ : ( ox : Ordinal {suc n}) → Set (suc (suc n))
336 ψ ox = (( x : Ordinal {suc n}) → x o< ox → ( ¬ def X x )) ∨ choiced X
337 lemma-ord : ( ox : Ordinal {suc n} ) → ψ ox
338 lemma-ord ox = TransFinite {n} {suc (suc n)} {ψ} caseΦ caseOSuc1 ox where
339 ∋-p' : (A x : OD ) → Dec ( A ∋ x )
340 ∋-p' A x with p∨¬p ( A ∋ x )
341 ∋-p' A x | case1 t = yes t
342 ∋-p' A x | case2 t = no t
343 ∀-imply-or : {n : Level} {A : Ordinal {suc n} → Set (suc n) } {B : Set (suc (suc n)) }
344 → ((x : Ordinal {suc n}) → A x ∨ B) → ((x : Ordinal {suc n}) → A x) ∨ B
345 ∀-imply-or {n} {A} {B} ∀AB with p∨¬p ((x : Ordinal {suc n}) → A x)
346 ∀-imply-or {n} {A} {B} ∀AB | case1 t = case1 t
347 ∀-imply-or {n} {A} {B} ∀AB | case2 x = case2 (lemma x) where
348 lemma : ¬ ((x : Ordinal {suc n}) → A x) → B
349 lemma not with p∨¬p B
350 lemma not | case1 b = b
351 lemma not | case2 ¬b = ⊥-elim (not (λ x → dont-orb (∀AB x) ¬b ))
352 caseΦ : (lx : Nat) → ( (x : Ordinal {suc n} ) → x o< ordinal lx (Φ lx) → ψ x) → ψ (ordinal lx (Φ lx) )
353 caseΦ lx prev with ∋-p' X ( ord→od (ordinal lx (Φ lx) ))
354 caseΦ lx prev | yes p = case2 ( record { a-choice = ord→od (ordinal lx (Φ lx)) ; is-in = p } )
355 caseΦ lx prev | no ¬p = lemma where
356 lemma1 : (x : Ordinal) → (((Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X)
357 lemma1 x with trio< x (ordinal lx (Φ lx))
358 lemma1 x | tri< a ¬b ¬c with prev (osuc x) (lemma2 a) where
359 lemma2 : x o< (ordinal lx (Φ lx)) → osuc x o< ordinal lx (Φ lx)
360 lemma2 (case1 lt) = case1 lt
361 lemma1 x | tri< a ¬b ¬c | case2 found = case2 found
362 lemma1 x | tri< a ¬b ¬c | case1 not_found = case1 ( λ lt df → not_found x <-osuc df )
363 lemma1 x | tri≈ ¬a refl ¬c = case1 ( λ lt → ⊥-elim (o<¬≡ refl lt ))
364 lemma1 x | tri> ¬a ¬b c = case1 ( λ lt → ⊥-elim (o<> lt c ))
365 lemma : ((x : Ordinal) → (Suc (lv x) ≤ lx) ∨ (ord x d< Φ lx) → def X x → ⊥) ∨ choiced X
366 lemma = ∀-imply-or lemma1
367 caseOSuc : (lx : Nat) (x : OrdinalD lx) → ψ ( ordinal lx x ) → ψ ( ordinal lx (OSuc lx x) )
368 caseOSuc lx x prev with ∋-p' X (ord→od record { lv = lx ; ord = x } )
369 caseOSuc lx x prev | yes p = case2 (record { a-choice = ord→od record { lv = lx ; ord = x } ; is-in = p })
370 caseOSuc lx x (case1 not_found) | no ¬p = case1 lemma where
371 lemma : (y : Ordinal) → (Suc (lv y) ≤ lx) ∨ (ord y d< OSuc lx x) → def X y → ⊥
372 lemma y lt with trio< y (ordinal lx x )
373 lemma y lt | tri< a ¬b ¬c = not_found y a
374 lemma y lt | tri≈ ¬a refl ¬c = subst (λ k → def X k → ⊥ ) diso ¬p
375 lemma y lt | tri> ¬a ¬b c with osuc-≡< lt
376 lemma y lt | tri> ¬a ¬b c | case1 refl = ⊥-elim ( ¬b refl )
377 lemma y lt | tri> ¬a ¬b c | case2 lt1 = ⊥-elim (o<> c lt1 )
378 caseOSuc lx x (case2 found) | no ¬p = case2 found
379 caseOSuc1 : (lx : Nat) (x : OrdinalD lx) → ((y : Ordinal) → y o< ordinal lx (OSuc lx x) → ψ y) →
380 ψ (record { lv = lx ; ord = OSuc lx x })
381 caseOSuc1 lx x lt = caseOSuc lx x (lt ( ordinal lx x ) (case2 s<refl))
382 have_to_find : choiced X
383 have_to_find with lemma-ord (od→ord X )
384 have_to_find | t = dont-or t ¬¬X∋x where
385 ¬¬X∋x : ¬ ((x : Ordinal) → (Suc (lv x) ≤ lv (od→ord X)) ∨ (ord x d< ord (od→ord X)) → def X x → ⊥)
386 ¬¬X∋x nn = not record {
387 eq→ = λ {x} lt → ⊥-elim (nn x (def→o< lt) lt)
388 ; eq← = λ {x} lt → ⊥-elim ( ¬x<0 lt )
389 }
390