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