|
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
|
|
1300
|
19 record IsOrdinals {n : Level} (ord : Set n) (o∅ : ord ) (osuc : ord → ord ) (_o<_ : ord → ord → Set n) : Set (suc (suc n)) where
|
|
431
|
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 record Ordinals {n : Level} : Set (suc (suc n)) where
|
|
|
33 field
|
|
|
34 Ordinal : Set n
|
|
|
35 o∅ : Ordinal
|
|
|
36 osuc : Ordinal → Ordinal
|
|
|
37 _o<_ : Ordinal → Ordinal → Set n
|
|
1300
|
38 isOrdinal : IsOrdinals Ordinal o∅ osuc _o<_
|
|
431
|
39
|
|
|
40 module inOrdinal {n : Level} (O : Ordinals {n} ) where
|
|
|
41
|
|
|
42 open Ordinals O
|
|
|
43 open IsOrdinals isOrdinal
|
|
|
44
|
|
|
45 TransFinite0 : { ψ : Ordinal → Set n }
|
|
|
46 → ( (x : Ordinal) → ( (y : Ordinal ) → y o< x → ψ y ) → ψ x )
|
|
|
47 → ∀ (x : Ordinal) → ψ x
|
|
|
48 TransFinite0 {ψ} ind x = lower (TransFinite {λ y → Lift (suc n) ( ψ y)} ind1 x) where
|
|
|
49 ind1 : (z : Ordinal) → ((y : Ordinal) → y o< z → Lift (suc n) (ψ y)) → Lift (suc n) (ψ z)
|
|
|
50 ind1 z prev = lift (ind z (λ y y<z → lower (prev y y<z ) ))
|
|
|
51
|
