comparison Ordinals.agda @ 339:feb0fcc430a9

...
author Shinji KONO Sun, 12 Jul 2020 19:55:37 +0900 bca043423554 639fbb6284d8
comparison
equal inserted replaced
338:bca043423554 339:feb0fcc430a9
19 OTri : Trichotomous {n} _≡_ _o<_ 19 OTri : Trichotomous {n} _≡_ _o<_
20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ ) 20 ¬x<0 : { x : ord } → ¬ ( x o< o∅ )
21 <-osuc : { x : ord } → x o< osuc x 21 <-osuc : { x : ord } → x o< osuc x
22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a) 22 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
23 not-limit : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) )) 23 not-limit : ( x : ord ) → Dec ( ¬ ((y : ord) → ¬ (x ≡ osuc y) ))
24 next-limit : { y : ord } → (y o< next y ) ∧ ((x : ord) → x o< next y → osuc x o< next y ) 24 next-limit : { y : ord } → (y o< next y ) ∧ ((x : ord) → x o< next y → osuc x o< next y ) ∧
25 ( (x : ord) → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z) ))
25 TransFinite : { ψ : ord → Set n } 26 TransFinite : { ψ : ord → Set n }
26 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) 27 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
27 → ∀ (x : ord) → ψ x 28 → ∀ (x : ord) → ψ x
28 TransFinite1 : { ψ : ord → Set (suc n) } 29 TransFinite1 : { ψ : ord → Set (suc n) }
29 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x ) 30 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
217 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p ) 218 → {p : Set l} ( P : { y : Ordinal } → ψ y → ¬ p )
218 → (exists : ¬ (∀ y → ¬ ( ψ y ) )) 219 → (exists : ¬ (∀ y → ¬ ( ψ y ) ))
219 → ¬ p 220 → ¬ p
220 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p ) 221 FExists {m} {l} ψ {p} P = contra-position ( λ p y ψy → P {y} ψy p )
221 222
223 next< : {x y z : Ordinal} → x o< next z → y o< next x → y o< next z
224 next< {x} {y} {z} x<nz y<nx with trio< y (next z)
225 next< {x} {y} {z} x<nz y<nx | tri< a ¬b ¬c = a
226 next< {x} {y} {z} x<nz y<nx | tri≈ ¬a b ¬c = ⊥-elim ((proj2 (proj2 next-limit)) (next z) x<nz (subst (λ k → k o< next x) b y<nx)
227 (λ w nz=ow → o<¬≡ nz=ow (subst₂ (λ j k → j o< k ) (sym nz=ow) nz=ow (proj1 (proj2 next-limit) w (subst (λ k → w o< k ) (sym nz=ow) <-osuc) ))))
228 next< {x} {y} {z} x<nz y<nx | tri> ¬a ¬b c = ⊥-elim (proj2 (proj2 next-limit) (next z) x<nz (ordtrans c y<nx )
229 (λ w nz=ow → o<¬≡ (sym nz=ow) (proj1 (proj2 next-limit) _ (subst (λ k → w o< k ) (sym nz=ow) <-osuc ))))
230
222 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where 231 record OrdinalSubset (maxordinal : Ordinal) : Set (suc n) where
223 field 232 field
224 os→ : (x : Ordinal) → x o< maxordinal → Ordinal 233 os→ : (x : Ordinal) → x o< maxordinal → Ordinal
225 os← : Ordinal → Ordinal 234 os← : Ordinal → Ordinal
226 os←limit : (x : Ordinal) → os← x o< maxordinal 235 os←limit : (x : Ordinal) → os← x o< maxordinal