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 DiscreteAndSeparated

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

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 f = h
  where
   h : (x : X) (a : is-accessible x) β†’ P x a
   h x (next x Οƒ) = f 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

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

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) β†’ next x Οƒ ≑ b
  Ο† x Οƒ IH b = next x Οƒ β‰‘βŸ¨ i ⟩
               next x Ο„ β‰‘βŸ¨ prev-behaviour x b ⟩
               b        ∎
   where
    Ο„ : (y : X) β†’ 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)

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

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))

_β‰Ύ_ : 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

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 : X) β†’ 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

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)

<-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)

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 , p) = Ξ³
 where
  g : (x : X) β†’ is-accessible x β†’ Β¬ (A x)
  g x (next x Οƒ) Ξ½ = Ξ΄
   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 p = g x (w x) p

  γ : 𝟘
  Ξ³ = f s x p

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

\end{code}

The remainder of this file is not needed anywhere else (at least at
the time of writing, namely 11th January 2021).

\begin{code}

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

\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}

trichomous-gives-discrete : is-well-founded
                          β†’ is-trichotomous
                          β†’ is-discrete X
trichomous-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).

\begin{code}

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

 trichotomy : is-well-order
            β†’ is-trichotomous
 trichotomy (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 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 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}

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

\begin{code}

 open import UF-PropTrunc
 open PropositionalTruncation (fem-proptrunc (Ξ» 𝓀 π“₯ β†’ fe {𝓀} {π“₯}) em)

 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 A-is-prop-valued f = Ξ³
  where
   B : 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
   B = Ξ£ 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 (well-foundedness 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))

   δ : ¬¬ B
   Ξ΄ = ¬¬-functor (Ξ» (x , f) β†’ x , Ο• x f) h

   j : (x : X) β†’ is-prop ((y : X) β†’ A y β†’ x β‰Ύ y)
   j x = Π₃-is-prop fe (Ξ» x 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)

   B-is-prop : is-prop B
   B-is-prop (x , a , f) (x' , a' , f') = to-subtype-≑ i q
    where
     q : x ≑ x'
     q = k (trichotomy W 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)

   Ξ³ : B
   Ξ³ = EM-gives-DNE em B B-is-prop Ξ΄

\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)

\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 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 , (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).