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}