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.

Fredrik Nordvall Forsberg, 3 November 2023: Changed order of multiplication to
reverse lexicographic order to adhere to the standard convention.

Martin Escardo 13th September 2024. But notice that for sums we can't do this swap, due to type dependency, and hence *swapped* mulplication is a particular case of ordinal sum.

\begin{code}

module times
        {๐“ค ๐“ฅ ๐“ฆ ๐“ฃ}
        {X : ๐“ค ฬ‡ }
        {Y : ๐“ฅ ฬ‡ }
        (_<_ : X โ†’ X โ†’ ๐“ฆ ฬ‡ )
        (_โ‰บ_ : Y โ†’ Y โ†’ ๐“ฃ ฬ‡ )
       where

 private
  _โŠ_ : X ร— Y โ†’ X ร— Y โ†’ ๐“ฃ โŠ” ๐“ฅ โŠ” ๐“ฆ ฬ‡
  (a , b) โŠ (x , y) = (b โ‰บ y) + ((b ๏ผ y) ร— (a < x))

 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 _โŠ_

   ฮณ : (y : Y)
     โ†’ ((y' : Y) โ†’ y' โ‰บ y โ†’ (x' : X) โ†’ P (x' , y'))
     โ†’ (x : X) โ†’ P (x , y)
   ฮณ y s = transfinite-induction _<_ w (ฮป x โ†’ P (x , y)) (ฮป x f โ†’ acc (ฯˆ x f))
    where
     ฯˆ : (x : X)
       โ†’ ((x' : X) โ†’ x' < x โ†’ P (x' , y))
       โ†’ (z' : X ร— Y) โ†’ z' โŠ (x , y) โ†’ P z'
     ฯˆ x f (x' , y') (inl l) = s y' l x'
     ฯˆ x f (x' , y') (inr (r , m)) = transportโปยน P p ฮฑ
      where
       ฮฑ : P (x' , y)
       ฮฑ = f x' m

       p : (x' , y') ๏ผ (x' , y)
       p = to-ร—-๏ผ refl r

   ฯ† : (x : X) (y : Y) โ†’ P (x , y)
   ฯ† x y = transfinite-induction _โ‰บ_ w' (ฮป y โ†’ (x : X) โ†’ P (x , y)) ฮณ y x

 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 (ฮป - โ†’ b โ‰บ -) q l)
   f (inr (r , l)) (inl m)          = inl (transportโปยน (ฮป - โ†’ - โ‰บ v) 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 , b) (inr (refl , l)))
             (ฮป (m : b โ‰บ y)
                โ†’ ๐Ÿ˜-elim (irreflexive _<_ a (w a)
                           (Cases (g (a , b) (inl m))
                             (ฮป (n : b โ‰บ b)
                                โ†’ ๐Ÿ˜-elim (irreflexive _โ‰บ_ b (w' b) n))
                             (ฮป (ฯƒ : (b ๏ผ b) ร— (a < a))
                                โ†’ ๐Ÿ˜-elim (irreflexive _<_ a (w a) (prโ‚‚ ฯƒ))))))
             (ฮป (ฯƒ : (b ๏ผ y) ร— (u < x)) โ†’ prโ‚‚ ฯƒ)

   g' : (u : X) โ†’ u < x โ†’ u < a
   g' u l = Cases (g (u , y) (inr (refl , l)))
             (ฮป (m : y โ‰บ b)
                โ†’ Cases (f (x , y) (inl m))
                   (ฮป (m : y โ‰บ y) โ†’ ๐Ÿ˜-elim (irreflexive _โ‰บ_ y (w' y) m))
                   (ฮป (ฯƒ : (y ๏ผ y) ร— (x < x))
                      โ†’ ๐Ÿ˜-elim (irreflexive _<_ x (w x) (prโ‚‚ ฯƒ))))
             (ฮป (ฯƒ : (y ๏ผ b) ร— (u < a)) โ†’ prโ‚‚ ฯƒ)

   p : a ๏ผ x
   p = e a x f' g'

   f'' : (v : Y) โ†’ v โ‰บ b โ†’ v โ‰บ y
   f'' v l = Cases (f (x , v) (inl l))
              (ฮป (m : v โ‰บ y) โ†’ m)
              (ฮป (ฯƒ : (v ๏ผ y) ร— (x < x))
                 โ†’ ๐Ÿ˜-elim (irreflexive _<_ x (w x) (prโ‚‚ ฯƒ)))

   g'' : (v : Y) โ†’ v โ‰บ y โ†’ v โ‰บ b
   g'' v l = Cases (g (a , v) (inl l))
              (ฮป (m : v โ‰บ b) โ†’ m)
              (ฮป (ฯƒ : (v ๏ผ b) ร— (a < a))
                 โ†’ ๐Ÿ˜-elim (irreflexive _<_ a (w a) (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' b y l m)
   prop-valued (a , b) (x , y) (inl l) (inr (s , m)) =
    ๐Ÿ˜-elim (irreflexive _โ‰บ_ y (w' y) (transport (ฮป - โ†’ - โ‰บ y) s l))
   prop-valued (a , b) (x , y) (inr (r , l)) (inl m) =
    ๐Ÿ˜-elim (irreflexive _โ‰บ_ y (w' y) (transport (ฮป - โ†’ - โ‰บ y) 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 a x 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) = g y' l
   h (x' , y') (inr (r , l)) = f x' 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 (u y')
   (ฮป (l : y โ‰บ y') โ†’ inl (inl l))
   (cases
     (ฮป (p : y ๏ผ y')
        โ†’ Cases (t x')
           (ฮป (l : x < x')
              โ†’ inl (inr (p , l)))
           (cases
             (ฮป (q : x ๏ผ x')
                โ†’ inr (inl (to-ร—-๏ผ q p)))
             (ฮป (l : x' < x) โ†’ inr (inr (inr ((p โปยน) , l))))))
     (ฮป (l : y' โ‰บ y) โ†’ 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.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                    ๏ผโŸจ I p q โŸฉ
                                   transport Y p (transportโปยน Y p y') ๏ผโŸจ II p โŸฉ
                                   y'                                 โˆŽ
                                      )))))
             (ฮป (l : transportโปยน Y p y' โ‰บ y) โ†’ inr (inr (inr ((p โปยน) , l))))))
     (ฮป (l : x' < x) โ†’ inr (inr (inl l))))
      where
       I  = ฮป p โ†’ ap (transport Y p)
       II = back-and-forth-transport

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

We can prove extensionality from cotransitivity, but this doesn't seem
to be very useful, as cotransivitiy doesn't have good preservation
properties.

\begin{code}

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

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}