### view Ordinals.agda @ 427:9b0630f03c4bdefaulttip

...
author Shinji KONO Sat, 08 Aug 2020 18:14:14 +0900 cc7909f86841
line wrap: on
line source
```
open import Level
module Ordinals where

open import zf

open import Data.Nat renaming ( zero to Zero ; suc to Suc ;  ℕ to Nat ; _⊔_ to _n⊔_ )
open import Data.Empty
open import  Relation.Binary.PropositionalEquality
open import  logic
open import  nat
open import Data.Unit using ( ⊤ )
open import Relation.Nullary
open import Relation.Binary
open import Relation.Binary.Core

record Oprev {n : Level} (ord : Set n) (osuc :  ord → ord ) (x : ord ) : Set (suc n) where
field
oprev : ord
oprev=x : osuc oprev ≡ x

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
field
ordtrans : {x y z : ord }  → x o< y → y o< z → x o< z
trio<    : Trichotomous {n} _≡_  _o<_
¬x<0     : { x : ord  } → ¬ ( x o< o∅  )
<-osuc   : { x : ord  } → x o< osuc x
osuc-≡<  : { a x : ord  } → x o< osuc a  →  (x ≡ a ) ∨ (x o< a)
Oprev-p  : ( x : ord  ) → Dec ( Oprev ord osuc x )
TransFinite : { ψ : ord  → Set (suc n) }
→ ( (x : ord)  → ( (y : ord  ) → y o< x → ψ y ) → ψ x )
→  ∀ (x : ord)  → ψ x

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
field
x<nx :    { y : ord } → (y o< next y )
osuc<nx : { x y : ord } → x o< next y → osuc x o< next y
¬nx<nx :  {x y : ord} → y o< x → x o< next y →  ¬ ((z : ord) → ¬ (x ≡ osuc z))

record Ordinals {n : Level} : Set (suc (suc n)) where
field
Ordinal : Set n
o∅ : Ordinal
osuc : Ordinal → Ordinal
_o<_ : Ordinal → Ordinal → Set n
next :  Ordinal → Ordinal
isOrdinal : IsOrdinals Ordinal o∅ osuc _o<_ next
isNext : IsNext Ordinal o∅ osuc _o<_ next

module inOrdinal  {n : Level} (O : Ordinals {n} ) where

open Ordinals  O
open IsOrdinals isOrdinal
open IsNext isNext

TransFinite0 : { ψ : Ordinal  → Set n }
→ ( (x : Ordinal)  → ( (y : Ordinal  ) → y o< x → ψ y ) → ψ x )
→  ∀ (x : Ordinal)  → ψ x
TransFinite0 {ψ} ind x = lower (TransFinite {λ y → Lift (suc n) ( ψ y)} ind1 x) where
ind1 : (z : Ordinal) → ((y : Ordinal) → y o< z → Lift (suc n) (ψ y)) → Lift (suc n) (ψ z)
ind1 z prev = lift (ind z (λ y y<z → lower (prev y y<z ) ))

```