Martin Escardo, 21 June 2018

Ordinals proper are defined in the module Ordinals, as types equipped
with well orders. This module forms the basis for that module. We
still use the terminology "ordinal" here.

\begin{code}

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

module Ordinals.WellOrderArithmetic where

open import MLTT.Spartan hiding (transitive)
open import Ordinals.Notions

open import UF.Base
open import UF.FunExt
open import UF.Subsingletons
open import UF.Subsingletons-Properties

\end{code}

Any proposition (i.e. subsingleton) is an ordinal under the empty
ordering.

\begin{code}

module prop
        {𝓀 π“₯}
        (P : 𝓀 Μ‡ )
        (isp : is-prop P)
       where

 private
  _<_ : P β†’ P β†’ π“₯ Μ‡
  x < y = 𝟘

 order = _<_

 prop-valued : is-prop-valued _<_
 prop-valued x y = 𝟘-is-prop

 extensional : is-extensional _<_
 extensional x y f g = isp x y

 transitive : is-transitive _<_
 transitive x y z a = 𝟘-elim a

 well-founded : is-well-founded _<_
 well-founded x = acc (Ξ» y a β†’ 𝟘-elim a)

 well-order : is-well-order _<_
 well-order = prop-valued , well-founded , extensional , transitive

 topped : P β†’ has-top _<_
 topped p = p , Ξ» q l β†’ 𝟘-elim l

 trichotomous : is-trichotomous-order _<_
 trichotomous x y = inr (inl (isp x y))

\end{code}

Two particular cases are 𝟘 and πŸ™, of course.

The sum of two ordinals.

\begin{code}

module plus
        {𝓀 π“₯ 𝓦}
        {X : 𝓀 Μ‡ }
        {Y : π“₯ Μ‡ }
        (_<_ : X β†’ X β†’ 𝓦 Μ‡ )
        (_β‰Ί_ : Y β†’ Y β†’ 𝓦 Μ‡ )
       where

 private
  _⊏_ : X + Y β†’ X + Y β†’ 𝓦 Μ‡
  (inl x) ⊏ (inl x') = x < x'
  (inl x) ⊏ (inr y') = πŸ™
  (inr y) ⊏ (inl x') = 𝟘
  (inr y) ⊏ (inr y') = y β‰Ί y'

\end{code}

TODO. We would like to generalize _β‰Ί_ : Y β†’ Y β†’ 𝓣 Μ‡ with an arbitrary
universe 𝓣, and then _⊏_ : X + Y β†’ X + Y β†’ 𝓦 βŠ” 𝓣 Μ‡. In this case, we
would need to lift x < x' amd y β‰Ί y', in the above definition of _⊏_
and then adapt the following definitions.

\begin{code}

 order = _⊏_

 prop-valued : is-prop-valued _<_
             β†’ is-prop-valued _β‰Ί_
             β†’ is-prop-valued _⊏_
 prop-valued p p' (inl x) (inl x') l m = p x x' l m
 prop-valued p p' (inl x) (inr y') * * = refl
 prop-valued p p' (inr y) (inl x') a m = 𝟘-elim a
 prop-valued p p' (inr y) (inr y') l m = p' y y' l m

 extensional : is-well-founded _<_
             β†’ is-extensional _<_
             β†’ is-extensional _β‰Ί_
             β†’ is-extensional _⊏_
 extensional w e e' (inl x) (inl x') f g = ap inl (e x x' (f ∘ inl) (g ∘ inl))
 extensional w e e' (inl x) (inr y') f g = 𝟘-elim (irreflexive _<_ x (w x) (g (inl x) ⋆))
 extensional w e e' (inr y) (inl x') f g = 𝟘-elim (irreflexive _<_ x' (w x') (f (inl x') ⋆))
 extensional w e e' (inr y) (inr y') f g = ap inr (e' y y' (f ∘ inr) (g ∘ inr))

 transitive : is-transitive _<_
            β†’ is-transitive _β‰Ί_
            β†’ is-transitive _⊏_
 transitive t t' (inl x) (inl x') (inl z)  l m = t x x' z l m
 transitive t t' (inl x) (inl x') (inr z') l m = ⋆
 transitive t t' (inl x) (inr y') (inl z)  l m = 𝟘-elim m
 transitive t t' (inl x) (inr y') (inr z') l m = ⋆
 transitive t t' (inr y) (inl x') _        l m = 𝟘-elim l
 transitive t t' (inr y) (inr y') (inl z') l m = 𝟘-elim m
 transitive t t' (inr y) (inr y') (inr z') l m = t' y y' z' l m

 well-founded : is-well-founded _<_
              β†’ is-well-founded _β‰Ί_
              β†’ is-well-founded _⊏_
 well-founded w w' = g
  where
   Ο† : (x : X) β†’ is-accessible _<_ x β†’ is-accessible _⊏_ (inl x)
   Ο† x (acc Οƒ) = acc Ο„
    where
     Ο„ : (s : X + Y) β†’ s ⊏ inl x β†’ is-accessible _⊏_ s
     Ο„ (inl x') l = Ο† x' (Οƒ x' l)
     Ο„ (inr y') l = 𝟘-elim l

   Ξ³ : (y : Y) β†’ is-accessible _β‰Ί_ y β†’ is-accessible _⊏_ (inr y)
   Ξ³ y (acc Οƒ) = acc Ο„
    where
     Ο„ : (s : X + Y) β†’ s ⊏ inr y β†’ is-accessible _⊏_ s
     Ο„ (inl x)  l = Ο† x (w x)
     Ο„ (inr y') l = Ξ³ y' (Οƒ y' l)

   g : is-well-founded _⊏_
   g (inl x) = Ο† x (w x)
   g (inr y) = Ξ³ y (w' y)

 well-order : is-well-order _<_
            β†’ is-well-order _β‰Ί_
            β†’ is-well-order _⊏_
 well-order (p , w , e , t) (p' , w' , e' , t') = prop-valued p p' ,
                                                  well-founded w w' ,
                                                  extensional w e e' ,
                                                  transitive t t'

 top-preservation : has-top _β‰Ί_ β†’ has-top _⊏_
 top-preservation (y , f) = inr y , g
  where
   g : (z : X + Y) β†’ Β¬ (inr y ⊏ z)
   g (inl x)  l = 𝟘-elim l
   g (inr y') l = f y' l

 tricho-left : (x : X)
             β†’ is-trichotomous-element _<_ x
             β†’ is-trichotomous-element _⊏_ (inl x)
 tricho-left x t (inl x') = lemma (t x')
  where
   lemma : (x < x') + (x = x') + (x' < x)
         β†’ inl x ⊏ inl x' + (inl x = inl x') + inl x' ⊏ inl x
   lemma (inl l)       = inl l
   lemma (inr (inl e)) = inr (inl (ap inl e))
   lemma (inr (inr k)) = inr (inr k)

 tricho-left x t (inr y)  = inl ⋆

 tricho-right : (y : Y)
              β†’ is-trichotomous-element _β‰Ί_ y
              β†’ is-trichotomous-element _⊏_ (inr y)
 tricho-right y u (inl x)  = inr (inr ⋆)
 tricho-right y u (inr y') = lemma (u y')
  where
   lemma : (y β‰Ί y') + (y = y') + (y' β‰Ί y)
         β†’ inr y ⊏ inr y' + (inr y = inr y') + inr y' ⊏ inr y
   lemma (inl l)       = inl l
   lemma (inr (inl e)) = inr (inl (ap inr e))
   lemma (inr (inr k)) = inr (inr k)

 trichotomy-preservation : is-trichotomous-order _<_
                         β†’ is-trichotomous-order _β‰Ί_
                         β†’ is-trichotomous-order _⊏_
 trichotomy-preservation t u (inl x) = tricho-left  x (t x)
 trichotomy-preservation t u (inr y) = tricho-right y (u y)

\end{code}

Successor (probably get rid of it as we can do _+β‚’ πŸ™β‚’):

\begin{code}

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

  private
   _β‰Ί_ : πŸ™ β†’ πŸ™ β†’ π“₯ Μ‡
   _β‰Ί_ = prop.order {𝓀} πŸ™ πŸ™-is-prop

   _<'_ : X + πŸ™ β†’ X + πŸ™ β†’ π“₯ Μ‡
   _<'_ = plus.order _<_ _β‰Ί_

  order = _<'_

  well-order : is-well-order _<_ β†’ is-well-order _<'_
  well-order o = plus.well-order _<_ _β‰Ί_ o (prop.well-order πŸ™ πŸ™-is-prop)

  top : has-top _<'_
  top = inr ⋆ , g
   where
    g : (y : X + πŸ™) β†’ Β¬ (inr ⋆ <' y)
    g (inl x) l = 𝟘-elim l
    g (inr ⋆) l = 𝟘-elim l

\end{code}

Multiplication. Cartesian product with the lexicographic order.

\begin{code}

module times
        {𝓀 π“₯ 𝓦 𝓣}
        {X : 𝓀 Μ‡ }
        {Y : π“₯ Μ‡ }
        (_<_ : X β†’ X β†’ 𝓦 Μ‡ )
        (_β‰Ί_ : Y β†’ Y β†’ 𝓣 Μ‡ )
       where

 private
  _⊏_ : X Γ— Y β†’ X Γ— Y β†’ 𝓀 βŠ” 𝓦 βŠ” 𝓣 Μ‡
  (a , b) ⊏ (x , y) = (a < x) + ((a = x) Γ— (b β‰Ί y))

 order = _⊏_

 well-founded : is-well-founded _<_
              β†’ is-well-founded _β‰Ί_
              β†’ is-well-founded _⊏_
 well-founded w w' (x , y) = Ο† x y
  where
   P : X Γ— Y β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 βŠ” 𝓣 Μ‡
   P = is-accessible _⊏_

   Ξ³ : (x : X) β†’ ((x' : X) β†’ x' < x β†’ (y' : Y) β†’ P (x' , y')) β†’ (y : Y) β†’ P (x , y)
   Ξ³ x s = transfinite-induction _β‰Ί_ w' (Ξ» y β†’ P (x , y)) (Ξ» y f β†’ acc (ψ y f))
    where
     ψ : (y : Y) β†’ ((y' : Y) β†’ y' β‰Ί y β†’ P (x , y')) β†’ (z' : X Γ— Y) β†’ z' ⊏ (x , y) β†’ P z'
     ψ y f (x' , y') (inl l) = s x' l y'
     ψ y f (x' , y') (inr (r , m)) = transport⁻¹ P p α
      where
       Ξ± : P (x , y')
       Ξ± = f y' m

       p : (x' , y') = (x , y')
       p = to-Γ—-= r refl

   Ο† : (x : X) (y : Y) β†’ P (x , y)
   Ο† = transfinite-induction _<_ w (Ξ» x β†’ (y : Y) β†’ P (x , y)) Ξ³

 transitive : is-transitive _<_
            β†’ is-transitive _β‰Ί_
            β†’ is-transitive _⊏_
 transitive t t' (a , b) (x , y) (u , v) = f
  where
   f : (a , b) ⊏ (x , y) β†’ (x , y) ⊏ (u , v) β†’ (a , b) ⊏ (u , v)
   f (inl l)       (inl m)          = inl (t _ _ _ l m)
   f (inl l)       (inr (q , m))    = inl (transport (Ξ» - β†’ a < -) q l)
   f (inr (r , l)) (inl m)          = inl (transport⁻¹ (Ξ» - β†’ - < u) r m)
   f (inr (r , l)) (inr (refl , m)) = inr (r , (t' _ _ _ l m))

 extensional : is-well-founded _<_
             β†’ is-well-founded _β‰Ί_
             β†’ is-extensional _<_
             β†’ is-extensional _β‰Ί_
             β†’ is-extensional _⊏_
 extensional w w' e e' (a , b) (x , y) f g = to-Γ—-= p q
  where
   f' : (u : X) β†’ u < a β†’ u < x
   f' u l = Cases (f (u , y) (inl l))
             (Ξ» (m : u < x) β†’ m)
             (Ξ» (Οƒ : (u = x) Γ— (y β‰Ί y)) β†’ 𝟘-elim (irreflexive _β‰Ί_ y (w' y) (prβ‚‚ Οƒ)))

   g' : (u : X) β†’ u < x β†’ u < a
   g' u l = Cases (g ((u , b)) (inl l))
             (Ξ» (m : u < a) β†’ m)
             (Ξ» (Οƒ : (u = a) Γ— (b β‰Ί b)) β†’ 𝟘-elim (irreflexive _β‰Ί_ b (w' b) (prβ‚‚ Οƒ)))

   p : a = x
   p = e a x f' g'

   f'' : (v : Y) β†’ v β‰Ί b β†’ v β‰Ί y
   f'' v l = Cases (f (a , v) (inr (refl , l)))
              (Ξ» (m : a < x)
                 β†’ 𝟘-elim (irreflexive _β‰Ί_ b (w' b)
                             (Cases (g (a , b) (inl m))
                              (Ξ» (n : a < a) β†’ 𝟘-elim (irreflexive _<_ a (w a) n))
                              (Ξ» (Οƒ : (a = a) Γ— (b β‰Ί b)) β†’ 𝟘-elim (irreflexive _β‰Ί_ b (w' b) (prβ‚‚ Οƒ))))))
              (Ξ» (Οƒ : (a = x) Γ— (v β‰Ί y))
                 β†’ prβ‚‚ Οƒ)

   g'' : (v : Y) β†’ v β‰Ί y β†’ v β‰Ί b
   g'' v l = Cases (g (x , v) (inr (refl , l)))
              (Ξ» (m : x < a)
                 β†’ Cases (f (x , y) (inl m))
                     (Ξ» (m : x < x)
                        β†’ 𝟘-elim (irreflexive _<_ x (w x) m))
                     (Ξ» (Οƒ : (x = x) Γ— (y β‰Ί y))
                        β†’ 𝟘-elim (irreflexive _β‰Ί_ y (w' y) (prβ‚‚ Οƒ))))
              (Ξ» (Οƒ : (x = a) Γ— (v β‰Ί b))
                 β†’ prβ‚‚ Οƒ)

   q : b = y
   q = e' b y f'' g''

 well-order : FunExt
            β†’ is-well-order _<_
            β†’ is-well-order _β‰Ί_
            β†’ is-well-order _⊏_
 well-order fe (p , w , e , t) (p' , w' , e' , t') = prop-valued ,
                                                     well-founded w w' ,
                                                     extensional w w' e e' ,
                                                     transitive t t'
  where
   prop-valued : is-prop-valued _⊏_
   prop-valued (a , b) (x , y) (inl l) (inl m) =
     ap inl (p a x l m)
   prop-valued (a , b) (x , y) (inl l) (inr (s , m)) =
     𝟘-elim (irreflexive _<_ x (w x) (transport (Ξ» - β†’ - < x) s l))
   prop-valued (a , b) (x , y) (inr (r , l)) (inl m) =
     𝟘-elim (irreflexive _<_ x (w x) (transport (Ξ» - β†’ - < x) r m))
   prop-valued (a , b) (x , y) (inr (r , l)) (inr (s , m)) =
     ap inr (to-Γ—-= (well-ordered-types-are-sets _<_ fe (p , w , e , t) r s) (p' b y l m))

 top-preservation : has-top _<_ β†’ has-top _β‰Ί_ β†’ has-top _⊏_
 top-preservation (x , f) (y , g) = (x , y) , h
  where
   h : (z : X Γ— Y) β†’ Β¬ ((x , y) ⊏ z)
   h (x' , y') (inl l) = f x' l
   h (x' , y') (inr (r , l)) = g y' l

 tricho : {x : X} {y : Y}
        β†’ is-trichotomous-element _<_ x
        β†’ is-trichotomous-element _β‰Ί_ y
        β†’ is-trichotomous-element _⊏_ (x , y)
 tricho {x} {y} t u (x' , y') =
  Cases (t x')
   (Ξ» (l : x < x') β†’ inl (inl l))
   (cases
     (λ (p : x = x')
        β†’ Cases (u y')
           (Ξ» (l : y β‰Ί y')
              β†’ inl (inr (p , l)))
           (cases
             (λ (q : y = y')
                β†’ inr (inl (to-Γ—-= p q)))
             (Ξ» (l : y' β‰Ί y) β†’ inr (inr (inr ((p ⁻¹) , l))))))
     (Ξ» (l : x' < x) β†’ inr (inr (inl l))))

 trichotomy-preservation : is-trichotomous-order _<_
                         β†’ is-trichotomous-order _β‰Ί_
                         β†’ is-trichotomous-order _⊏_
 trichotomy-preservation t u (x , y) = tricho (t x) (u y)

\end{code}

Above trichotomy preservation added 20th April 2022.

Added 27 June 2018. A product of ordinals indexed by a prop is
an ordinal. Here "is" is used to indicate a construction, not a
proposition. We begin with a general lemma (and a corollary, which is
not used for our purposes).

\begin{code}

retract-accessible : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                     (_<_ : X β†’ X β†’ 𝓦 Μ‡ ) (_β‰Ί_ : Y β†’ Y β†’ 𝓣 Μ‡ )
                     (r : X β†’ Y) (s : Y β†’ X)
                   β†’ ((y : Y) β†’ r (s y) = y)
                   β†’ ((x : X) (y : Y) β†’ y β‰Ί r x β†’ s y < x)
                   β†’ (x : X) β†’ is-accessible _<_ x β†’ is-accessible _β‰Ί_ (r x)
retract-accessible _<_ _β‰Ί_ r s Ξ· Ο† = transfinite-induction' _<_ P Ξ³
 where
  P = Ξ» x β†’ is-accessible _β‰Ί_ (r x)

  Ξ³ : βˆ€ x β†’ (βˆ€ x' β†’ x' < x β†’ is-accessible _β‰Ί_ (r x')) β†’ is-accessible _β‰Ί_ (r x)
  Ξ³ x Ο„ = acc Οƒ
   where
    Οƒ : βˆ€ y β†’ y β‰Ί r x β†’ is-accessible _β‰Ί_ y
    Οƒ y l = transport (is-accessible _β‰Ί_) (Ξ· y) m
     where
      m : is-accessible _β‰Ί_ (r (s y))
      m = Ο„ (s y) (Ο† x y l)

retract-well-founded : {X : 𝓀 Μ‡ } {Y : π“₯ Μ‡ }
                       (_<_ : X β†’ X β†’ 𝓦 Μ‡ ) (_β‰Ί_ : Y β†’ Y β†’ 𝓣 Μ‡ )
                       (r : X β†’ Y) (s : Y β†’ X)
                     β†’ ((y : Y) β†’ r (s y) = y)
                     β†’ ((x : X) (y : Y) β†’ y β‰Ί r x β†’ s y < x)
                     β†’ is-well-founded _<_ β†’ is-well-founded _β‰Ί_
retract-well-founded {𝓀} {π“₯} {𝓦} {𝓣} {X} {Y} _<_ _β‰Ί_ r s Ξ· Ο† w = w'
 where
  wr : (x : X) β†’ is-accessible _β‰Ί_ (r x)
  wr x = retract-accessible _<_ _β‰Ί_ r s Ξ· Ο† x (w x)

  w' : (y : Y) β†’ is-accessible _β‰Ί_ y
  w' y = transport (is-accessible _β‰Ί_) (Ξ· y) (wr (s y))

\end{code}

The product of a proposition-indexed family of ordinals (pip):

\begin{code}

module pip
        {𝓀 π“₯ 𝓦}
        (fe : funext 𝓀 π“₯)
        (P : 𝓀 Μ‡ )
        (P-is-prop : is-prop P)
        (X : P β†’ π“₯ Μ‡ )
        (_<_ : {p : P} β†’ X p β†’ X p β†’ 𝓦 Μ‡ )
       where

\end{code}

We have the following families of equivalences indexed by P,
constructed in the module UF.PropIndexedPiSigma:

\begin{code}

 open import UF.Equiv
 open import UF.PropIndexedPiSigma

 private
  Ο† : (p : P) β†’ Ξ  X β†’ X p
  Ο† p u = u p

  ψ : (p : P) β†’ X p β†’ Ξ  X
  ψ p x q = transport X (P-is-prop p q) x

  Ξ· : (p : P) (u : Ξ  X) β†’ ψ p (Ο† p u) = u
  Ξ· p = prβ‚‚ (prβ‚‚ (prβ‚‚ (prop-indexed-product fe P-is-prop p)))

  Ξ΅ : (p : P) (x : X p) β†’ Ο† p (ψ p x) = x
  Ξ΅ p = prβ‚‚ (pr₁ (prβ‚‚ (prop-indexed-product fe P-is-prop p)))

\end{code}

The order on the product is constructed as follows from the order in
the components:

\begin{code}

 private
   _β‰Ί_ : Ξ  X β†’ Ξ  X β†’ 𝓀 βŠ” 𝓦 Μ‡
   u β‰Ί v = Ξ£ p κž‰ P , Ο† p u < Ο† p v

 order = _β‰Ί_

\end{code}

That it is prop-valued depends only on the fact that the given order
_<_ {p} on the components of the product are prop-valued.

\begin{code}

 prop-valued : ((p : P) β†’ is-prop-valued (_<_ {p}))
             β†’ is-prop-valued _β‰Ί_
 prop-valued f u v = Ξ£-is-prop P-is-prop (Ξ» p β†’ f p (Ο† p u) (Ο† p v))

\end{code}

The extensionality of the constructed order depends only on the fact
that Ο† is a retraction.

\begin{code}

 extensional : ((p : P) β†’ is-extensional (_<_ {p}))
             β†’ is-extensional _β‰Ί_
 extensional e u v f g = dfunext fe Ξ³
  where
   f' : (p : P) (x : X p) β†’ x < Ο† p u β†’ x < Ο† p v
   f' p x l = transport (Ξ» - β†’ - < Ο† p v) (Ξ΅ p x) n'
    where
     l' : Ο† p (ψ p x) < Ο† p u
     l' = transport⁻¹ (Ξ» - β†’ - < Ο† p u) (Ξ΅ p x) l

     a : ψ p x β‰Ί u
     a = p , l'

     m : ψ p x β‰Ί v
     m = f (ψ p x) a

     q : P
     q = pr₁ m

     n : Ο† q (ψ p x) < Ο† q v
     n = prβ‚‚ m

     n' : Ο† p (ψ p x) < Ο† p v
     n' = transport (Ξ» - β†’ ψ p x - < Ο† - v) (P-is-prop q p) n

   g' : (p : P) (x : X p) β†’ x < Ο† p v β†’ x < Ο† p u
   g' p x l = transport (Ξ» - β†’ - < Ο† p u) (Ξ΅ p x) n'
    where
     l' : Ο† p (ψ p x) < Ο† p v
     l' = transport⁻¹ (Ξ» - β†’ - < Ο† p v) (Ξ΅ p x) l

     a : ψ p x β‰Ί v
     a = p , l'

     m : ψ p x β‰Ί u
     m = g (ψ p x) a

     q : P
     q = pr₁ m

     n : Ο† q (ψ p x) < Ο† q u
     n = prβ‚‚ m

     n' : Ο† p (ψ p x) < Ο† p u
     n' = transport (Ξ» - β†’ ψ p x - < Ο† - u) (P-is-prop q p) n

   Ξ΄ : (p : P) β†’ Ο† p u = Ο† p v
   Ξ΄ p = e p (Ο† p u) (Ο† p v) (f' p) (g' p)

   γ : u ∼ v
   Ξ³ = Ξ΄

\end{code}

The transitivity of the constructed order depends only on the
transitivity of given order, using Ο† to transfer it, but not the fact
that it is an equivalence (or a retraction or a section).

\begin{code}

 transitive : ((p : P) β†’ is-transitive (_<_ {p}))
            β†’ is-transitive _β‰Ί_
 transitive t u v w (p , l) (q , m) = p , f l m'
  where
   f : Ο† p u < Ο† p v β†’ Ο† p v < Ο† p w β†’ Ο† p u < Ο† p w
   f = t p (Ο† p u) (Ο† p v) (Ο† p w)

   m' : Ο† p v < Ο† p w
   m' = transport (Ξ» - β†’ Ο† - v < Ο† - w) (P-is-prop q p) m

\end{code}

The well-foundedness of the constructed order uses the above
accessibility lemma for retracts. However, not only the fact that ψ is
a retraction is needed to apply the lemma, but also that it is a
section, to derive the order condition (given by f below) for the
lemma.

\begin{code}

 well-founded : ((p : P) β†’ is-well-founded (_<_ {p}))
              β†’ is-well-founded _β‰Ί_
 well-founded w u = acc Οƒ
  where
   Οƒ : (v : Ξ  X) β†’ v β‰Ί u β†’ is-accessible _β‰Ί_ v
   Οƒ v (p , l) = d
    where
     b : is-accessible _<_ (Ο† p v)
     b = prev _<_ (w p (Ο† p u)) (Ο† p v) l

     c : is-accessible _β‰Ί_ (ψ p (Ο† p v))
     c = retract-accessible _<_ _β‰Ί_ (ψ p) (Ο† p) (Ξ· p) f (Ο† p v) b
      where
       f : (x : X p) (u : Ξ  X) β†’ u β‰Ί ψ p x β†’ Ο† p u < x
       f x u (q , l) = transport (Ξ» - β†’ Ο† p u < -) (Ξ΅ p x) l'
        where
         l' : u p < ψ p x p
         l' = transport (Ξ» - β†’ u - < ψ p x -) (P-is-prop q p) l

     d : is-accessible _β‰Ί_ v
     d = transport (is-accessible _β‰Ί_) (Ξ· p v) c

 well-order : ((p : P) β†’ is-well-order (_<_ {p}))
            β†’ is-well-order _β‰Ί_
 well-order o = prop-valued  (Ξ» p β†’ prop-valuedness _<_ (o p)) ,
                well-founded (Ξ» p β†’ well-foundedness _<_ (o p)) ,
                extensional  (Ξ» p β†’ extensionality _<_ (o p)) ,
                transitive   (Ξ» p β†’ transitivity _<_ (o p))

\end{code}

I am not sure this is going to be useful:

\begin{code}

 top-preservation : P β†’ ((p : P) β†’ has-top (_<_ {p})) β†’ has-top _β‰Ί_
 top-preservation p f = (Ξ» q β†’ transport X (P-is-prop p q) (pr₁ (f p))) , g
  where
   g : (u : Ξ  X) β†’ Β¬ ((Ξ» q β†’ transport X (P-is-prop p q) (pr₁ (f p))) β‰Ί u)
   g u (q , l) = h n
    where
     h : Β¬ (pr₁ (f q) < u q)
     h = prβ‚‚ (f q) (u q)

     m : transport X (P-is-prop q q) (pr₁ (f q)) < u q
     m = transport (Ξ» p β†’ transport X (P-is-prop p q) (pr₁ (f p)) < u q) (P-is-prop p q) l

     n : pr₁ (f q) < u q
     n = transport (Ξ» - β†’ transport X - (pr₁ (f q)) < u q) (props-are-sets P-is-prop (P-is-prop q q) refl) m

\end{code}

Sum of an ordinal-indexed family of ordinals. To show that
extensionality is preserved, our argument uses the assumption that
each ordinal in the family has a top element or that the index type is
discrete.  (Perhaps better assumptions are possible. TODO: think about
this.) These assumptions are valid in our applications. We have three
sum submodules, the first one without assumptions.

\begin{code}

module sum
        {𝓀 π“₯ 𝓦 𝓣}
        {X : 𝓀 Μ‡ }
        {Y : X β†’ π“₯ Μ‡ }
        (_<_ : X β†’ X β†’ 𝓦 Μ‡ )
        (_β‰Ί_ : {x : X} β†’ Y x β†’ Y x β†’ 𝓣 Μ‡ )
      where

 open import Ordinals.LexicographicOrder

 private
  _⊏_ : Ξ£ Y β†’ Ξ£ Y β†’ 𝓀 βŠ” 𝓦 βŠ” 𝓣 Μ‡
  _⊏_ = slex-order _<_ _β‰Ί_

 order = _⊏_

 well-founded : is-well-founded _<_
              β†’ ((x : X) β†’ is-well-founded (_β‰Ί_ {x}))
              β†’ is-well-founded _⊏_
 well-founded w w' (x , y) = Ο† x y
  where
   P : Ξ£ Y β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 βŠ” 𝓣 Μ‡
   P = is-accessible _⊏_

   Ξ³ : (x : X)
     β†’ ((x' : X) β†’ x' < x β†’ (y' : Y x') β†’ P (x' , y'))
     β†’ (y : Y x) β†’ P (x , y)
   Ξ³ x s = transfinite-induction _β‰Ί_ (w' x)
            (Ξ» y β†’ P (x , y))
            (Ξ» y f β†’ acc (ψ y f))
    where
     ψ : (y : Y x)
       β†’ ((y' : Y x) β†’ y' β‰Ί y β†’ P (x , y'))
       β†’ (z' : Ξ£ Y) β†’ z' ⊏ (x , y) β†’ P z'
     ψ y f (x' , y') (inl l) = s x' l y'
     ψ y f (x' , y') (inr (r , m)) = transport⁻¹ P p α
      where
       Ξ± : P (x , transport Y r y')
       Ξ± = f (transport Y r y') m

       p : (x' , y') = (x , transport Y r y')
       p = to-Σ-= (r , refl)

   Ο† : (x : X) (y : Y x) β†’ P (x , y)
   Ο† = transfinite-induction _<_ w (Ξ» x β†’ (y : Y x) β†’ P (x , y)) Ξ³

 transitive : is-transitive _<_
            β†’ ((x : X) β†’ is-transitive (_β‰Ί_ {x}))
            β†’ is-transitive _⊏_
 transitive t t' (a , b) (x , y) (u , v) = f
  where
   f : (a , b) ⊏ (x , y) β†’ (x , y) ⊏ (u , v) β†’ (a , b) ⊏ (u , v)
   f (inl l)       (inl m)          = inl (t _ _ _ l m)
   f (inl l)       (inr (q , m))    = inl (transport (Ξ» - β†’ a < -) q l)
   f (inr (r , l)) (inl m)          = inl (transport⁻¹ (Ξ» - β†’ - < u) r m)
   f (inr (r , l)) (inr (refl , m)) = inr (r , (t' x _ _ _ l m))

 prop-valued : FunExt
             β†’ is-prop-valued _<_
             β†’ is-well-founded _<_
             β†’ is-extensional _<_
             β†’ ((x : X) β†’ is-prop-valued (_β‰Ί_ {x}))
             β†’ is-prop-valued _⊏_
 prop-valued fe p w e f (a , b) (x , y) (inl l) (inl m) =
   ap inl (p a x l m)
 prop-valued fe p w e f (a , b) (x , y) (inl l) (inr (s , m)) =
   𝟘-elim (irreflexive _<_ x (w x) (transport (Ξ» - β†’ - < x) s l))
 prop-valued fe p w e f (a , b) (x , y) (inr (r , l)) (inl m) =
   𝟘-elim (irreflexive _<_ x (w x) (transport (Ξ» - β†’ - < x) r m))
 prop-valued fe p _ e f (a , b) (x , y) (inr (r , l)) (inr (s , m)) =
   ap inr (to-Σ-= (extensionally-ordered-types-are-sets _<_ fe p e r s ,
                     (f x (transport Y s b) y _ m)))

 tricho : {x : X} {y : Y x}
        β†’ is-trichotomous-element _<_ x
        β†’ is-trichotomous-element _β‰Ί_ y
        β†’ is-trichotomous-element _⊏_ (x , y)
 tricho {x} {y} t u (x' , y') =
  Cases (t x')
   (Ξ» (l : x < x') β†’ inl (inl l))
   (cases
     (λ (p : x = x')
        β†’ Cases (u (transport⁻¹ Y p y'))
           (Ξ» (l : y β‰Ί transport⁻¹ Y p y')
              β†’ inl (inr (p , transport⁻¹-right-rel _β‰Ί_ x' x y' y p l)))
           (cases
             (λ (q : y = transport⁻¹ Y p y')
                β†’ inr (inl (to-Ξ£-=
                             (p , (transport Y p y                    =⟨ ap (transport Y p) q ⟩
                                   transport Y p (transport⁻¹ Y p y') =⟨ back-and-forth-transport p ⟩
                                   y'                                 ∎
                                      )))))
             (Ξ» (l : transport⁻¹ Y p y' β‰Ί y) β†’ inr (inr (inr ((p ⁻¹) , l))))))
     (Ξ» (l : x' < x) β†’ inr (inr (inl l))))

 trichotomy-preservation : is-trichotomous-order _<_
                         β†’ ((x : X) β†’ is-trichotomous-order (_β‰Ί_ {x}))
                         β†’ is-trichotomous-order _⊏_
 trichotomy-preservation t u (x , y) = tricho (t x) (u x y)

\end{code}

The above trichotomy preservation added 19th April 2022.

We know how to prove extensionality either assuming top elements or
assuming cotransitivity. We do this in the following two modules.

\begin{code}

module sum-top
        (fe : FunExt)
        {𝓀 π“₯ 𝓦 𝓣}
        {X : 𝓀 Μ‡ }
        {Y : X β†’ π“₯ Μ‡ }
        (_<_ : X β†’ X β†’ 𝓦 Μ‡ )
        (_β‰Ί_ : {x : X} β†’ Y x β†’ Y x β†’ 𝓣 Μ‡ )
        (top : Ξ  Y)
        (ist : (x : X) β†’ is-top _β‰Ί_ (top x))
      where

 open sum {𝓀} {π“₯} {𝓦} {𝓣} {X} {Y} _<_  _β‰Ί_ public

 private _⊏_ = order

 extensional : is-prop-valued _<_
             β†’ is-well-founded _<_
             β†’ ((x : X) β†’ is-well-founded (_β‰Ί_ {x}))
             β†’ is-extensional _<_
             β†’ ((x : X) β†’ is-extensional (_β‰Ί_ {x}))
             β†’ is-extensional _⊏_
 extensional ispv w w' e e' (a , b) (x , y) f g = to-Σ-= (p , q)
  where
   f' : (u : X) β†’ u < a β†’ u < x
   f' u l = Cases (f (u , top u) (inl l))
             (Ξ» (m : u < x)
                β†’ m)
             (Ξ» (Οƒ : Ξ£ r κž‰ u = x , transport Y r (top u) β‰Ί y)
                β†’ 𝟘-elim (transport-fam (is-top _β‰Ί_) u (top u)
                           (ist u) x (pr₁ Οƒ) y (prβ‚‚ Οƒ)))

   g' : (u : X) β†’ u < x β†’ u < a
   g' u l = Cases (g (u , top u) (inl l))
             (Ξ» (m : u < a)
                β†’ m)
             (Ξ» (Οƒ : Ξ£ r κž‰ u = a , transport Y r (top u) β‰Ί b)
                β†’ 𝟘-elim (transport-fam (is-top _β‰Ί_) u (top u)
                           (ist u) a (pr₁ Οƒ) b (prβ‚‚ Οƒ)))

   p : a = x
   p =  e a x f' g'

   f'' : (v : Y x) β†’ v β‰Ί transport Y p b β†’ v β‰Ί y
   f'' v l = Cases (f (x , v) (inr ((p ⁻¹) , transport-right-rel _β‰Ί_ a x b v p l)))
              (Ξ» (l : x < x)
                 β†’ 𝟘-elim (irreflexive _<_ x (w x) l))
              (Ξ» (Οƒ : Ξ£ r κž‰ x = x , transport Y r v β‰Ί y)
                 β†’ Ο† Οƒ)
              where
               Ο† : (Οƒ : Ξ£ r κž‰ x = x , transport Y r v β‰Ί y) β†’ v β‰Ί y
               Ο† (r , l) = transport
                            (Ξ» - β†’ transport Y - v β‰Ί y)
                            (extensionally-ordered-types-are-sets _<_ fe ispv e r refl)
                            l

   g'' : (u : Y x) β†’ u β‰Ί y β†’ u β‰Ί transport Y p b
   g'' u m = Cases (g (x , u) (inr (refl , m)))
              (Ξ» (l : x < a)
                 β†’ 𝟘-elim (irreflexive _<_ x (w x) (transport (Ξ» - β†’ x < -) p l)))
              (Ξ» (Οƒ : Ξ£ r κž‰ x = a , transport Y r u β‰Ί b)
                 β†’ transport
                     (Ξ» - β†’ u β‰Ί transport Y - b)
                     (extensionally-ordered-types-are-sets _<_ fe ispv e ((pr₁ Οƒ)⁻¹) p)
                     (transport-left-rel _β‰Ί_ a x b u (pr₁ Οƒ) (prβ‚‚ Οƒ)))

   q : transport Y p b = y
   q = e' x (transport Y p b) y f'' g''

 well-order : is-well-order _<_
            β†’ ((x : X) β†’ is-well-order (_β‰Ί_ {x}))
            β†’ is-well-order _⊏_
 well-order (p , w , e , t) f = prop-valued fe p w e (Ξ» x β†’ prop-valuedness _β‰Ί_ (f x)) ,
                                well-founded w (Ξ» x β†’ well-foundedness _β‰Ί_ (f x)) ,
                                extensional
                                  (prop-valuedness _<_ (p , w , e , t))
                                     w
                                     (Ξ» x β†’ well-foundedness _β‰Ί_ (f x))
                                     e
                                     (Ξ» x β†’ extensionality _β‰Ί_ (f x)) ,
                                transitive t (Ξ» x β†’ transitivity _β‰Ί_ (f x))

 top-preservation : has-top _<_ β†’ has-top _⊏_
 top-preservation (x , f) = (x , top x) , g
  where
   g : (Οƒ : Ξ£ Y) β†’ Β¬ ((x , top x) ⊏ Οƒ)
   g (x' , y) (inl l)          = f x' l
   g (x' , y) (inr (refl , l)) = ist x' y l

\end{code}

\begin{code}

open import UF.DiscreteAndSeparated

module sum-cotransitive
        (fe : FunExt)
        {𝓀 π“₯ 𝓦 𝓣}
        {X : 𝓀 Μ‡ }
        {Y : X β†’ π“₯ Μ‡ }
        (_<_ : X β†’ X β†’ 𝓦 Μ‡ )
        (_β‰Ί_ : {x : X} β†’ Y x β†’ Y x β†’ 𝓣 Μ‡ )
        (c : cotransitive _<_)
      where

 open sum {𝓀} {π“₯} {𝓦} {𝓣} {X} {Y} _<_  _β‰Ί_ public

 private _⊏_ = order

 extensional : is-prop-valued _<_
             β†’ is-well-founded _<_
             β†’ ((x : X) β†’ is-well-founded (_β‰Ί_ {x}))
             β†’ is-extensional _<_
             β†’ ((x : X) β†’ is-extensional (_β‰Ί_ {x}))
             β†’ is-extensional _⊏_
 extensional ispv w w' e e' (a , b) (x , y) f g = to-Σ-= (p , q)
  where
   f' : (u : X) β†’ u < a β†’ u < x
   f' u l = Cases (c u a x l)
             (Ξ» (m : u < x)
                β†’ m)
             (Ξ» (m : x < a)
                β†’ let n : (x , y) ⊏ (x , y)
                      n = f (x , y) (inl m)
                  in 𝟘-elim (irreflexive _⊏_ (x , y)
                      (sum.well-founded _<_ _β‰Ί_ w w' (x , y)) n))

   g' : (u : X) β†’ u < x β†’ u < a
   g' u l = Cases (c u x a l)
             (Ξ» (m : u < a)
                β†’ m)
             (Ξ» (m : a < x)
                β†’ let n : (a , b) ⊏ (a , b)
                      n = g (a , b) (inl m)
                  in 𝟘-elim (irreflexive _⊏_ (a , b)
                      (sum.well-founded _<_ _β‰Ί_ w w' (a , b)) n))
   p : a = x
   p =  e a x f' g'

   f'' : (v : Y x) β†’ v β‰Ί transport Y p b β†’ v β‰Ί y
   f'' v l = Cases (f (x , v) (inr ((p ⁻¹) , transport-right-rel _β‰Ί_ a x b v p l)))
              (Ξ» (l : x < x)
                 β†’ 𝟘-elim (irreflexive _<_ x (w x) l))
              (Ξ» (Οƒ : Ξ£ r κž‰ x = x , transport Y r v β‰Ί y)
                 β†’ Ο† Οƒ)
              where
               Ο† : (Οƒ : Ξ£ r κž‰ x = x , transport Y r v β‰Ί y) β†’ v β‰Ί y
               Ο† (r , l) = transport
                            (Ξ» r β†’ transport Y r v β‰Ί y)
                            (extensionally-ordered-types-are-sets _<_ fe
                              ispv e r refl)
                            l

   g'' : (u : Y x) β†’ u β‰Ί y β†’ u β‰Ί transport Y p b
   g'' u m = Cases (g (x , u) (inr (refl , m)))
              (Ξ» (l : x < a)
                 β†’ 𝟘-elim (irreflexive _<_ x (w x) (transport (Ξ» - β†’ x < -) p l)))
              (Ξ» (Οƒ : Ξ£ r κž‰ x = a , transport Y r u β‰Ί b)
                 β†’ transport
                     (Ξ» - β†’ u β‰Ί transport Y - b)
                     (extensionally-ordered-types-are-sets _<_ fe
                       ispv e ((pr₁ Οƒ)⁻¹) p)
                     (transport-left-rel _β‰Ί_ a x b u (pr₁ Οƒ) (prβ‚‚ Οƒ)))

   q : transport Y p b = y
   q = e' x (transport Y p b) y f'' g''

 well-order : is-well-order _<_
            β†’ ((x : X) β†’ is-well-order (_β‰Ί_ {x}))
            β†’ is-well-order _⊏_
 well-order (p , w , e , t) f =
   prop-valued fe p w e (Ξ» x β†’ prop-valuedness _β‰Ί_ (f x)) ,
   well-founded w (Ξ» x β†’ well-foundedness _β‰Ί_ (f x)) ,
   extensional
     (prop-valuedness _<_ (p , w , e , t))
     w
     (Ξ» x β†’ well-foundedness _β‰Ί_ (f x))
     e
     (Ξ» x β†’ extensionality _β‰Ί_ (f x)) ,
   transitive t (Ξ» x β†’ transitivity _β‰Ί_ (f x))

\end{code}

28 June 2018.

For a universe (and hence an injective type) 𝓦 and an embedding
j : X β†’ A, if every type in a family Y : X β†’ 𝓦 has the structure of an
ordinal, then so does every type in the extended family Y/j : A β†’ 𝓦.

                   j
              X ------> A
               \       /
                \     /
             Y   \   / Y/j
                  \ /
                   v
                   𝓦

This is a direct application of the construction in the module
OrdinalArithmetic.prop-indexed-product-of-ordinals.

This assumes X A : 𝓦, and that the given ordinal structure is
W-valued. More generally, we have the following typing, for which the
above triangle no longer makes sense, because Y / j : A β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦,
but the constructions still work.

\begin{code}

open import UF.Embeddings
open import UF.Equiv

module extension
        (fe : FunExt)
        {𝓀 π“₯ 𝓦}
        {X : 𝓀 Μ‡ }
        {A : π“₯ Μ‡ }
        (Y : X β†’ 𝓦 Μ‡ )
        (j : X β†’ A)
        (j-is-embedding : is-embedding j)
        (_<_ : {x : X} β†’ Y x β†’ Y x β†’ 𝓦 Μ‡ )
        (a : A)
       where

 open import InjectiveTypes.Blackboard fe

 private
  _β‰Ί_ : (Y / j) a β†’ (Y / j) a β†’ 𝓀 βŠ” π“₯ βŠ” 𝓦 Μ‡
  u β‰Ί v = Ξ£ p κž‰ fiber j a , u p < v p

 order = _β‰Ί_

 well-order : ((x : X) β†’ is-well-order (_<_ {x}))
            β†’ is-well-order _β‰Ί_
 well-order o = pip.well-order
                 (fe (𝓀 βŠ” π“₯) 𝓦)
                 (fiber j a)
                 (j-is-embedding a)
                 (Ξ» (p : fiber j a) β†’ Y (pr₁ p))
                 (Ξ» {p : fiber j a} y y' β†’ y < y')
                 (Ξ» (p : fiber j a) β†’ o (pr₁ p))

 top-preservation : ((x : X) β†’ has-top (_<_ {x})) β†’ has-top _β‰Ί_
 top-preservation f = Ο† , g
   where
    Ο† : (p : fiber j a) β†’ Y (pr₁ p)
    Ο† (x , r) = pr₁ (f x)

    g : (ψ : (Y / j) a) β†’ Β¬ (Ο† β‰Ί ψ)
    g ψ ((x , r) , l) = prβ‚‚ (f x) (ψ (x , r)) l

\end{code}