Martin Escardo, April 2013, adapted to this development June 2018,
with further additions.

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
the lexicographic order (think about this).