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 --auto-inline #-}

open import MLTT.Spartan
open import TypeTopology.DiscreteAndSeparated

open import UF.Base
open import UF.Subsingletons
open import UF.FunExt
open import UF.Subsingletons-FunExt
open import UF.ExcludedMiddle
open import UF.PropTrunc
open import MLTT.Plus-Properties using (+-commutative)

module Ordinals.Notions
        {𝓀 π“₯ : Universe}
        {X : 𝓀 Μ‡ }
        (_<_ : X β†’ X β†’ π“₯ Μ‡ )
       where

is-prop-valued : 𝓀 βŠ” π“₯ Μ‡
is-prop-valued = (x y : X) β†’ is-prop (x < y)

data is-accessible : X β†’ 𝓀 βŠ” π“₯ Μ‡ where
 step : {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 (step Οƒ))
                     β†’ (x : X) (a : is-accessible x) β†’ P x a
accessible-induction P f = h
  where
   h : (x : X) (a : is-accessible x) β†’ P x a
   h x (step Οƒ) = f x Οƒ (Ξ» y l β†’ h y (Οƒ y l))

prev : {x : X}
     β†’ is-accessible x
     β†’ (y : X) β†’ y < x β†’ is-accessible y
prev (step a) = a

prev-behaviour : (x : X) (a : is-accessible x)
               β†’ step (prev a) ＝ a
prev-behaviour = accessible-induction _ (Ξ» _ _ _ β†’ 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)

\end{code}

Added 31 October 2022 by Tom de Jong.
We record the (computational) behaviour of transfinite induction for use in
other constructions.

\begin{code}

transfinite-induction'-behaviour :
   (P : X β†’ 𝓦 Μ‡ ) (f : (x : X) β†’ ((y : X) β†’ y < x β†’ P y) β†’ P x)
   (x : X) (a : is-accessible x)
 β†’ transfinite-induction' P f x a
   ＝ f x (Ξ» y l β†’ transfinite-induction' P f y (prev a y l))
transfinite-induction'-behaviour P f x (step Οƒ) = refl

\end{code}

End of addition.

\begin{code}

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 (Ξ» _ β†’ step)

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)

accessibility-is-prop : FunExt
                      β†’ (x : X) β†’ is-prop (is-accessible x)
accessibility-is-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) β†’ step Οƒ ＝ b
  Ο† x Οƒ IH b = step Οƒ ＝⟨ i ⟩
               step Ο„ ＝⟨ prev-behaviour x b ⟩
               b      ∎
   where
    Ο„ : (y : X) β†’ y < x β†’ is-accessible y
    Ο„ = prev b

    h :  (y : X) (l : y < x) β†’ Οƒ y l ＝ Ο„ y l
    h y l = IH y l (Ο„ y l)

    i = ap step
           (dfunext (fe 𝓀 (𝓀 βŠ” π“₯)) (Ξ» y β†’ dfunext (fe π“₯ (𝓀 βŠ” π“₯)) (h y)))

\end{code}

Added 31 October 2022 by Tom de Jong.
We record the (computational) behaviour of transfinite induction/recursion for
use in other constructions.

\begin{code}

transfinite-induction-behaviour : FunExt β†’ (w : is-well-founded)
                                  {𝓦 : Universe} (P : X β†’ 𝓦 Μ‡ )
                                  (f : (x : X) β†’ ((y : X) β†’ y < x β†’ P y) β†’ P x)
                                  (x : X)
                                β†’ transfinite-induction w P f x
                                  ＝ f x (Ξ» y l β†’ transfinite-induction w P f y)
transfinite-induction-behaviour fe w {𝓦} P f x =
 transfinite-induction w P f x                               ＝⟨ I    ⟩
 f x (Ξ» y l β†’ transfinite-induction' P f y (prev (w x) y l)) ＝⟨ II   ⟩
 f x (Ξ» y l β†’ transfinite-induction' P f y (w y))            ＝⟨ refl ⟩
 f x (Ξ» y l β†’ transfinite-induction w P f y)                 ∎
  where
   I = transfinite-induction'-behaviour P f x (w x)
   II = ap (f x) (dfunext (fe 𝓀 (π“₯ βŠ” 𝓦))
                          (Ξ» y β†’ dfunext (fe π“₯ 𝓦)
                                         (Ξ» l β†’ ap (transfinite-induction' P f y) (e y l))))
    where
     e : (y : X) (l : y < x) β†’ prev (w x) y l ＝ w y
     e y l = accessibility-is-prop fe y (prev (w x) y l) (w y)

transfinite-recursion-behaviour : FunExt
                                β†’ (w : is-well-founded)
                                  {𝓦 : Universe} {Y : 𝓦 Μ‡ }
                                  (f : (x : X) β†’ ((y : X) β†’ y < x β†’ Y) β†’ Y)
                                  (x : X)
                                β†’ transfinite-recursion w f x
                                  ＝ f x (Ξ» y _ β†’ transfinite-recursion w f y)
transfinite-recursion-behaviour fe w {𝓦} {Y} =
 transfinite-induction-behaviour fe w (Ξ» _ β†’ Y)

\end{code}

End of addition.

\begin{code}

is-transitive : 𝓀 βŠ” π“₯ Μ‡
is-transitive = (x y z : X) β†’ x < y β†’ y < z β†’ x < z

private
  _β‰Ό_ : X β†’ X β†’ 𝓀 βŠ” π“₯ Μ‡
  x β‰Ό y = βˆ€ u β†’ u < x β†’ u < y

extensional-po = _β‰Ό_

extensional-po-is-prop-valued : FunExt
                              β†’ is-prop-valued
                              β†’ (x y : X) β†’ is-prop (x β‰Ό y)
extensional-po-is-prop-valued fe isp x y =
  Ξ β‚‚-is-prop (Ξ» {𝓀} {π“₯} β†’ fe 𝓀 π“₯) (Ξ» u 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

well-foundedness-is-prop : FunExt β†’ is-prop is-well-founded
well-foundedness-is-prop fe = Ξ -is-prop (fe 𝓀 (𝓀 βŠ” π“₯))
                               (accessibility-is-prop fe)

extensionally-ordered-types-are-sets : FunExt
                                     β†’ is-prop-valued
                                     β†’ is-extensional
                                     β†’ is-set X
extensionally-ordered-types-are-sets fe isp e = Ξ³
 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)
                                     (extensional-po-is-prop-valued fe isp x y l l')
                                     (extensional-po-is-prop-valued fe isp y x m m')

  ΞΊ : {x y : X} β†’ wconstant (f {x} {y})
  ΞΊ p q = ec

  Ξ³ : is-set X
  Ξ³ = Id-collapsibles-are-sets (f , ΞΊ)

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-prop : FunExt β†’ is-prop-valued β†’ is-prop is-extensional
extensionality-is-prop fe isp e e' =
 dfunext (fe 𝓀 (𝓀 βŠ” π“₯))
   (Ξ» x β†’ dfunext (fe 𝓀 (𝓀 βŠ” π“₯))
           (Ξ» y β†’ Ξ β‚‚-is-prop (Ξ» {𝓀} {π“₯} β†’ fe 𝓀 π“₯)
                    (Ξ» l m β†’ extensionally-ordered-types-are-sets fe isp e)
                    (e x y)
                    (e' x y)))

transitivity-is-prop : FunExt β†’ is-prop-valued β†’ is-prop is-transitive
transitivity-is-prop fe isp = Ξ β‚…-is-prop (Ξ» {𝓀} {π“₯} β†’ fe 𝓀 π“₯)
                               (Ξ» x y z l m β†’ isp x z)

being-well-order-is-prop : FunExt β†’ is-prop is-well-order
being-well-order-is-prop fe = prop-criterion Ξ³
 where
  Ξ³ : is-well-order β†’ is-prop is-well-order
  Ξ³ o = Γ—β‚„-is-prop (Ξ β‚‚-is-prop ((Ξ» {𝓀} {π“₯} β†’ fe 𝓀 π“₯))
                      (Ξ» x y β†’ being-prop-is-prop (fe π“₯ π“₯)))
                   (well-foundedness-is-prop fe)
                   (extensionality-is-prop fe (prop-valuedness o))
                   (transitivity-is-prop fe (prop-valuedness o))

private
 _β‰Ύ_ : X β†’ X β†’ π“₯ Μ‡
 x β‰Ύ y = Β¬ (y < x)

β‰Ύ-is-prop-valued : funext π“₯ 𝓀₀ β†’ is-prop-valued β†’ (x y : X) β†’ is-prop (x β‰Ύ y)
β‰Ύ-is-prop-valued fe p x y = negations-are-props fe

<-gives-β‰Ύ  : (x : X)
           β†’ is-accessible x
           β†’ (y : X) β†’ y < x β†’ y β‰Ύ x
<-gives-β‰Ύ = 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 = <-gives-β‰Ύ x a x l l

irreflexive : (x : X) β†’ is-accessible x β†’ Β¬ (x < x)
irreflexive = β‰Ύ-refl

<-gives-β‰  : is-well-founded
          β†’ (x y : X) β†’ x < y β†’ x β‰  y
<-gives-β‰  w x y l p = irreflexive y (w y) (transport (_< y) p l)

<-gives-β‰Ό : is-transitive β†’ {x y : X} β†’ x < y β†’ x β‰Ό y
<-gives-β‰Ό 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)

is-bot : X β†’ 𝓀 βŠ” π“₯ Μ‡
is-bot x = (y : X) β†’ x β‰Ύ y

is-bot' : X β†’ 𝓀 βŠ” π“₯ Μ‡
is-bot' x = (y : X) β†’ x β‰Ό y

is-bot'-gives-is-bot : is-well-founded β†’ (x : X) β†’ is-bot' x β†’ is-bot x
is-bot'-gives-is-bot w x i y = β‰Ό-coarser-than-β‰Ύ y (w y) x (i y)

is-bot-gives-is-bot' : (x : X) β†’ is-bot x β†’ is-bot' x
is-bot-gives-is-bot' x i y z l = 𝟘-elim (i z l)

is-top : X β†’ 𝓀 βŠ” π“₯ Μ‡
is-top x = (y : X) β†’ y β‰Ύ x

is-top' : X β†’ 𝓀 βŠ” π“₯ Μ‡
is-top' x = (y : X) β†’ y β‰Ό x

is-top'-gives-is-top : is-well-founded β†’ (x : X) β†’ is-top' x β†’ is-top x
is-top'-gives-is-top w x i y = β‰Ό-coarser-than-β‰Ύ x (w x) y (i y)

\end{code}

There is no hope of proving the converse constructively, because in
the ordinal of truth values any ¬¬-dense truth-value p satisfies
is-top p, and the only truth-value that satisfies is-top is ⊀. See the
module OrdinalOfTruthValues.

\begin{code}

has-top : 𝓀 βŠ” π“₯ Μ‡
has-top = Ξ£ x κž‰ X , is-top x

no-minimal-is-empty : is-well-founded
                    β†’ βˆ€ {𝓦} (A : X β†’ 𝓦 Μ‡ )
                    β†’ ((x : X) β†’ A x β†’ is-nonempty (Ξ£ y κž‰ X , (y < x) Γ— A y))
                    β†’ is-empty (Ξ£ A)
no-minimal-is-empty w A s (x , aβ‚€) = Ξ³
 where
  g : (x : X) β†’ is-accessible x β†’ Β¬ (A x)
  g x (step Οƒ) Ξ½ = Ξ΄
   where
    h : ¬¬ (Ξ£ y κž‰ X , (y < x) Γ— A y)
    h = s x Ξ½

    IH : (y : X) β†’ y < x β†’ Β¬ (A y)
    IH y l = g y (Οƒ y l)

    k : Β¬ (Ξ£ y κž‰ X , (y < x) Γ— A y)
    k (y , l , a) = IH y l a

    δ : 𝟘
    Ξ΄ = h k

  f : ((x : X) β†’ A x β†’ ¬¬ (Ξ£ y κž‰ X , (y < x) Γ— A y))
    β†’ (x : X) β†’ Β¬ (A x)
  f s x = g x (w x)

  γ : 𝟘
  Ξ³ = f s x aβ‚€

no-minimal-is-empty' : is-well-founded
                     β†’ βˆ€ {𝓦} (A : X β†’ 𝓦 Μ‡ )
                     β†’ ((x : X) β†’ A x β†’ Ξ£ y κž‰ X , (y < x) Γ— A y)
                     β†’ is-empty (Ξ£ A)
no-minimal-is-empty' w A s = no-minimal-is-empty w A (Ξ» x a β†’ ¬¬-intro (s x a))

\end{code}


The emptiness of the empty set doesn't play any special role in the
above argument, and can be replaced by any type - would that be
useful?

\begin{code}

in-trichotomy : (x y : X) β†’ 𝓀 βŠ” π“₯ Μ‡
in-trichotomy x y = (x < y) + (x ＝ y) + (y < x)

is-trichotomous-element : X β†’ 𝓀 βŠ” π“₯ Μ‡
is-trichotomous-element x = (y : X) β†’ in-trichotomy x y

is-trichotomous-order : 𝓀 βŠ” π“₯ Μ‡
is-trichotomous-order = (x : X) β†’ is-trichotomous-element x

-- injections into in-trichotomy
>-implies-in-trichotomy : {x y : X} β†’ (x < y) β†’ in-trichotomy x y
>-implies-in-trichotomy = inl

＝-implies-in-trichotomy : {x y : X} β†’ (x ＝ y) β†’ in-trichotomy x y
＝-implies-in-trichotomy = inr ∘ inl

<-implies-in-trichotomy : {x y : X} β†’ (y < x) β†’ in-trichotomy x y
<-implies-in-trichotomy = inr ∘ inr

in-trichotomy-symm : {x y : X} β†’ in-trichotomy x y β†’ in-trichotomy y x
in-trichotomy-symm (inl x-lt-y) = inr (inr x-lt-y)
in-trichotomy-symm (inr (inl x-equiv-y)) = inr (inl (x-equiv-y ⁻¹))
in-trichotomy-symm (inr (inr y-lt-x)) = inl y-lt-x

_>_ : (x y : X) β†’ π“₯ Μ‡
x > y = y < x

_≦_ : (x y : X) β†’ 𝓀 βŠ” π“₯ Μ‡
x ≦ y = (x < y) + (y ＝ x)

_≧_ : (x y : X) β†’ 𝓀 βŠ” π“₯ Μ‡
x ≧ y = (x ＝ y) + (y < x)

≧-implies-≦ : {x y : X} β†’ x ≧ y β†’ y ≦ x
≧-implies-≦ x-geq-y = +-commutative x-geq-y

≦-implies-≧ : {x y : X} β†’ x ≦ y β†’ y ≧ x
≦-implies-≧ x-leq-y = +-commutative x-leq-y

≧-implies-in-trichotomy : {x y : X} β†’ x ≧ y β†’ in-trichotomy x y
≧-implies-in-trichotomy = inr

≦-implies-in-trichotomy : {x y : X} β†’ x ≦ y β†’ in-trichotomy x y
≦-implies-in-trichotomy = cases inl (＝-implies-in-trichotomy ∘ _⁻¹)

in-trichotomy-not->-implies-≦ : {x y : X} β†’ in-trichotomy x y β†’ Β¬ (y < x) β†’ x ≦ y
in-trichotomy-not->-implies-≦ (inl x-lt-y) y-not-lt-x = inl x-lt-y
in-trichotomy-not->-implies-≦ (inr (inl x-equals-y)) y-not-lt-x = inr (x-equals-y ⁻¹)
in-trichotomy-not->-implies-≦ (inr (inr y-lt-x)) y-not-lt-x = 𝟘-elim (y-not-lt-x y-lt-x)

in-trichotomy-not->-implies-≧ : {x y : X} β†’ in-trichotomy x y β†’ Β¬ (x < y) β†’ x ≧ y
in-trichotomy-not->-implies-≧ x-in-trichotomy-y y-not-lt-x =
  ≦-implies-≧ (in-trichotomy-not->-implies-≦
                 (in-trichotomy-symm x-in-trichotomy-y)
                 y-not-lt-x)

≧->-transitive : is-well-order β†’ {x y z : X} β†’ (x ≧ y) β†’ (z < y) β†’ z < x
≧->-transitive wo {x} {y} {z} (inl refl) y-gt-z = y-gt-z
≧->-transitive wo@(p , w , e , t) {x} {y} {z} (inr x-gt-y) y-gt-z = t z y x y-gt-z x-gt-y

>-≧-transitive : is-well-order β†’ {x y z : X} β†’ (y < x) β†’ (y ≧ z) β†’ z < x
>-≧-transitive wo {x} {y} {.y} x-gt-y (inl refl) = x-gt-y
>-≧-transitive wo@(p , w , e , t) {x} {y} {z} x-gt-y (inr y-gt-z) = t z y x y-gt-z x-gt-y

module _ (fe : FunExt) (wo : is-well-order) where
  private
    X-is-set : is-set X
    X-is-set = well-ordered-types-are-sets fe wo

  ≦-is-prop : (x y : X) β†’ is-prop (x ≦ y)
  ≦-is-prop x y = sum-of-contradictory-props (prop-valuedness wo x y)
    X-is-set
    Ξ» x-lt-y x-equals-y β†’ irreflexive y (well-foundedness wo y)
      (transport (_< y) (x-equals-y ⁻¹) x-lt-y)

  ≧-is-prop : (x y : X) β†’ is-prop (x ≧ y)
  ≧-is-prop x y = sum-of-contradictory-props
    (well-ordered-types-are-sets fe wo)
    (prop-valuedness wo y x)
    Ξ» x-equals-y x-gt-y β†’ irreflexive x (well-foundedness wo x)
      (transport (_< x) (x-equals-y ⁻¹) x-gt-y)

  in-trichotomy-is-prop : (x y : X) β†’ is-prop (in-trichotomy x y)
  in-trichotomy-is-prop x y =
    sum-of-contradictory-props (prop-valuedness wo x y) (≧-is-prop x y)
      Ξ» x-lt-y  x-geq-y β†’ irreflexive x (well-foundedness wo x)
        (≧->-transitive wo x-geq-y x-lt-y)

  being-trichotomous-element-is-prop : (x : X) β†’ is-prop (is-trichotomous-element x)
  being-trichotomous-element-is-prop x =
    Ξ -is-prop (fe 𝓀 (𝓀 βŠ” π“₯))
     (Ξ» y β†’ in-trichotomy-is-prop x y)

  trichotomy-is-prop : is-prop (is-trichotomous-order)
  trichotomy-is-prop = Ξ -is-prop (fe 𝓀 (𝓀 βŠ” π“₯))
                         being-trichotomous-element-is-prop

\end{code}

Not all ordinals are trichotomous, in the absence of excluded middle
or even just LPO, because β„•βˆž is not discrete unless LPO holds, but its
natural order is well-founded, and types with well-founded trichotomous
relations are discrete (have decidable equality):

\begin{code}

trichotomous-gives-discrete : is-well-founded
                            β†’ is-trichotomous-order
                            β†’ is-discrete X
trichotomous-gives-discrete w t x y = f (t x y)
 where
  f : (x < y) + (x ＝ y) + (y < x) β†’ (x ＝ y) + (x β‰  y)
  f (inl l)       = inr (<-gives-β‰  w x y l)
  f (inr (inl p)) = inl p
  f (inr (inr l)) = inr (β‰ -sym (<-gives-β‰  w y x l))

\end{code}

The following proof that excluded middle gives trichotomy, added 11th
Jan 2021, is the same as that in the HoTT book, except that we use
negation instead of the assumption of existence of propositional
truncations to get a proposition to which we can apply excluded
middle.  But notice that, under excluded middle and function
extensionality, double negation is the same thing as propositional
truncation. Notice also we additionally need function extensionality
as an assumption (to know that the negation of a type is a
proposition).

There is also a shorter proof below that uses the existence of
propositional truncations (but seems different to the proof of the
HoTT book).

\begin{code}
trichotomy : funext (𝓀 βŠ” π“₯) 𝓀₀
           β†’ excluded-middle (𝓀 βŠ” π“₯)
           β†’ is-well-order
           β†’ is-trichotomous-order
trichotomy fe em (p , w , e , t) = Ξ³
 where
  P : X β†’ X β†’ 𝓀 βŠ” π“₯ Μ‡
  P x y = (x < y) + (x ＝ y) + (y < x)

  Ξ³ : (x y : X) β†’ P x y
  Ξ³ = transfinite-induction w (Ξ» x β†’ βˆ€ y β†’ P x y) Ο•
   where
    Ο• : (x : X)
      β†’ ((x' : X) β†’ x' < x β†’ (y : X) β†’ P x' y)
      β†’ (y : X) β†’ P x y
    Ο• x IH-x = transfinite-induction w (Ξ» y β†’ P x y) ψ
     where
      ψ : (y : X)
        β†’ ((y' : X) β†’ y' < y β†’ P x y')
        β†’ P x y
      ψ y IH-y = δ
       where
        A = Ξ£ x' κž‰ X , (x' < x) Γ— ((y < x') + (x' ＝ y))

        ¬¬A-gives-P : ¬¬ A β†’ P x y
        ¬¬A-gives-P = b
         where
          a : A β†’ y < x
          a (x' , l , inl m) = t y x' x m l
          a (x' , l , inr p) = transport (_< x) p l

          b : ¬¬ A β†’ (x < y) + (x ＝ y) + (y < x)
          b = inr ∘ inr ∘ EM-gives-DNE (lower-EM 𝓀 em) (y < x) (p y x) ∘ ¬¬-functor a

        Β¬A-gives-β‰Ό : Β¬ A β†’ x β‰Ό y
        Β¬A-gives-β‰Ό Ξ½ x' l = d
         where
          a : ¬ ((y < x') + (x' ＝ y))
          a f = Ξ½ (x' , l , f)

          b : P x' y
          b = IH-x x' l y

          c : Β¬ ((y < x') + (x' ＝ y)) β†’ P x' y β†’ x' < y
          c g (inl i)         = i
          c g (inr (inl ii))  = 𝟘-elim (g (inr ii))
          c g (inr (inr iii)) = 𝟘-elim (g (inl iii))

          d : x' < y
          d = c a b

        B = Ξ£ y' κž‰ X , (y' < y) Γ— ((x < y') + (x ＝ y'))

        ¬¬B-gives-P : ¬¬ B β†’ P x y
        ¬¬B-gives-P = b
         where
          a : B β†’ x < y
          a (y' , l , inl m) = t x y' y m l
          a (y' , l , inr p) = transport (_< y) (p ⁻¹) l

          b : ¬¬ B β†’ (x < y) + (x ＝ y) + (y < x)
          b = inl ∘ EM-gives-DNE (lower-EM 𝓀 em) (x < y) (p x y) ∘ ¬¬-functor a

        Β¬B-gives-β‰Ό : Β¬ B β†’ y β‰Ό x
        Β¬B-gives-β‰Ό Ξ½ y' l = d
         where
          a : ¬ ((x < y') + (x ＝ y'))
          a f = Ξ½ (y' , l , f)

          b : P x y'
          b = IH-y y' l

          c : Β¬ ((x < y') + (x ＝ y')) β†’ P x y' β†’ y' < x
          c g (inl i)         = 𝟘-elim (g (inl i))
          c g (inr (inl ii))  = 𝟘-elim (g (inr ii))
          c g (inr (inr iii)) = iii

          d : y' < x
          d = c a b

        Β¬A-and-Β¬B-give-P : Β¬ A β†’ Β¬ B β†’ P x y
        Β¬A-and-Β¬B-give-P Ξ½ Ξ½' = b
         where
          a : Β¬ A β†’ Β¬ B β†’ x ＝ y
          a Ξ½ Ξ½' = e x y (Β¬A-gives-β‰Ό Ξ½) (Β¬B-gives-β‰Ό Ξ½')

          b : (x < y) + (x ＝ y) + (y < x)
          b = inr (inl (a Ξ½ Ξ½'))

        Ξ΄ : P x y
        Ξ΄ = Cases (em (Β¬ A) (negations-are-props fe))
             (Ξ» (Ξ½ : Β¬ A)
                   β†’ Cases (em (Β¬ B) (negations-are-props fe))
                      (Β¬A-and-Β¬B-give-P Ξ½)
                      ¬¬B-gives-P)
             ¬¬A-gives-P
\end{code}

Added 09-04-2022 -- 04-05-2022 by Ohad Kammar.

We can give a shorter proof using `βˆƒΒ¬-gives-βˆ€` and LEM, by deducing
that in a well-order, for every u and v, either u β‰Ό v or there is some
i < u for which Β¬ (i < v).

Like the HoTT proof, we nest two inductions, the outer one that every
element is trichotomous, and the inner one that the currently
considered outer element u is in trichotomy with the currently
considered inner element v.

The crucial observation (`lemma`) is that, under the outer induction
hypothesis for u, the relations (_β‰Ό u) and (_≦ u) coincide. We prove
this observation by appealing to LEM to get that either u β‰Ό x or there
is a witness i < u but Β¬ (i < x). The former means (by extensionality)
that u ＝ x. In the latter case, the witness i satisfies the induction
hypothesis, and so is in trichotomy with x, which by elimination means
i >= x, so u > i >= x.

With this lemma, we can prove the inner induction step by LEM.  If v β‰Ό
u, then by the lemma v <= u and so they are in trichotomy.  Otherwise,
there is a witness i < v , Β¬ (i < u). By the induction hypothesis for
v, we have that i is in trichotomy with u, which by elimination means
i >= u, and so v > i >= u, and so u and v are again in trichotomy.

\begin{code}

induction-hypothesis : (P : X β†’ 𝓦 Μ‡ ) β†’ (x : X) β†’ (𝓀 βŠ” π“₯ βŠ” 𝓦) Μ‡
induction-hypothesis P x = (y : X) β†’ y < x β†’ P y

module _
        (f-e : Fun-Ext)
        (em : Excluded-Middle)
       where
 private
   pt : propositional-truncations-exist
   pt = fe-and-em-give-propositional-truncations (Ξ» 𝓀 π“₯ β†’ f-e {𝓀} {π“₯}) em

   fe : FunExt
   fe 𝓀 π“₯ = f-e

   open import UF.PropTrunc
   open PropositionalTruncation pt

   lem-consequence : is-well-order β†’ (u v : X) β†’ (βˆƒ i κž‰ X , ((i < u) Γ— Β¬ (i < v))) + (u β‰Ό v)
   lem-consequence (p , _) u v = Cases
     (βˆƒ-not+Ξ  pt em {Ξ£ (Ξ» i β†’ i < u)}
        (Ξ» (i , i-lt-u) β†’ i < v)
        (Ξ» (i , i-<-u) β†’ p i v))
     (Ξ» witness β†’ inl ((βˆ₯βˆ₯-induction (Ξ» s β†’ βˆƒ-is-prop)
       (Ξ» ((i , i-lt-u) , i-not-lt-v) β†’ ∣ i , i-lt-u , i-not-lt-v ∣) witness)))
     Ξ» prf β†’ inr (Ξ» i i-lt-u β†’ prf (i , i-lt-u))

 trichotomyβ‚‚ : is-well-order β†’ is-trichotomous-order
 trichotomyβ‚‚ wo@(p , w , e , t) = transfinite-induction w is-trichotomous-element Ο•
  where
   Ο• : (x : X) β†’ induction-hypothesis is-trichotomous-element x β†’ is-trichotomous-element x
   Ο• u ih = -- now we proceed by induction on the inner argument
     transfinite-induction w (in-trichotomy u) Ξ» v innerIH β†’
       -- use LEM to get either (βˆƒi<v . iβ‰―u) ∨ (v β‰Ό u)
       Cases (lem-consequence wo v u)
         (βˆ₯βˆ₯-induction (Ξ» s β†’ in-trichotomy-is-prop fe wo u v)
           Ξ» (i , i-lt-v , i-not-lt-u) β†’ inl -- show u < v
           let u-leq-i = in-trichotomy-not->-implies-≦ ((innerIH i i-lt-v)) i-not-lt-u in
           >-≧-transitive wo i-lt-v (≦-implies-≧ u-leq-i))
         Ξ» v-below-u β†’ in-trichotomy-symm (≦-implies-in-trichotomy (lemma v v-below-u))
    where
     lemma : (x : X) β†’ (x β‰Ό u) β†’ x ≦ u
     lemma x x-below-u = Cases (lem-consequence wo u x)
       (βˆ₯βˆ₯-induction (Ξ» s β†’ ≦-is-prop fe wo x u)
         Ξ» (i , i-lt-u , i-not-lt-x) β†’ inl -- show x < u
           let i-in-trichotomy-x = ih i i-lt-u x in
           (>-≧-transitive wo
             i-lt-u
             (in-trichotomy-not->-implies-≧ i-in-trichotomy-x i-not-lt-x)))
       Ξ» u-below-x β†’ inr ((e x u x-below-u u-below-x) ⁻¹)
\end{code}

End of proof added by Ohad Kammar.

The following fact and proof were communicated verbally by Paul Blain
Levy to Martin Escardo and Ohad Kammar on 16th November 2022, and it
is written down in Agda by Martin Escardo on the same date:

\begin{code}

is-decidable-order : 𝓀 βŠ” π“₯ Μ‡
is-decidable-order = (x y : X) β†’ decidable (x < y)

trichotomy-from-decidable-order : is-transitive
                                β†’ is-extensional
                                β†’ is-well-founded
                                β†’ is-decidable-order
                                β†’ is-trichotomous-order
trichotomy-from-decidable-order t e w d = Ξ³
 where
  T : X β†’ X β†’ 𝓀 βŠ” π“₯ Μ‡
  T x y = (x < y) + (x ＝ y) + (y < x)

  Ξ³ : (a b : X) β†’ T a b
  Ξ³ = transfinite-induction w (Ξ» a β†’ (b : X) β†’ T a b) Ο•
   where
    Ο• : (a : X) β†’ ((x : X) β†’ x < a β†’ (b : X) β†’ T x b) β†’ (b : X) β†’ T a b
    Ο• a IH-a = transfinite-induction w (T a) ψ
     where
      ψ : (b : X) β†’ ((y : X) β†’ y < b β†’ T a y) β†’ T a b
      ψ b IH-b = III
       where
        I : Β¬ (a < b) β†’ b β‰Ό a
        I Ξ½ y l = f (IH-b y l)
         where
          f : (a < y) + (a ＝ y) + (y < a) β†’ y < a
          f (inl m)       = 𝟘-elim (ν (t a y b m l))
          f (inr (inl p)) = 𝟘-elim (ν (transport (_< b) (p ⁻¹) l))
          f (inr (inr m)) = m

        II : Β¬ (b < a) β†’ a β‰Ό b
        II Ξ½ x l = g (IH-a x l b)
         where
          g : (x < b) + (x ＝ b) + (b < x) β†’ x < b
          g (inl m)       = m
          g (inr (inl p)) = 𝟘-elim (ν (transport (_< a) p l))
          g (inr (inr m)) = 𝟘-elim (ν (t b x a m l))

        III : T a b
        III = h (d a b) (d b a)
         where
          h : (a < b) + Β¬ (a < b)
            β†’ (b < a) + Β¬ (b < a)
            β†’ (a < b) + (a ＝ b) + (b < a)
          h (inl l) _       = inl l
          h (inr Ξ±) (inl l) = inr (inr l)
          h (inr Ξ±) (inr Ξ²) = inr (inl (e a b (II Ξ²) (I Ξ±)))

trichotomy₃ : excluded-middle π“₯
            β†’ is-well-order
            β†’ is-trichotomous-order
trichotomy₃ em (p , w , e , t) = trichotomy-from-decidable-order
                                  t e w (Ξ» x y β†’ em (x < y) (p x y))

decidable-order-from-trichotomy : is-transitive
                                β†’ is-well-founded
                                β†’ is-trichotomous-order
                                β†’ is-decidable-order
decidable-order-from-trichotomy t w Ο„ = Ξ³
 where
  Ξ³ : (x y : X) β†’ decidable (x < y)
  Ξ³ x y = f (Ο„ x y)
   where
    f : (x < y) + (x ＝ y) + (y < x) β†’ (x < y) + Β¬ (x < y)
    f (inl l)       = inl l
    f (inr (inl p)) = inr (Ξ» (m : x < y) β†’ irreflexive x (w x) (transport (x <_) (p ⁻¹) m))
    f (inr (inr l)) = inr (Ξ» (m : x < y) β†’ irreflexive x (w x) (t x y x m l))

decidable-order-iff-trichotomy : is-well-order
                               β†’ is-trichotomous-order ⇔ is-decidable-order
decidable-order-iff-trichotomy (_ , w , e , t) =
 decidable-order-from-trichotomy t w ,
 trichotomy-from-decidable-order t e w

\end{code}

Paul also remarks that the result can be strengthened as follows: A
transitive well-founded relation is trichotomous iff it is both
extensional and decidable. TODO. Write this down in Agda.

End of 16th November 2022 addition.

\begin{code}
not-<-gives-β‰Ό : funext (𝓀 βŠ” π“₯) 𝓀₀
              β†’ excluded-middle (𝓀 βŠ” π“₯)
              β†’ is-well-order
              β†’ (x y : X) β†’ Β¬ (x < y) β†’ y β‰Ό x
not-<-gives-β‰Ό fe em wo@(p , w , e , t) x y = Ξ³ (trichotomy fe em wo x y)
 where
  Ξ³ : (x < y) + (x ＝ y) + (y < x) β†’ Β¬ (x < y) β†’ y β‰Ό x
  γ (inl l)       ν = 𝟘-elim (ν l)
  Ξ³ (inr (inl e)) Ξ½ = transport (_β‰Ό x) e β‰Ό-refl
  Ξ³ (inr (inr m)) Ξ½ = <-gives-β‰Ό t m

β‰Ό-or-> : funext (𝓀 βŠ” π“₯) 𝓀₀
       β†’ excluded-middle (𝓀 βŠ” π“₯)
       β†’ is-well-order
       β†’ (x y : X) β†’ (x β‰Ό y) + y < x
β‰Ό-or-> fe em wo@(p , w , e , t) x y = Ξ³ (trichotomy fe em wo x y)
 where
  Ξ³ : (x < y) + (x ＝ y) + (y < x) β†’ (x β‰Ό y) + (y < x)
  Ξ³ (inl l)       = inl (<-gives-β‰Ό t l)
  Ξ³ (inr (inl e)) = inl (transport (x β‰Ό_) e β‰Ό-refl)
  Ξ³ (inr (inr m)) = inr m

\end{code}

Because we assume function extensionality and excluded middle in this
annonymous submodule, propositional truncations are available, and it
amounts to double negation.

\begin{code}

β‰Ύ-gives-β‰Ό-under-trichotomy : is-transitive
                           β†’ {a b : X}
                           β†’ ((x : X) β†’ in-trichotomy x b)
                           β†’ a β‰Ύ b
                           β†’ a β‰Ό b
β‰Ύ-gives-β‰Ό-under-trichotomy t {a} {b} Ο„ Ξ½ x = Ξ³ (Ο„ x)
 where
  γ : (x < b) + (x ＝ b) + (b < x)
    β†’ x < a
    β†’ x < b
  Ξ³ (inl m)       l = m
  γ (inr (inl p)) l = 𝟘-elim (ν (transport (_< a) p l))
  γ (inr (inr m)) l = 𝟘-elim (ν (t b x a m l))

β‰Ύ-gives-β‰Ό-under-trichotomy' : is-transitive
                            β†’ is-trichotomous-order
                            β†’ {a b : X} β†’ a β‰Ύ b β†’ a β‰Ό b
β‰Ύ-gives-β‰Ό-under-trichotomy' t Ο„ {a} {b} = β‰Ύ-gives-β‰Ό-under-trichotomy t (Ξ» x β†’ Ο„ x b)


module _ (fe : Fun-Ext)
         (em : Excluded-Middle)
       where

 nonempty-has-minimal' : is-well-order
                       β†’ (A : X β†’ 𝓦 Μ‡ )
                       β†’ ((x : X) β†’ is-prop (A x))
                       β†’ ¬¬ (Ξ£ x κž‰ X , A x)
                       β†’ Ξ£ x κž‰ X , A x Γ— ((y : X) β†’ A y β†’ x β‰Ό y)
 nonempty-has-minimal' {𝓦} W@(p , w , e , t) A A-is-prop-valued f = Ξ³ Ξ΄
  where
   Ξ” : 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
   Ξ” = Ξ£ x κž‰ X , A x Γ— ((y : X) β†’ A y β†’ x β‰Ύ y)

   g : Β¬ ((x : X) β†’ A x β†’ ¬¬ (Ξ£ y κž‰ X , (y < x) Γ— A y))
   g = contrapositive (no-minimal-is-empty w A) f

   h : ¬¬ (Ξ£ x κž‰ X , Β¬ (A x β†’ ¬¬ (Ξ£ y κž‰ X , (y < x) Γ— A y)))
   h = not-Ξ -implies-not-not-Ξ£
        (Ξ» x β†’ EM-gives-DNE em
                (A x β†’ ¬¬ (Ξ£ y κž‰ X , (y < x) Γ— A y))
                (Ξ β‚‚-is-prop fe (Ξ» _ _ β†’ 𝟘-is-prop)))
        g

   Ο• : (x : X)
     β†’ Β¬ (A x β†’ ¬¬ (Ξ£ y κž‰ X , (y < x) Γ— A y))
     β†’ A x Γ— ((y : X) β†’ A y β†’ x β‰Ύ y)
   Ο• x ψ = EM-gives-DNE em (A x)
             (A-is-prop-valued x)
             ((Ξ» Ξ½ β†’ ψ (Ξ» a _ β†’ Ξ½ a))) ,
           Ξ» y a l β†’ ψ (Ξ» _ Ξ½ β†’ Ξ½ (y , l , a))

   Ξ½ : ¬¬ Ξ”
   Ξ½ = ¬¬-functor (Ξ» (x , f) β†’ x , Ο• x f) h

   j : (x : X) β†’ is-prop ((y : X) β†’ A y β†’ x β‰Ύ y)
   j x = Π₃-is-prop fe (Ξ» y a l β†’ 𝟘-is-prop)

   i : (x : X) β†’ is-prop (A x Γ— ((y : X) β†’ A y β†’ x β‰Ύ y))
   i x = Γ—-is-prop (A-is-prop-valued x) (j x)

   Ο„ : is-trichotomous-order
   Ο„ = trichotomy₃ em W

   Ξ”-is-prop : is-prop Ξ”
   Ξ”-is-prop (x , a , f) (x' , a' , f') = to-subtype-＝ i q
    where
     q : x ＝ x'
     q = k (Ο„ x x')
      where
       k : (x < x') + (x ＝ x') + (x' < x) β†’ x ＝ x'
       k (inl l)       = 𝟘-elim (f' x a l)
       k (inr (inl p)) = p
       k (inr (inr l)) = 𝟘-elim (f x' a' l)

   Ξ΄ : Ξ”
   Ξ΄ = EM-gives-DNE em Ξ” Ξ”-is-prop Ξ½

   Ξ³ : Ξ” β†’ Ξ£ x κž‰ X , A x Γ— ((y : X) β†’ A y β†’ x β‰Ό y)
   Ξ³ (x , a , h) = x , a , (Ξ» y a β†’ β‰Ύ-gives-β‰Ό-under-trichotomy' t Ο„ {x} {y} (h y a))

 module _ (pt : propositional-truncations-exist) where

  open import UF.PropTrunc
  open PropositionalTruncation pt

  nonempty-has-minimal : is-well-order
                       β†’ (A : X β†’ 𝓦 Μ‡ )
                       β†’ ((x : X) β†’ is-prop (A x))
                       β†’ βˆƒ x κž‰ X , A x
                       β†’ Ξ£ x κž‰ X , A x Γ— ((y : X) β†’ A y β†’ x β‰Ό y)
  nonempty-has-minimal w A i e = nonempty-has-minimal' w A i (inhabited-is-nonempty e)

\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-β‰Ύ-gives-β‰Ό : cotransitive β†’ (x y : X) β†’ x β‰Ύ y β†’ x β‰Ό y
cotransitive-β‰Ύ-gives-β‰Ό 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)

tricho-gives-cotrans : is-transitive β†’ is-trichotomous-order β†’ cotransitive
tricho-gives-cotrans tra tri x y z l = Ξ³ (tri z y)
 where
  Ξ³ : (z < y) + (z ＝ y) + (y < z) β†’ (x < z) + (z < y)
  Ξ³ (inl m)          = inr m
  Ξ³ (inr (inl refl)) = inl l
  Ξ³ (inr (inr m))    = inl (tra x y z l m)

em-gives-cotrans : FunExt β†’ EM (𝓀 βŠ” π“₯) β†’ is-well-order β†’ cotransitive
em-gives-cotrans fe em wo@(p , w , e , t) = tricho-gives-cotrans t
                                              (trichotomy (fe (𝓀 βŠ” π“₯) 𝓀₀) em wo)
\end{code}

This is the end of the submodule with the assumption of excluded
middle.

Originally, in 2011 (see my JSL publication), we needed to work with
the following weakening of well-foundedness (transfinite induction for
detachable subsets), but as of Summer 2018, it is not needed any
longer as we are able to show that our compact ordinals are
well-founded in the standard, stronger, sense.

\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-prop : FunExt β†’ is-prop is-well-foundedβ‚‚
being-well-foundedβ‚‚-is-prop fe = Π₃-is-prop (Ξ» {𝓀} {π“₯} β†’ fe 𝓀 π“₯)
                                   (Ξ» p s 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-prop : FunExt β†’ is-prop-valued β†’ is-prop is-well-orderβ‚‚
being-well-orderβ‚‚-is-prop fe isp = Γ—β‚„-is-prop
                                     (Ξ β‚‚-is-prop (Ξ» {𝓀} {π“₯} β†’ fe 𝓀 π“₯)
                                        (Ξ» x y β†’ being-prop-is-prop (fe π“₯ π“₯)))
                                     (being-well-foundedβ‚‚-is-prop fe)
                                     (extensionality-is-prop fe isp)
                                     (transitivity-is-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 MLTT.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

𝟚-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 , m , Ο•) = Cases (𝟚-is-discrete (p z) β‚€)
                   (Ξ» (t : p z ＝ β‚€)
                            β†’  inr (prβ‚‚ (Ο• z y) (Lemma[a＝₀→b<cβ†’a<c] t m)))
                   (Ξ» (t : Β¬ (p z ＝ β‚€))
                            → inl (pr₂ (ϕ x z) (Lemma[a<b→c≠₀→a<c] m 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).