```-- Ordinals as defined in the HoTT book.

{-# OPTIONS --without-K --safe #-}
module Ordinal.HoTT where

open import Data.Empty using (⊥)
open import Data.Unit using (⊤)
open import Induction.WellFounded using (Acc ; acc ; WellFounded)
open import Level using (Level ; _⊔_ ; 0ℓ) renaming (suc to lsuc)
open import Relation.Binary using (Rel ; IsEquivalence ; Transitive)

private
variable
α β γ ρ ε : Level
A B C : Set α

record _↔_ (A : Set α) (B : Set β) : Set (α ⊔ β) where
field
forth : A → B
back : B → A

open _↔_ public

IsExtensional : ∀ {α} {A : Set α} (_≈_ : Rel A ε) (_<_ : Rel A ρ) → Set (α ⊔ ε ⊔ ρ)
IsExtensional _≈_ _<_ = ∀ {a b} → (∀ c → (c < a) ↔ (c < b)) → a ≈ b

record IsOrdinal (A : Set α) ε ρ : Set (α ⊔ lsuc (ε ⊔ ρ)) where
field
_≈_ : Rel A ε
≈-equiv : IsEquivalence _≈_
_<_ : Rel A ρ
<-wf : WellFounded _<_
<-ext : IsExtensional _≈_ _<_
<-trans : Transitive _<_

open IsEquivalence ≈-equiv public using () renaming
( refl to ≈-refl
; sym to ≈-sym
; trans to ≈-trans)

open IsOrdinal public

record Ordinal α ε ρ : Set (lsuc (α ⊔ ε ⊔ ρ)) where
field
_↓ : Set α
isOrdinal : IsOrdinal _↓ ε ρ

open Ordinal public

zero : Ordinal 0ℓ 0ℓ 0ℓ
zero = record
{ _↓ = ⊤
; isOrdinal = record
{ _≈_ = λ _ _ → ⊤
; ≈-equiv = _
; _<_ = λ _ _ → ⊥
; <-wf = λ _ → acc λ y ()
; <-ext = _
; <-trans = λ()
}
}
```