Martin Escardo, 2018, April 2022.

The type of ordinals is (algebraically) injective.

\begin{code}

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

open import UF.FunExt

module Ordinals.Injectivity where

open import MLTT.Spartan
open import Notation.CanonicalMap
open import Ordinals.Equivalence
open import Ordinals.Maps
open import Ordinals.Type
open import Ordinals.Underlying
open import Ordinals.WellOrderArithmetic
open import UF.Base
open import UF.Embeddings
open import UF.Equiv
open import UF.Subsingletons-Properties
open import UF.Univalence

module ordinals-injectivity (fe : FunExt) where

open import InjectiveTypes.Blackboard fe

_↗_ : {I : 𝓤  ̇ } {J : 𝓥 ̇ }
→ (I → Ordinal 𝓦)
→ (I ↪ J)
→ (J → Ordinal (𝓤 ⊔ 𝓥 ⊔ 𝓦))
α ↗ (e , e-is-embedding) = λ j → ((a / e) j  ,
Extension.order j ,
Extension.well-order j (λ i → is-well-ordered (α i)))
where
a = λ i → ⟨ α i ⟩
module Extension = extension fe a e e-is-embedding (λ {i} → underlying-order (α i))

↗-propertyₒ : {I : 𝓤  ̇ } {J : 𝓥 ̇ }
(α : I → Ordinal 𝓦)
(𝓮@(e , e-is-embedding) : I ↪ J)
(i : I)
→ (α ↗ 𝓮) (e i) ≃ₒ α i
↗-propertyₒ {𝓤} {𝓥} {I} {J} α 𝓮@(e , e-is-embedding) i = γ
where
ϕ : ⟨ (α ↗ 𝓮) (e i) ⟩ ≃ ⟨ α i ⟩
ϕ = Π-extension-property (λ i → ⟨ α i ⟩) e e-is-embedding i

g : ⟨ (α ↗ 𝓮) (e i) ⟩ → ⟨ α i ⟩
g = ⌜ ϕ ⌝

g-is-equiv : is-equiv g
g-is-equiv = ⌜⌝-is-equiv ϕ

g-is-order-preserving : is-order-preserving ((α ↗ 𝓮) (e i)) (α i) g
g-is-order-preserving u v ((i' , p) , l) = m
where
q : (i' , p) ＝ (i , refl)
q = e-is-embedding (e i) (i' , p) (i , refl)

m : u (i , refl) ≺⟨ α i ⟩ v (i , refl)
m = transport (λ (i' , p) → u (i' , p) ≺⟨ α i' ⟩ v (i' , p)) q l

g⁻¹ : ⟨ α i ⟩ → ⟨ (α ↗ 𝓮) (e i) ⟩
g⁻¹ = ⌜ ϕ ⌝⁻¹

g⁻¹-is-order-preserving : is-order-preserving (α i) ((α ↗ 𝓮) (e i)) g⁻¹
g⁻¹-is-order-preserving x y l = (i , refl) , r
where
p : g⁻¹ x (i , refl) ＝ x
p = inverses-are-sections g g-is-equiv x

q : g⁻¹ y (i , refl) ＝ y
q = inverses-are-sections g g-is-equiv y

r : g⁻¹ x (i , refl) ≺⟨ α i ⟩ g⁻¹ y (i , refl)
r = transport₂ (λ x y → x ≺⟨ α  i ⟩ y) (p ⁻¹) (q ⁻¹) l

γ : (α ↗ 𝓮) (e i) ≃ₒ α i
γ = g , g-is-order-preserving , g-is-equiv , g⁻¹-is-order-preserving

↗-property : is-univalent (𝓤 ⊔ 𝓥)
→ {I : 𝓤  ̇ } {J : 𝓥 ̇ }
(α : I → Ordinal (𝓤 ⊔ 𝓥))
(𝓮@(e , e-is-embedding) : I ↪ J)
(i : I)
→ (α ↗ 𝓮) (e i) ＝ α i
↗-property ua α 𝓮@(e , e-is-embedding) i =
eqtoidₒ ua (fe _ _) ((α ↗ 𝓮) (e i)) (α i) (↗-propertyₒ α 𝓮 i)

Ordinal-is-ainjective : is-univalent (𝓤 ⊔ 𝓥)
→ ainjective-type (Ordinal (𝓤 ⊔ 𝓥)) 𝓤 𝓥
Ordinal-is-ainjective ua e e-is-embedding α = (α ↗ (e , e-is-embedding)) ,
↗-property ua α (e , e-is-embedding)

module topped-ordinals-injectivity (fe : FunExt) where

open import InjectiveTypes.Blackboard fe
open import Ordinals.ToppedType fe

_↗_ : {I : 𝓤  ̇ } {J : 𝓥 ̇ }
→ (I → Ordinalᵀ 𝓦)
→ (I ↪ J)
→ (J → Ordinalᵀ (𝓤 ⊔ 𝓥 ⊔ 𝓦))
τ ↗ (e , e-is-embedding) = λ j → ((t / e) j ,
Extension.order j ,
Extension.well-order j (λ i → tis-well-ordered (τ i))) ,
Extension.top-preservation j (λ i → topped (τ i))
where
t = λ x → ⟨ τ x ⟩
module Extension = extension fe t e e-is-embedding (λ {i} → underlying-order (τ i))

↗-propertyₒ : {I : 𝓤  ̇ } {J : 𝓥 ̇ }
(α : I → Ordinalᵀ 𝓦)
(𝓮@(e , e-is-embedding) : I ↪ J)
(i : I)
→ [ (α ↗ 𝓮) (e i) ] ≃ₒ [ α i ]
↗-propertyₒ α = ordinals-injectivity.↗-propertyₒ fe (λ i → [ α i ])

\end{code}

TODO. The type of compact∙ ordinals is injective. The type of ordinals
that have infs of complemented subsets is injective. These two results
are already proved in other modules, but these results are not
explicitly stated. We should refactor that code.

\begin{code}

open import UF.Univalence

module ordinals-injectivity-order (ua : Univalence) where

open import Ordinals.OrdinalOfOrdinals ua
open import UF.UA-FunExt
open import UF.Subsingletons

fe : FunExt
fe = Univalence-gives-FunExt ua

open ordinals-injectivity fe

↗-preserves-⊴ : {I J : 𝓤  ̇ } (𝓮 : I ↪ J)
(α β : I → Ordinal 𝓤)
→ ((i : I) → α i ⊴ β i)
→ (j : J) → (α ↗ 𝓮) j ⊴ (β ↗ 𝓮) j
↗-preserves-⊴ {𝓤} {I} {J} 𝓮@(e , e-is-embedding) α β ℓ j = f , fi , fop
where
h : (i : I) → ⟨ α i ⟩ → ⟨ β i ⟩
h i = pr₁ (ℓ i)

hi : (i : I) → is-initial-segment (α i) (β i) (h i)
hi i = pr₁ (pr₂ (ℓ i))

hop : (i : I) → is-order-preserving (α i) (β i) (h i)
hop i = pr₂ (pr₂ (ℓ i))

f : ⟨ (α ↗ 𝓮) j ⟩ → ⟨ (β ↗ 𝓮) j ⟩
f ϕ (i , refl) = h i (ϕ (i , refl))

fi : is-initial-segment ((α ↗ 𝓮) j) ((β ↗ 𝓮) j) f
fi ϕ γ ((i , refl) , m) = ⦅b⦆ ⦅a⦆
where
g⁻¹ : ⟨ α i ⟩ → ⟨ (α ↗ 𝓮) (e i) ⟩
g⁻¹ = case (↗-propertyₒ α 𝓮 i) of (λ (g , gop , geq , g⁻¹op) → inverse g geq)

w : fiber e (e i)
w = (i , refl)

u : w ＝ w
u = e-is-embedding (e i) w w

v : u ＝ 𝓻𝓮𝒻𝓵 w
v = props-are-sets (e-is-embedding (e i)) _ _

⦅a⦆ : Σ x ꞉ ⟨ α i ⟩ , (x ≺⟨ α i ⟩ ϕ (i , refl)) × (h i x ＝ γ (i , refl))
⦅a⦆ = hi i (ϕ (i , refl)) (γ (i , refl)) m

⦅b⦆ : type-of ⦅a⦆
→ Σ ϕ' ꞉ ⟨ (α ↗ 𝓮) (e i) ⟩ , (ϕ' ≺⟨ (α ↗ 𝓮) (e i) ⟩ ϕ) × (f ϕ' ＝ γ)
⦅b⦆ (x , n , t) = g⁻¹ x , (w , l) , dfunext (fe 𝓤 𝓤) H
where
p : g⁻¹ x w ＝ x
p = g⁻¹ x w                                     ＝⟨ refl ⟩
transport (λ - → ⟨ α (pr₁ -) ⟩) u x         ＝⟨ ⦅0⦆ ⟩
transport (λ - → ⟨ α (pr₁ -) ⟩) (𝓻𝓮𝒻𝓵 w) x ＝⟨ refl ⟩
x                                           ∎
where
⦅0⦆ = ap (λ - → transport (λ - → ⟨ α (pr₁ -) ⟩) - x) v

l : g⁻¹ x w ≺⟨ α i ⟩ ϕ w
l = transport (λ - → - ≺⟨ α i ⟩ ϕ w) (p ⁻¹) n

H : f (g⁻¹ x) ∼ γ
H (i' , r) =
f (g⁻¹ x) (i' , r)                              ＝⟨ ⦅1⦆ ⟩
transport (λ - → ⟨ β (pr₁ -) ⟩) q (f (g⁻¹ x) w) ＝⟨ ⦅3⦆ ⟩
transport (λ - → ⟨ β (pr₁ -) ⟩) q (γ w)         ＝⟨ ⦅4⦆ ⟩
γ (i' , r)                                      ∎
where
q : w ＝ (i' , r)
q = e-is-embedding (e i) w (i' , r)

⦅1⦆ = (apd ( f (g⁻¹ x)) q)⁻¹

⦅2⦆ = f (g⁻¹ x) w   ＝⟨ refl ⟩
h i (g⁻¹ x w) ＝⟨ ap (h i) p ⟩
h i x         ＝⟨ t ⟩
γ w           ∎

⦅3⦆ = ap (transport (λ - → ⟨ β (pr₁ -) ⟩) q) ⦅2⦆

⦅4⦆ = apd γ q

fop : is-order-preserving ((α ↗ 𝓮) j) ((β ↗ 𝓮) j) f
fop ϕ γ ((i , refl) , m) = (i , refl) , hop i (ϕ (i , refl)) (γ (i , refl)) m

module topped-ordinals-injectivity-order (ua : Univalence) where

open import UF.UA-FunExt

fe : FunExt
fe = Univalence-gives-FunExt ua

open import Ordinals.ToppedType fe
open import Ordinals.OrdinalOfOrdinals ua
open import UF.Subsingletons

open topped-ordinals-injectivity fe

↗-preserves-⊴ : {I J : 𝓤  ̇ } (𝓮 : I ↪ J)
(α β : I → Ordinalᵀ 𝓤)
→ ((i : I) → [ α i ] ⊴ [ β i ])
→ (j : J) → [ (α ↗ 𝓮) j ] ⊴ [ (β ↗ 𝓮) j ]
↗-preserves-⊴ 𝓮 α β =
ordinals-injectivity-order.↗-preserves-⊴ ua 𝓮 (λ i → [ α i ]) (λ i → [ β i ])

\end{code}