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}