|
431
|
1 open import Level
|
|
|
2 module Ordinals where
|
|
|
3
|
|
|
4 open import zf
|
|
|
5
|
|
|
6 open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ )
|
|
|
7 open import Data.Empty
|
|
|
8 open import Relation.Binary.PropositionalEquality
|
|
|
9 open import logic
|
|
|
10 open import nat
|
|
|
11 open import Data.Unit using ( ⊤ )
|
|
|
12 open import Relation.Nullary
|
|
|
13 open import Relation.Binary
|
|
|
14 open import Relation.Binary.Core
|
|
|
15
|
|
|
16 record Oprev {n : Level} (ord : Set n) (osuc : ord → ord ) (x : ord ) : Set (suc n) where
|
|
|
17 field
|
|
|
18 oprev : ord
|
|
|
19 oprev=x : osuc oprev ≡ x
|
|
|
20
|
|
|
21 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
|
|
|
22 field
|
|
|
23 ordtrans : {x y z : ord } → x o< y → y o< z → x o< z
|
|
|
24 trio< : Trichotomous {n} _≡_ _o<_
|
|
|
25 ¬x<0 : { x : ord } → ¬ ( x o< o∅ )
|
|
|
26 <-osuc : { x : ord } → x o< osuc x
|
|
|
27 osuc-≡< : { a x : ord } → x o< osuc a → (x ≡ a ) ∨ (x o< a)
|
|
|
28 Oprev-p : ( x : ord ) → Dec ( Oprev ord osuc x )
|
|
1009
|
29 o<-irr : { x y : ord } → { lt lt1 : x o< y } → lt ≡ lt1
|
|
431
|
30 TransFinite : { ψ : ord → Set (suc n) }
|
|
|
31 → ( (x : ord) → ( (y : ord ) → y o< x → ψ y ) → ψ x )
|
|
|
32 → ∀ (x : ord) → ψ x
|
|
|
33
|
|
|
34
|
|
|
35 record IsNext {n : Level } (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) (next : ord → ord ) : Set (suc (suc n)) where
|
|
|
36 field
|
|
|
37 x<nx : { y : ord } → (y o< next y )
|
|
|
38 osuc<nx : { x y : ord } → x o< next y → osuc x o< next y
|
|
|
39 ¬nx<nx : {x y : ord} → y o< x → x o< next y → ¬ ((z : ord) → ¬ (x ≡ osuc z))
|
|
|
40
|
|
|
41 record Ordinals {n : Level} : Set (suc (suc n)) where
|
|
|
42 field
|
|
|
43 Ordinal : Set n
|
|
|
44 o∅ : Ordinal
|
|
|
45 osuc : Ordinal → Ordinal
|
|
|
46 _o<_ : Ordinal → Ordinal → Set n
|
|
|
47 next : Ordinal → Ordinal
|
|
|
48 isOrdinal : IsOrdinals Ordinal o∅ osuc _o<_ next
|
|
|
49 isNext : IsNext Ordinal o∅ osuc _o<_ next
|
|
|
50
|
|
|
51 module inOrdinal {n : Level} (O : Ordinals {n} ) where
|
|
|
52
|
|
|
53 open Ordinals O
|
|
|
54 open IsOrdinals isOrdinal
|
|
|
55 open IsNext isNext
|
|
|
56
|
|
|
57 TransFinite0 : { ψ : Ordinal → Set n }
|
|
|
58 → ( (x : Ordinal) → ( (y : Ordinal ) → y o< x → ψ y ) → ψ x )
|
|
|
59 → ∀ (x : Ordinal) → ψ x
|
|
|
60 TransFinite0 {ψ} ind x = lower (TransFinite {λ y → Lift (suc n) ( ψ y)} ind1 x) where
|
|
|
61 ind1 : (z : Ordinal) → ((y : Ordinal) → y o< z → Lift (suc n) (ψ y)) → Lift (suc n) (ψ z)
|
|
|
62 ind1 z prev = lift (ind z (λ y y<z → lower (prev y y<z ) ))
|
|
|
63
|
