Martin Escardo, April 2013, adapted to this development June 2018,

Ordinals like in the HoTT book and variations.

\begin{code}

{-# OPTIONS --without-K --exact-split --safe #-}

open import SpartanMLTT

open import UF-Base
open import UF-Subsingletons
open import UF-FunExt
open import UF-Subsingletons-FunExt

module OrdinalNotions
{π€ π₯ : Universe}
{X : π€ Μ }
(_<_ : X β X β π₯ Μ )
where

is-prop-valued : π€ β π₯ Μ
is-prop-valued = (x y : X) β is-prop(x < y)

data is-accessible : X β π€ β π₯ Μ  where
next : (x : X) β ((y : X) β y < x β is-accessible y) β is-accessible x

accessible-induction : (P : (x : X) β is-accessible x β π¦ Μ )
β ((x : X) (Ο : (y : X) β y < x β is-accessible y)
β ((y : X) (l : y < x) β P y (Ο y l))
β P x (next x Ο))
β (x : X) (a : is-accessible x) β P x a
accessible-induction P step = h
where
h : (x : X) (a : is-accessible x) β P x a
h x (next .x Ο) = step x Ο (Ξ» y l β h y (Ο y l))

prev : (x : X) β is-accessible x β (y : X) β y < x β is-accessible y
prev = accessible-induction (Ξ» x _ β (y : X) β y < x β is-accessible y)
(Ξ» x Ο f β Ο)

prev-behaviour : (x : X) (a : is-accessible x) β next x (prev x a) β‘ a
prev-behaviour = accessible-induction _ (Ξ» _ _ _ β refl)

prev-behaviour' : (x : X) (Ο : (y : X) β y < x β is-accessible y) β prev x (next x Ο) β‘ Ο
prev-behaviour' x Ο = refl

transfinite-induction' :  (P : X β π¦ Μ )
β ((x : X) β (β(y : X) β y < x β P y) β P x)
β (x : X) β is-accessible x β P x
transfinite-induction' P f = accessible-induction (Ξ» x _ β P x)
(Ξ» x _ β f x)

is-well-founded : π€ β π₯ Μ
is-well-founded = (x : X) β is-accessible x

Well-founded : π€ β π₯ β π¦  βΊ Μ
Well-founded {π¦} = (P : X β π¦ Μ ) β ((x : X) β ((y : X) β y < x β P y) β P x)
β (x : X) β P x

transfinite-induction : is-well-founded β β {π¦} β Well-founded {π¦}
transfinite-induction w P f x = transfinite-induction' P f x (w x)

transfinite-induction-converse : Well-founded {π€ β π₯} β is-well-founded
transfinite-induction-converse Ο = Ο is-accessible next

transfinite-recursion : is-well-founded
β β {π¦} {Y : π¦ Μ }
β ((x : X) β ((y : X) β y < x β Y) β Y) β X β Y
transfinite-recursion w {π¦} {Y} = transfinite-induction w (Ξ» x β Y)

is-transitive : π€ β π₯ Μ
is-transitive = (x y z : X) β x < y β y < z β x < z

_βΌ_ : X β X β π€ β π₯ Μ
x βΌ y = β u β u < x β u < y

βΌ-prop-valued-order : FunExt β is-prop-valued β (x y : X) β is-prop(x βΌ y)
βΌ-prop-valued-order fe isp x y = Ξ -is-prop (fe π€ π₯)
(Ξ» u β Ξ -is-prop (fe π₯ π₯) (Ξ» l β isp u y))

βΌ-refl : {x : X} β x βΌ x
βΌ-refl u l = l

βΌ-trans : {x y z : X} β x βΌ y β y βΌ z β x βΌ z
βΌ-trans f g u l = g u (f u l)

is-extensional : π€ β π₯ Μ
is-extensional = (x y : X) β x βΌ y β y βΌ x β x β‘ y

is-extensional' : π€ β π₯ Μ
is-extensional' = (x y : X) β ((u : X) β (u < x) β (u < y)) β x β‘ y

extensional-gives-extensional' : is-extensional β is-extensional'
extensional-gives-extensional' e x y f = e x y (Ξ» u l β prβ (f u) l)
(Ξ» u l β prβ (f u) l)

extensional'-gives-extensional : is-extensional' β is-extensional
extensional'-gives-extensional e' x y g h = e' x y (Ξ» u β (g u , h u))

\end{code}

The HoTT Book additionally requires that the underlying type is a set
in the following definition, but this actually follows from the
extensionality condition (see below):

\begin{code}

is-well-order : π€ β π₯ Μ
is-well-order = is-prop-valued Γ is-well-founded Γ is-extensional Γ is-transitive

prop-valuedness : is-well-order β is-prop-valued
prop-valuedness (p , w , e , t) = p

well-foundedness : is-well-order β is-well-founded
well-foundedness (p , w , e , t) = w

extensionality : is-well-order β is-extensional
extensionality (p , w , e , t) = e

transitivity : is-well-order β is-transitive
transitivity (p , w , e , t) = t

accessibility-is-a-prop : FunExt
β (x : X) β is-prop(is-accessible x)
accessibility-is-a-prop fe = accessible-induction P Ο
where
P : (x : X) β is-accessible x β π€ β π₯ Μ
P x a = (b : is-accessible x) β a β‘ b

Ο : (x : X) (Ο : (y : X) β y < x β is-accessible y)
β ((y : X) (l : y < x) (a : is-accessible y) β Ο y l β‘ a)
β (b : is-accessible x) β next x Ο β‘ b
Ο x Ο IH b = next x Ο β‘β¨ ap (next x)
(dfunext (fe π€ (π€ β π₯)) (Ξ» y β dfunext (fe π₯ (π€ β π₯)) (h y))) β©
next x Ο β‘β¨ prev-behaviour x b β©
b β
where
Ο : (y : X) (l : y < x) β is-accessible y
Ο = prev x b
h :  (y : X) (l : y < x) β Ο y l β‘ Ο y l
h y l = IH y l (Ο y l)

well-foundedness-is-a-prop : FunExt β is-prop is-well-founded
well-foundedness-is-a-prop fe = Ξ -is-prop (fe π€ (π€ β π₯)) (accessibility-is-a-prop fe)

extensionally-ordered-types-are-sets : FunExt β is-prop-valued
β is-extensional β is-set X
extensionally-ordered-types-are-sets fe isp e = Id-collapsibles-are-sets (f , ΞΊ)
where
f : {x y :  X} β x β‘ y β x β‘ y
f {x} {y} p = e x y (transport (Ξ» - β x βΌ -) p (βΌ-refl {x}))
(transport (Ξ» - β - βΌ x) p (βΌ-refl {x}))
ec : {x y : X} {l l' : x βΌ y} {m m' : y βΌ x} β e x y l m β‘ e x y l' m'
ec {x} {y} {l} {l'} {m} {m'} = apβ (e x y) (βΌ-prop-valued-order fe isp x y l l')
(βΌ-prop-valued-order fe isp y x m m')
ΞΊ : {x y : X} β constant (f {x} {y})
ΞΊ p q = ec

well-ordered-types-are-sets : FunExt β is-well-order β is-set X
well-ordered-types-are-sets fe (p , w , e , t) = extensionally-ordered-types-are-sets fe p e

extensionality-is-a-prop : FunExt β is-prop-valued β is-prop is-extensional
extensionality-is-a-prop fe isp e e' =
dfunext (fe π€ (π€ β π₯))
(Ξ» x β dfunext (fe π€ (π€ β π₯))
(Ξ» y β Ξ -is-prop (fe (π€ β π₯) (π€ β π₯))
(Ξ» l β Ξ -is-prop (fe (π€ β π₯) π€)
(Ξ» m β extensionally-ordered-types-are-sets fe isp e))
(e x y)
(e' x y)))

transitivity-is-a-prop : FunExt β is-prop-valued β is-prop is-transitive
transitivity-is-a-prop fe isp =
Ξ -is-prop (fe π€ (π€ β π₯))
(Ξ» x β Ξ -is-prop (fe π€ (π€ β π₯))
(Ξ» y β Ξ -is-prop (fe π€ π₯)
(Ξ» z β Ξ -is-prop (fe π₯ π₯)
(Ξ» l β Ξ -is-prop (fe π₯ π₯)
(Ξ» m β isp x z)))))

being-well-order-is-a-prop : FunExt β is-prop is-well-order
being-well-order-is-a-prop fe o = Γ-is-prop (Ξ -is-prop (fe π€ (π€ β π₯))
Ξ» x β Ξ -is-prop (fe π€ π₯)
(Ξ» y β being-a-prop-is-a-prop (fe π₯ π₯)))
(Γ-is-prop (well-foundedness-is-a-prop fe)
(Γ-is-prop (extensionality-is-a-prop fe (prβ o))
(transitivity-is-a-prop fe (prβ o))))
o

_β€_ : X β X β π₯ Μ
x β€ y = Β¬(y < x)

is-top : X β π€ β π₯ Μ
is-top x = (y : X) β y β€ x

has-top : π€ β π₯ Μ
has-top = Ξ£ \(x : X) β is-top x

<-coarser-than-β€  : (x : X) β is-accessible x β β y β y < x β y β€ x
<-coarser-than-β€ = transfinite-induction'
(Ξ» x β (y : X) β y < x β y β€ x)
(Ξ» x f y l m β f y l x m l)

β€-refl : (x : X) β is-accessible x β x β€ x
β€-refl x a l = <-coarser-than-β€ x a x l l

non-strict-trans : (z : X) β is-accessible z
β (x y : X) β x < y β y < z β x β€ z
non-strict-trans = transfinite-induction'
(Ξ» z β (x y : X) β x < y β y < z β x β€ z)
(Ξ» z f x y l m n β f y m z x n l m)

<-coarser-than-βΌ : is-transitive β {x y : X} β x < y β x βΌ y
<-coarser-than-βΌ t {x} {y} l u m = t u x y m l

βΌ-coarser-than-β€ : (y : X) β is-accessible y β (x : X) β x βΌ y β x β€ y
βΌ-coarser-than-β€ y a x f l = β€-refl y a (f y l)

trichotomous : π€ β π₯ Μ
trichotomous = (x y : X) β (x < y) + (x β‘ y) + (y < x)

\end{code}

When do we get x β€ y β x βΌ y (say for ordinals)? When do we get
cotransitivity? Jean S. Josef observed that cotransitivity gives x β€ y
β x βΌ y if _<_ is an order. But cotransitivity alone is enough.

Or consider the truncated version of the following, if _<_ is
proposition valued.

\begin{code}

cotransitive : π€ β π₯ Μ
cotransitive = (x y z : X) β x < y β x < z + z < y

cotransitive-β€-coarser-than-βΌ : cotransitive β (x y : X) β x β€ y β x βΌ y
cotransitive-β€-coarser-than-βΌ c x y n u l = Ξ³ (c u x y l)
where
Ξ³ : (u < y) + (y < x) β u < y
Ξ³ (inl l) = l
Ξ³ (inr l) = π-elim (n l)

no-minimal-is-empty : is-well-founded
β β {π¦} (P : X β π¦ Μ )
β ((x : X) β P x β Ξ£ \(y : X) β (y < x) Γ P y)
β is-empty(Ξ£ P)
no-minimal-is-empty w P s (x , p) = f s x p
where
f : ((x : X) β P x β Ξ£ \(y : X) β (y < x) Γ P y) β (x : X) β Β¬(P x)
f s x p = g x (w x) p
where
g : (x : X) β is-accessible x β Β¬(P x)
g x (next .x Ο) p = IH (prβ (s x p)) (prβ(prβ(s x p))) (prβ(prβ(s x p)))
where
IH : (y : X) β y < x β Β¬(P y)
IH y l = g y (Ο y l)

NB : Ξ£ P β Β¬((x : X) β P x β Ξ£ \(y : X) β (y < x) Γ P y)
NB (x , p) s = f s x p

\end{code}

Originally we needed the following weakening of well-foundedness
(transfinite induction for detachable subsets), but now it is not
needed any longer:

\begin{code}

is-well-foundedβ : π€ β π₯ Μ
is-well-foundedβ = (p : X β π) β ((x : X) β ((y : X) β y < x β p y β‘ β) β p x β‘ β)
β (x : X) β p x β‘ β

well-founded-Wellfoundedβ : is-well-founded β is-well-foundedβ
well-founded-Wellfoundedβ w p = transfinite-induction w (Ξ» x β p x β‘ β)

open import UF-Miscelanea

being-well-foundedβ-is-a-prop : FunExt β is-prop is-well-foundedβ
being-well-foundedβ-is-a-prop fe = Ξ -is-prop (fe π€ (π€ β π₯))
(Ξ» p β Ξ -is-prop (fe (π€ β π₯) π€)
(Ξ» s β Ξ -is-prop (fe π€ π€β) (Ξ» x β π-is-set)))

is-well-orderβ : π€ β π₯ Μ
is-well-orderβ = is-prop-valued Γ is-well-foundedβ Γ is-extensional Γ is-transitive

is-well-order-gives-is-well-orderβ : is-well-order β is-well-orderβ
is-well-order-gives-is-well-orderβ (p , w , e , t) = p , (well-founded-Wellfoundedβ w) , e , t

being-well-orderβ-is-a-prop : FunExt β is-prop-valued β is-prop is-well-orderβ
being-well-orderβ-is-a-prop fe isp = Γ-is-prop (Ξ -is-prop (fe π€ (π€ β π₯))
(Ξ» x β Ξ -is-prop (fe π€ π₯)
(Ξ» y β being-a-prop-is-a-prop (fe π₯ π₯))))
(Γ-is-prop (being-well-foundedβ-is-a-prop fe)
(Γ-is-prop (extensionality-is-a-prop fe isp)
(transitivity-is-a-prop fe isp)))

\end{code}

Experimental ideas. We don't truncate the Ξ£, at least not for the
moment, so x <β y won't be a proposition (i.e. subsingleton) in
general. However, given π-order-separation, this is logically
equivalent to a proposition (has split support).

\begin{code}

open import Two-Properties

_βΊβ_ : X β X β π€ β π₯ Μ
x βΊβ y = Ξ£ \(p : X β π) β (p x <β p y)
Γ ((u v : X) β (u < v β p u β€β p v)
Γ (p u <β p v β u < v))

βΊβ-courser-than-< : (x y : X) β x βΊβ y β x < y
βΊβ-courser-than-< x y (p , l , Ο) = prβ(Ο x y) l

π-order-separated : π€ β π₯ Μ
π-order-separated = (x y : X) β x < y β x βΊβ y

open import DiscreteAndSeparated

π-order-separated-gives-cotransitive : π-order-separated β cotransitive
π-order-separated-gives-cotransitive s x y z l = g (s x y l)
where
g : (Ξ£ \(p : X β π) β (p x <β p y)
Γ ((u v : X) β (u < v β p u β€β p v)
Γ (p u <β p v β u < v)))
β (x < z) + (z < y)
g (p , (r , s) , Ο) = Cases (π-is-discrete (p z) β)
(Ξ» (t : p z β‘ β)
β inr (prβ (Ο z y) (t , s)))
(Ξ» (t : Β¬(p z β‘ β))
β inl (prβ (Ο x z) (r , (different-from-β-equal-β t))))

\end{code}

It seems that this is not going to be useful, because although ββ
satisfies this property, the property doesn't seem to be preserved by