Tom de Jong, 27 & 30 November and 7 & 8 December 2022.
In collaboration with Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu.

Cleaned up on 16, 17 and 19 December 2022.

Abstract
────────
We previously defined (in Ordinals/CumulativeHierarchy.lagda) the map
𝕍-to-Ord : 𝕍 → Ord
such that
𝕍-to-Ord (𝕍-set f) ＝ sup (λ a → 𝕍-to-Ord (f a) +ₒ 𝟙ₒ).

The recursive nature of 𝕍-to-Ord is convenient because it allows us to prove
properties by induction. Moreover, the supremum yields an ordinal by
construction.

We show here that this map also admits a nonrecursive description and pay
particular attention to the size issues involved.

Introduction
────────────
A natural function that turns elements of 𝕍 into types is the map that takes an
element x : 𝕍 to its total space, the type of elements contained in x,
Σ y ꞉ 𝕍 , y ∈ x.
Note that when x is a set theoretic ordinal, i.e. it is an element of x : 𝕍ᵒʳᵈ,
then, since being a set theoretic ordinal is hereditary, we have
(Σ y ꞉ 𝕍 , y ∈ x) ≃ (Σ y ꞉ 𝕍ᵒʳᵈ , y ∈ x).
Hence, the total space is an ordinal as it inherits the well-order from 𝕍ᵒʳᵈ.

However, the above does *not* define a map 𝕍 → Ord, because 𝕍, and hence the
total space, are large types, so that we get an ordinal in 𝓤 ⁺ and not in 𝓤, as
desired.

Still, we can prove that the total space yields an ordinal isomorphic to the one
obtained by 𝕍-to-Ord as the recursive supremum. In particular, it it thus
possible to give a more direct presentation, at least up to equivalence, of
𝕍-to-Ord (𝕍-set f) that is nonrecursive.

But we can do better, because the cumulative hierarchy 𝕍 is locally small,
meaning that its identity types are 𝓤-valued up to equivalence. We first observe
that the total space
Σ y ꞉ 𝕍 , y ∈ 𝕍-set f
is equivalent to the image of f : A → 𝕍 (with A : 𝓤), which is a small type up
to equivalence thanks to the fact that 𝕍 is locally small.

(This general fact on small images of maps into locally small sets is recorded
in the module set-replacement-construction in the file Quotient.GivesSetReplacement.)

Specifically, the image of f is equivalent to the set quotient A/~ where ~
relates two elements if f identifies them. We then prove that
𝕍-to-Ord (𝕍-set {A} f) ＝ (A/~ , <),
where [a] < [a'] is defined to hold when f a ∈ f a'.

Summary
───────
In summary, we prove two results:
(1) 𝕍-to-Ord (𝕍-set {A} f) and (A/~ , <) are equal as ordinals, and
(2) 𝕍-to-Ord x and the total space (Σ y ꞉ 𝕍 , y ∈ x) are isomorphic as
ordinals.
The isomorphism in (2) cannot be promoted to an equality (despite univalence),
because the type (Σ y ꞉ 𝕍 , y ∈ x) of elements contained in x is a large type.

\begin{code}

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

open import MLTT.Spartan

open import UF.PropTrunc
open import UF.Univalence

(pt : propositional-truncations-exist)
(ua : Univalence)
(𝓤 : Universe)
where

open import Quotient.Type hiding (is-prop-valued)
open import Quotient.GivesSetReplacement

open import UF.Base hiding (_≈_)
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.FunExt
open import UF.ImageAndSurjection pt
open import UF.Sets
open import UF.Size
open import UF.SubtypeClassifier
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UA-FunExt

open PropositionalTruncation pt

private
fe : Fun-Ext
fe = Univalence-gives-Fun-Ext ua

fe' : FunExt
fe' _ _ = fe

pe : Prop-Ext
pe = Univalence-gives-Prop-Ext ua

open import UF.CumulativeHierarchy pt fe pe
open import UF.CumulativeHierarchy-LocallySmall pt fe pe

open import Ordinals.CumulativeHierarchy pt ua 𝓤
open import Ordinals.Equivalence
open import Ordinals.Maps
open import Ordinals.Notions
open import Ordinals.OrdinalOfOrdinals ua
open import Ordinals.Type
open import Ordinals.Underlying
open import Ordinals.WellOrderTransport fe'

module _
(ch : cumulative-hierarchy-exists 𝓤)
where

open cumulative-hierarchy-exists ch

open 𝕍-is-locally-small ch
open ordinal-of-set-theoretic-ordinals ch

\end{code}

We start by showing that the total space (Σ y ꞉ 𝕍 , y ∈ x) of a set theoretic
ordinal x is a (large) type theoretic ordinal when ordered by membership.

\begin{code}

module total-space-of-an-element-of-𝕍
(x : 𝕍)
(σ : is-set-theoretic-ordinal x)
where

𝕋x : 𝓤 ⁺ ̇
𝕋x = Σ y ꞉ 𝕍 , y ∈ x

_∈ₓ_ : 𝕋x → 𝕋x → 𝓤 ⁺ ̇
u ∈ₓ v = pr₁ u ∈ pr₁ v

∈ₓ-is-prop-valued : is-prop-valued _∈ₓ_
∈ₓ-is-prop-valued u v = ∈-is-prop-valued

∈ₓ-is-transitive : is-transitive _∈ₓ_
∈ₓ-is-transitive u v w m n =
transitive-set-if-set-theoretic-ordinal
(being-set-theoretic-ordinal-is-hereditary σ (pr₂ w)) (pr₁ v) (pr₁ u) n m

∈ₓ-is-extensional : is-extensional _∈ₓ_
∈ₓ-is-extensional u v s t =
to-subtype-＝ (λ _ → ∈-is-prop-valued)
(∈-extensionality (pr₁ u) (pr₁ v) s' t')
where
s' : pr₁ u ⊆ pr₁ v
s' y y-in-u = s (y , τ) y-in-u
where
τ : y ∈ x
τ = transitive-set-if-set-theoretic-ordinal σ (pr₁ u) y (pr₂ u) y-in-u
t' : pr₁ v ⊆ pr₁ u
t' y y-in-v = t (y , τ) y-in-v
where
τ : y ∈ x
τ = transitive-set-if-set-theoretic-ordinal σ (pr₁ v) y (pr₂ v) y-in-v

∈ₓ-is-well-founded : is-well-founded _∈ₓ_
∈ₓ-is-well-founded = λ (y , m) → ρ y m
where
ρ : (y : 𝕍) (m : y ∈ x) → is-accessible _∈ₓ_ (y , m)
ρ = transfinite-induction _∈_ ∈-is-well-founded _ h
where
h : (y : 𝕍)
→ ((u : 𝕍) → u ∈ y → (m : u ∈ x) → is-accessible _∈ₓ_ (u , m))
→ (m : y ∈ x) → is-accessible _∈ₓ_ (y , m)
h y IH m = acc (λ (u , u-in-x) u-in-y → IH u u-in-y u-in-x)

𝕋xᵒʳᵈ : Ordinal (𝓤 ⁺)
𝕋xᵒʳᵈ = 𝕋x , _∈ₓ_ , ∈ₓ-is-prop-valued , ∈ₓ-is-well-founded
, ∈ₓ-is-extensional , ∈ₓ-is-transitive

total-spaceᵒʳᵈ : Ordinal (𝓤 ⁺)
total-spaceᵒʳᵈ = 𝕋xᵒʳᵈ

\end{code}

Because being an set theoretic ordinal is hereditary the total spaces
(Σ y ꞉ 𝕍 , y ∈ x) and (Σ y ꞉ 𝕍ᵒʳᵈ , y ∈ᵒʳᵈ (x , σ))
are equivalent, as we record below.

\begin{code}

𝕋x-restricted-to-𝕍ᵒʳᵈ : 𝓤 ⁺ ̇
𝕋x-restricted-to-𝕍ᵒʳᵈ = Σ y ꞉ 𝕍ᵒʳᵈ , y ∈ᵒʳᵈ (x , σ)

𝕋x-restricted-to-𝕍ᵒʳᵈ-≃-𝕋x : 𝕋x-restricted-to-𝕍ᵒʳᵈ ≃ 𝕋x
𝕋x-restricted-to-𝕍ᵒʳᵈ-≃-𝕋x = qinveq f (g , η , ε)
where
f : 𝕋x-restricted-to-𝕍ᵒʳᵈ → 𝕋x
f ((y , _) , m) = y , m
g : 𝕋x → 𝕋x-restricted-to-𝕍ᵒʳᵈ
g (y , m) = (y , (being-set-theoretic-ordinal-is-hereditary σ m)) , m
ε : f ∘ g ∼ id
ε (y , m) = to-subtype-＝ (λ _ → ∈-is-prop-valued) refl
η : g ∘ f ∼ id
η ((y , τ) , m) =
to-subtype-＝ (λ _ → ∈-is-prop-valued)
(to-subtype-＝ (λ _ → being-set-theoretic-ordinal-is-prop)
refl)

\end{code}

When x = 𝕍-set f, then the total space of x is equivalent to the image f,
because y ∈ 𝕍-set f if and only if y is in the image of f.

\begin{code}

module total-space-of-𝕍-set
(sq : set-quotients-exist)
{A : 𝓤 ̇ }
(f : A → 𝕍)
(σ : is-set-theoretic-ordinal (𝕍-set f))
where

private
x = 𝕍-set f

open total-space-of-an-element-of-𝕍 x σ
open general-set-quotients-exist sq

𝕋x-≃-image-f : 𝕋x ≃ image f
𝕋x-≃-image-f = Σ-cong h
where
h : (y : 𝕍) → (y ∈ x) ≃ y ∈image f
h y = logically-equivalent-props-are-equivalent
∈-is-prop-valued
(being-in-the-image-is-prop y f)
from-∈-of-𝕍-set
to-∈-of-𝕍-set

\end{code}

The well order on the total space induces a well order on the image of f.

\begin{code}

private
transfer : Σ s ꞉ OrdinalStructure (image f) , (image f , s) ≃ₒ 𝕋xᵒʳᵈ
transfer = transfer-structure (image f) 𝕋xᵒʳᵈ
(≃-sym 𝕋x-≃-image-f)
(_∈ₓ_ , (λ u v → ≃-refl (u ∈ₓ v)))

image-fᵒʳᵈ : Ordinal (𝓤 ⁺)
image-fᵒʳᵈ = image f , pr₁ transfer

𝕋xᵒʳᵈ-≃-image-fᵒʳᵈ : 𝕋xᵒʳᵈ ≃ₒ image-fᵒʳᵈ
𝕋xᵒʳᵈ-≃-image-fᵒʳᵈ = ≃ₒ-sym _ _ (pr₂ transfer)

\end{code}

As mentioned at the top of this file, the image of f : A → 𝕍 is equivalent to
the set quotient A/~ where ~ relates two elements of A if f identifies them.

We show that the relation ≺ on A/~ defined by [ a ] ≺ [ a' ] := f a ∈ f a' makes
this quotient into a type theoretic ordinal that moreover is isomorphic to the
ordinal image-fᵒʳᵈ.

Note that because equality on 𝕍 and ∈ take values in 𝓤 ⁺, this quotient
construction yields an ordinal in 𝓤 ⁺. We present a resized small-valued
variation of this construction below to get a quotient that lives in 𝓤, rather
than 𝓤 ⁺.

NB: We use the word "resized" here to indicate that we have a small type/ordinal
equivalent to a large one. We do *not* use resizing axioms.

\begin{code}

module 𝕍-set-carrier-quotient
(sq : set-quotients-exist)
{A : 𝓤 ̇ }
(f : A → 𝕍)
where

open general-set-quotients-exist sq
open extending-relations-to-quotient fe pe

_~_ : A → A → 𝓤 ⁺ ̇
a ~ b = f a ＝ f b

~EqRel : EqRel A
~EqRel = _~_ , (λ a b → 𝕍-is-large-set)
, (λ a → refl)
, (λ a b e → e ⁻¹)
, (λ a b c e₁ e₂ → e₁ ∙ e₂)

A/~ : 𝓤 ⁺ ̇
A/~ = A / ~EqRel

[_] : A → A/~
[_] = η/ ~EqRel

_≺[Ω]_ : A/~ → A/~ → Ω (𝓤 ⁺)
_≺[Ω]_ = extension-rel₂ ~EqRel (λ a b → f a ∈[Ω] f b) ρ
where
ρ : {a b a' b' : A}
→ a ~ a' → b ~ b' → f a ∈[Ω] f b ＝ f a' ∈[Ω] f b'
ρ {a} {b} {a'} {b'} e e' =
Ω-extensionality pe fe (transport₂ _∈_ e e')
(transport₂ _∈_ (e ⁻¹) (e' ⁻¹))

_≺_ : A/~ → A/~ → 𝓤 ⁺ ̇
a ≺ b = (a ≺[Ω] b) holds

≺-is-prop-valued : is-prop-valued _≺_
≺-is-prop-valued a b = holds-is-prop (a ≺[Ω] b)

≺-＝-∈ : {a b : A} → [ a ] ≺ [ b ] ＝ f a ∈ f b
≺-＝-∈ {a} {b} = ap (_holds) (extension-rel-triangle₂ ~EqRel _ _ a b)

∈-to-≺ : {a b : A} → f a ∈ f b → [ a ] ≺ [ b ]
∈-to-≺ = Idtofun⁻¹ ≺-＝-∈

≺-to-∈ : {a b : A} → [ a ] ≺ [ b ] → f a ∈ f b
≺-to-∈ = Idtofun ≺-＝-∈

≺-is-transitive : is-set-theoretic-ordinal (𝕍-set f)
→ is-transitive _≺_
≺-is-transitive σ = /-induction₃ fe ~EqRel prop-valued trans
where
prop-valued : (x y z : A / ~EqRel) → is-prop (x ≺ y → y ≺ z → x ≺ z)
prop-valued x y z = Π₂-is-prop fe (λ _ _ → ≺-is-prop-valued x z)
trans : (a b c : A) → [ a ] ≺ [ b ] → [ b ] ≺ [ c ] → [ a ] ≺ [ c ]
trans a b c m n = ∈-to-≺ (τ (f a) (≺-to-∈ n) (≺-to-∈ m))
where
τ : (v : 𝕍) → f b ∈ f c → v ∈ f b → v ∈ f c
τ = transitive-set-if-element-of-set-theoretic-ordinal σ
(to-∈-of-𝕍-set ∣ c , refl ∣) (f b)

≺-is-extensional : is-transitive-set (𝕍-set f)
→ is-extensional _≺_
≺-is-extensional τ =
/-induction₂ fe ~EqRel (λ x y → Π₂-is-prop fe (λ _ _ → /-is-set ~EqRel))
ext
where
ext : (a b : A)
→ ((x : A/~) → x ≺ [ a ] → x ≺ [ b ])
→ ((x : A/~) → x ≺ [ b ] → x ≺ [ a ])
→ [ a ] ＝ [ b ]
ext a b s t = η/-identifies-related-points ~EqRel e'
where
e' : a ~ b
e' = ∈-extensionality (f a) (f b) s' t'
where
lem : (x : 𝕍) (c : A) → x ∈ f c → ∃ d ꞉ A , f d ＝ x
lem x c m = from-∈-of-𝕍-set (τ (f c) x (to-∈-of-𝕍-set ∣ c , refl ∣) m)
s' : f a ⊆ f b
s' x m = ∥∥-rec ∈-is-prop-valued h (lem x a m)
where
h : (Σ c ꞉ A , f c ＝ x) → x ∈ f b
h (c , refl) = ≺-to-∈ (s [ c ] (∈-to-≺ m))
t' : f b ⊆ f a
t' x m = ∥∥-rec ∈-is-prop-valued h (lem x b m)
where
h : (Σ c ꞉ A , f c ＝ x) → x ∈ f a
h (c , refl) = ≺-to-∈ (t [ c ] (∈-to-≺ m))

≺-is-well-founded : is-well-founded _≺_
≺-is-well-founded = /-induction ~EqRel acc-is-prop acc''
where
acc-is-prop : (x : A/~) → is-prop (is-accessible _≺_ x)
acc-is-prop = accessibility-is-prop _≺_ fe'
acc' : (x : 𝕍) → ((a : A) → f a ＝ x → is-accessible _≺_ [ a ])
acc' = transfinite-induction _∈_ ∈-is-well-founded _ h
where
h : (x : 𝕍)
→ ((y : 𝕍) → y ∈ x → (a : A) → f a ＝ y → is-accessible _≺_ [ a ])
→ (a : A) → f a ＝ x → is-accessible _≺_ [ a ]
h x IH a refl =
acc (/-induction ~EqRel (λ _ → Π-is-prop fe (λ _ → acc-is-prop _)) α)
where
α : (b : A) → [ b ] ≺ [ a ] → is-accessible _≺_ [ b ]
α b m = IH (f b) (≺-to-∈ m) b refl
acc'' : (a : A) → is-accessible _≺_ [ a ]
acc'' a = acc' (f a) a refl

module quotient-as-ordinal
(σ : is-set-theoretic-ordinal (𝕍-set f))
where

A/~ᵒʳᵈ : Ordinal (𝓤 ⁺)
A/~ᵒʳᵈ = A/~ , _≺_
, ≺-is-prop-valued
, ≺-is-well-founded
, ≺-is-extensional (transitive-set-if-set-theoretic-ordinal σ)
, ≺-is-transitive σ

\end{code}

We now show that for x = 𝕍-set {A} f, the total space 𝕋xᵒʳᵈ and the above set
quotient A/~ᵒʳᵈ are equal as (large) ordinals. The equivalence of types is
proved generally in the module set-replacement-construction in the file
UF/Quotient.lagda. We only need to check that the equivalence is order
preserving and reflecting.

\begin{code}

private
x = 𝕍-set f

open total-space-of-an-element-of-𝕍 x σ
open total-space-of-𝕍-set sq f σ

open set-replacement-construction sq pt f
𝕍-is-locally-small
𝕍-is-large-set
hiding ([_])

private
ϕ : A/~ → image f
ϕ = quotient-to-image

ϕ-behaviour : (a : A) → ϕ [ a ] ＝ corestriction f a
ϕ-behaviour = universality-triangle/ ~EqRel
(image-is-set f 𝕍-is-large-set) (corestriction f) _

ϕ-is-order-preserving : is-order-preserving A/~ᵒʳᵈ image-fᵒʳᵈ ϕ
ϕ-is-order-preserving = /-induction₂ fe ~EqRel prop-valued preserve
where
prop-valued : (a' b' : A / ~EqRel)
→ is-prop (a' ≺ b' → underlying-order image-fᵒʳᵈ (ϕ a') (ϕ b'))
prop-valued a' b' = Π-is-prop fe (λ _ → prop-valuedness _
(is-well-ordered image-fᵒʳᵈ)
(ϕ a') (ϕ b'))
preserve : (a b : A)
→ [ a ] ≺ [ b ]
→ underlying-order image-fᵒʳᵈ (ϕ [ a ]) (ϕ [ b ])
preserve a b l = transport₂ (underlying-order image-fᵒʳᵈ) p q mon
where
mem : f a ∈ f b
mem = ≺-to-∈ l
mon : underlying-order image-fᵒʳᵈ (corestriction f a) (corestriction f b)
mon = mem
p : corestriction f a ＝ ϕ [ a ]
p = (ϕ-behaviour a) ⁻¹
q : corestriction f b ＝ ϕ [ b ]
q = (ϕ-behaviour b) ⁻¹

ϕ-is-order-reflecting : is-order-reflecting A/~ᵒʳᵈ image-fᵒʳᵈ ϕ
ϕ-is-order-reflecting = /-induction₂ fe ~EqRel prop-valued reflect
where
prop-valued : (a' b' : A/~)
→ is-prop (underlying-order image-fᵒʳᵈ (ϕ a') (ϕ b') → a' ≺ b')
prop-valued a' b' = Π-is-prop fe (λ _ → prop-valuedness _≺_
(is-well-ordered A/~ᵒʳᵈ) a' b')
reflect : (a b : A)
→ underlying-order image-fᵒʳᵈ (ϕ [ a ]) (ϕ [ b ])
→ [ a ] ≺ [ b ]
reflect a b l = ∈-to-≺ mem
where
p : ϕ [ a ] ＝ corestriction f a
p = ϕ-behaviour a
q : ϕ [ b ] ＝ corestriction f b
q = ϕ-behaviour b
mem : f a ∈ f b
mem = transport₂ (underlying-order image-fᵒʳᵈ) p q l

total-space-is-quotientᵒʳᵈ : 𝕋xᵒʳᵈ ＝ A/~ᵒʳᵈ
total-space-is-quotientᵒʳᵈ = 𝕋xᵒʳᵈ      ＝⟨ ⦅1⦆ ⟩
image-fᵒʳᵈ ＝⟨ ⦅2⦆ ⟩
A/~ᵒʳᵈ     ∎
where
⦅1⦆ = eqtoidₒ (ua (𝓤 ⁺)) fe 𝕋xᵒʳᵈ image-fᵒʳᵈ 𝕋xᵒʳᵈ-≃-image-fᵒʳᵈ
⦅2⦆ = eqtoidₒ (ua (𝓤 ⁺)) fe
image-fᵒʳᵈ A/~ᵒʳᵈ
(≃ₒ-sym A/~ᵒʳᵈ image-fᵒʳᵈ (ϕ , ϕ-is-order-equiv))
where
ϕ-is-order-equiv : is-order-equiv A/~ᵒʳᵈ image-fᵒʳᵈ ϕ
ϕ-is-order-equiv =
order-preserving-reflecting-equivs-are-order-equivs _ _
ϕ (⌜⌝⁻¹-is-equiv image-≃-quotient)
ϕ-is-order-preserving
ϕ-is-order-reflecting

\end{code}

Next, we make use of the fact that the cumulative hierarchy 𝕍 is locally small,
as shown in UF/CumulativeHierarchy-LocallySmall.lagda, to construct a small quotient
A/~⁻ equivalent to A/~.

In general, we use the symbol ⁻ to indicate a resized small-valued analogue.

\begin{code}

_~⁻_ : A → A → 𝓤 ̇
a ~⁻ b = f a ＝⁻ f b

~⁻EqRel : EqRel A
~⁻EqRel = _~⁻_ , (λ a b → ＝⁻-is-prop-valued)
, (λ a → ＝⁻-is-reflexive)
, (λ a b → ＝⁻-is-symmetric)
, (λ a b c → ＝⁻-is-transitive)

A/~⁻ : 𝓤 ̇
A/~⁻ = A / ~⁻EqRel

A/~-≃-A/~⁻ : A/~ ≃ A/~⁻
A/~-≃-A/~⁻ = quotients-equivalent A ~EqRel ~⁻EqRel (＝-to-＝⁻ , ＝⁻-to-＝)

\end{code}

The small-valued membership relation ∈⁻ developed in the aforementioned file now
allows us to define a small-valued relation ≺' on A/~ and transfer the well
order on A/~ to A/~⁻, for which we use the machinery developed by Martín Escardó
in Ordinals/WellOrderTransport.lagda.

\begin{code}

private
≺-has-small-values : (x y : A/~) → is-small (x ≺ y)
≺-has-small-values =
/-induction₂ fe ~EqRel
(λ x y → being-small-is-prop ua (x ≺ y) 𝓤)
(λ a b → (f a ∈⁻ f b)
, ((f a ∈⁻ f b)    ≃⟨ ∈⁻-≃-∈ ⟩
(f a ∈ f b)     ≃⟨ idtoeq _ _ (≺-＝-∈ ⁻¹) ⟩
([ a ] ≺ [ b ]) ■))

_≺'_ : A/~ → A/~ → 𝓤 ̇
x ≺' y = pr₁ (≺-has-small-values x y)

≺-≃-≺' : {x y : A/~} → x ≺ y ≃ x ≺' y
≺-≃-≺' {x} {y} = ≃-sym (pr₂ (≺-has-small-values x y))

module small-quotient-as-ordinal
(σ : is-set-theoretic-ordinal (𝕍-set f))
where

open quotient-as-ordinal σ

private
resize-ordinal : Σ s ꞉ OrdinalStructure A/~⁻ , (A/~⁻ , s) ≃ₒ A/~ᵒʳᵈ
resize-ordinal = transfer-structure A/~⁻ A/~ᵒʳᵈ (≃-sym A/~-≃-A/~⁻)
(_≺'_ , (λ x y → ≺-≃-≺'))

A/~⁻ᵒʳᵈ : Ordinal 𝓤
A/~⁻ᵒʳᵈ = A/~⁻ , pr₁ resize-ordinal

A/~⁻ᵒʳᵈ-≃ₒ-A/~ᵒʳᵈ : A/~⁻ᵒʳᵈ ≃ₒ A/~ᵒʳᵈ
A/~⁻ᵒʳᵈ-≃ₒ-A/~ᵒʳᵈ = pr₂ resize-ordinal

A/~ᵒʳᵈ--≃ₒ-A/~⁻ᵒʳᵈ : A/~ᵒʳᵈ ≃ₒ A/~⁻ᵒʳᵈ
A/~ᵒʳᵈ--≃ₒ-A/~⁻ᵒʳᵈ = ≃ₒ-sym A/~⁻ᵒʳᵈ A/~ᵒʳᵈ A/~⁻ᵒʳᵈ-≃ₒ-A/~ᵒʳᵈ

[_]⁻ : A → A/~⁻
[_]⁻ = ⌜ A/~-≃-A/~⁻ ⌝ ∘ [_]

[]⁻-is-surjection : is-surjection [_]⁻
[]⁻-is-surjection = ∘-is-surjection (surjection-induction-converse [_] λ P → /-induction ~EqRel) (equivs-are-surjections (⌜⌝-is-equiv A/~-≃-A/~⁻))

_≺⁻_ : A/~⁻ → A/~⁻ → 𝓤 ̇
_≺⁻_ = underlying-order A/~⁻ᵒʳᵈ

\end{code}

We relate the order ≺⁻ on the small quotient A/~⁻ to the order ≺ on the large
quotient A/~ and the set membership relation ∈ on 𝕍.

\begin{code}

≺⁻-≃-≺ : {a b : A} → [ a ]⁻ ≺⁻ [ b ]⁻ ≃ [ a ] ≺ [ b ]
≺⁻-≃-≺ {a} {b} = logically-equivalent-props-are-equivalent
(prop-valuedness _≺⁻_ (is-well-ordered A/~⁻ᵒʳᵈ)
[ a ]⁻ [ b ]⁻)
(≺-is-prop-valued [ a ] [ b ])
(⦅2⦆ [ a ] [ b ])
(⦅1⦆ [ a ] [ b ])
where
φ⁺ : A/~⁻ᵒʳᵈ ≃ₒ A/~ᵒʳᵈ
φ⁺ = A/~⁻ᵒʳᵈ-≃ₒ-A/~ᵒʳᵈ
φ⁻¹ : A/~ → A/~⁻
φ⁻¹ = ≃ₒ-to-fun⁻¹ _ _ φ⁺
φ-is-order-equiv : is-order-equiv A/~⁻ᵒʳᵈ A/~ᵒʳᵈ (≃ₒ-to-fun _ _ φ⁺)
φ-is-order-equiv = ≃ₒ-to-fun-is-order-equiv _ _ φ⁺
⦅1⦆ : (x y : A/~) → x ≺ y → φ⁻¹ x ≺⁻ φ⁻¹ y
⦅1⦆ = inverses-of-order-equivs-are-order-preserving A/~⁻ᵒʳᵈ A/~ᵒʳᵈ
φ-is-order-equiv
⦅2⦆ : (x y : A/~) → φ⁻¹ x ≺⁻ φ⁻¹ y → x ≺ y
⦅2⦆ = inverses-of-order-equivs-are-order-reflecting A/~⁻ᵒʳᵈ A/~ᵒʳᵈ
φ-is-order-equiv

≺⁻-≃-∈ : {a b : A} → [ a ]⁻ ≺⁻ [ b ]⁻ ≃ f a ∈ f b
≺⁻-≃-∈ {a} {b} = [ a ]⁻ ≺⁻ [ b ]⁻ ≃⟨ ≺⁻-≃-≺ ⟩
([ a ] ≺ [ b ])  ≃⟨ idtoeq _ _ ≺-＝-∈ ⟩
f a ∈ f b        ■

≺⁻-to-∈ : {a b : A} → [ a ]⁻ ≺⁻ [ b ]⁻ → f a ∈ f b
≺⁻-to-∈ = ⌜ ≺⁻-≃-∈ ⌝

∈-to-≺⁻ : {a b : A} → f a ∈ f b → [ a ]⁻ ≺⁻ [ b ]⁻
∈-to-≺⁻ = ⌜ ≺⁻-≃-∈ ⌝⁻¹

\end{code}

Because A/~⁻ᵒʳᵈ is a small ordinal in 𝓤, it now typechecks to ask whether it
equals the recursive supremum given by 𝕍ᵒʳᵈ-to-Ord (𝕍-set f).

This is indeed the case and because Ord-to-𝕍ᵒʳᵈ is left-cancellable, it suffices
to show that
Ord-to-𝕍 (A/~ᵒʳᵈ) ＝ 𝕍-set f.
This boils down to proving the equality
f a ＝ Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ [ a ]⁻)
for every a : A, where ↓ denotes taking the initial segment.

We slightly generalise this statement so that we can prove it by transfinite
induction on A/~⁻ᵒʳᵈ.

\begin{code}

initial-segments-of-A/~⁻ᵒʳᵈ-are-given-by-f :
(a' : A/~⁻) (a : A)
→ a' ＝ [ a ]⁻
→ Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ [ a ]⁻) ＝ f a
initial-segments-of-A/~⁻ᵒʳᵈ-are-given-by-f =
transfinite-induction _≺⁻_ (Well-foundedness A/~⁻ᵒʳᵈ) _ ind-proof
where
ind-proof : (a' : A/~⁻)
→ ((b' : A/~⁻) → b' ≺⁻ a'
→ (b : A) → b' ＝ [ b ]⁻
→ Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ [ b ]⁻) ＝ f b)
→ (a : A) → a' ＝ [ a ]⁻ → Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ [ a ]⁻) ＝ f a
ind-proof a' IH a refl = ∈-extensionality _ _ ⦅1⦆ ⦅2⦆
where
↓a : Ordinal 𝓤
↓a = A/~⁻ᵒʳᵈ ↓ [ a ]⁻

⦅1⦆ : Ord-to-𝕍 ↓a ⊆ f a
⦅1⦆ x m = ∥∥-rec ∈-is-prop-valued ⦅1⦆' fact
where
lemma : (b : A)
→ f b ∈ f a
→ x ＝ Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ [ b ]⁻)
→ x ∈ f a
lemma b n e = transport (_∈ f a) (e' ⁻¹) n
where
e' = x                           ＝⟨ e                            ⟩
Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ [ b ]⁻) ＝⟨ IH [ b ]⁻ (∈-to-≺⁻ n) b refl ⟩
f b                         ∎

fact : ∃ b' ꞉ ⟨ ↓a ⟩ , Ord-to-𝕍 (↓a ↓ b') ＝ x
fact = from-∈-of-𝕍-set (transport (x ∈_) (Ord-to-𝕍-behaviour ↓a) m)

⦅1⦆' : (Σ b' ꞉ ⟨ A/~⁻ᵒʳᵈ ↓ [ a ]⁻ ⟩ , Ord-to-𝕍 (↓a ↓ b') ＝ x)
→ x ∈ f a
⦅1⦆' ((b' , l) , e) = ∥∥-rec ∈-is-prop-valued h ([]⁻-is-surjection b')
where
h : (Σ b ꞉ A , [ b ]⁻ ＝ b') → x ∈ f a
h (b , refl) = lemma b (≺⁻-to-∈ l) e'
where
e' = x                            ＝⟨ e ⁻¹ ⟩
Ord-to-𝕍 (↓a ↓ ([ b ]⁻ , l)) ＝⟨ e''  ⟩
Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ [ b ]⁻)  ∎
where
e'' = ap Ord-to-𝕍 (iterated-↓ A/~⁻ᵒʳᵈ [ a ]⁻ [ b ]⁻ l)

⦅2⦆ : f a ⊆ Ord-to-𝕍 ↓a
⦅2⦆ x m = ∥∥-rec ∈-is-prop-valued (λ (b , n , e) → ⦅2⦆' b n e) fact
where
fact : ∃ b ꞉ A , (f b ∈ f a) × (f b ＝ x)
fact = ∥∥-functor h fact'
where
fact' : ∃ b ꞉ A , f b ＝ x
fact' = from-∈-of-𝕍-set (transitive-set-if-set-theoretic-ordinal σ
(f a) x (to-∈-of-𝕍-set ∣ a , refl ∣) m)
abstract
h : (Σ b ꞉ A , f b ＝ x)
→ Σ b ꞉ A , (f b ∈ f a) × (f b ＝ x)
h (b , e) = b , transport⁻¹ (_∈ f a) e m , e

lemma : (b : A)
→ f b ∈ f a
→ f b ＝ x
→ Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ [ b ]⁻) ＝ x
lemma b n e = IH [ b ]⁻ (∈-to-≺⁻ n) b refl ∙ e

⦅2⦆' : (b : A)
→ f b ∈ f a
→ f b ＝ x
→ x ∈ Ord-to-𝕍 ↓a
⦅2⦆' b n e = transport (_∈ Ord-to-𝕍 ↓a) (lemma b n e) mem
where
mem' : Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ [ b ]⁻) ∈ 𝕍-set (λ b' → Ord-to-𝕍 (↓a ↓ b'))
mem' = to-∈-of-𝕍-set ∣ ([ b ]⁻ , ∈-to-≺⁻ n) , e' ∣
where
e' : Ord-to-𝕍 (↓a ↓ ([ b ]⁻ , ∈-to-≺⁻ n))
＝ Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ [ b ]⁻)
e' = ap Ord-to-𝕍 (iterated-↓ A/~⁻ᵒʳᵈ [ a ]⁻ [ b ]⁻ (∈-to-≺⁻ n))
mem : Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ [ b ]⁻) ∈ Ord-to-𝕍 ↓a
mem = transport⁻¹ (Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ [ b ]⁻) ∈_)
(Ord-to-𝕍-behaviour ↓a)
mem'

\end{code}

Using that Ord-to-𝕍ᵒʳᵈ is left-cancellable and a retraction of 𝕍ᵒʳᵈ-to-Ord, we
now prove that the recursive supremum given by 𝕍ᵒʳᵈ-to-Ord (𝕍-set f) is equal to
the nonrecursive set quotient A/~⁻ᵒʳᵈ.

\begin{code}

open 𝕍-to-Ord-construction sq

𝕍ᵒʳᵈ-to-Ord-is-quotient-of-carrier : 𝕍ᵒʳᵈ-to-Ord (𝕍-set f , σ) ＝ A/~⁻ᵒʳᵈ
𝕍ᵒʳᵈ-to-Ord-is-quotient-of-carrier =
Ord-to-𝕍-is-left-cancellable (𝕍ᵒʳᵈ-to-Ord (𝕍-set f , σ)) A/~⁻ᵒʳᵈ e
where
e = Ord-to-𝕍 (𝕍ᵒʳᵈ-to-Ord (𝕍-set f , σ))   ＝⟨ ap pr₁ ⦅1⦆        ⟩
𝕍-set f                                ＝⟨ 𝕍-set-ext _ _ ⦅2⦆ ⟩
𝕍-set (λ a' → Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ a')) ＝⟨ ⦅3⦆               ⟩
Ord-to-𝕍 A/~⁻ᵒʳᵈ                       ∎
where
⦅1⦆ : Ord-to-𝕍ᵒʳᵈ (𝕍ᵒʳᵈ-to-Ord (𝕍-set f , σ)) ＝ 𝕍-set f , σ
⦅1⦆ = 𝕍ᵒʳᵈ-to-Ord-is-section-of-Ord-to-𝕍ᵒʳᵈ (𝕍-set f , σ)
⦅2⦆ : f ≈ (λ a' → Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ a'))
⦅2⦆ = ⦅2⦆ˡ , ⦅2⦆ʳ
where
⦅2⦆ˡ : f ≲ (λ a' → Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ a'))
⦅2⦆ˡ a =
∣ [ a ]⁻ , initial-segments-of-A/~⁻ᵒʳᵈ-are-given-by-f [ a ]⁻ a refl ∣
⦅2⦆ʳ : (λ a' → Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ a')) ≲ f
⦅2⦆ʳ a' = ∥∥-functor h ([]⁻-is-surjection a')
where
h : (Σ a ꞉ A , [ a ]⁻ ＝ a')
→ (Σ a ꞉ A , f a ＝ Ord-to-𝕍 (A/~⁻ᵒʳᵈ ↓ a'))
h (a , refl) =
a , ((initial-segments-of-A/~⁻ᵒʳᵈ-are-given-by-f a' a refl) ⁻¹)
⦅3⦆ = (Ord-to-𝕍-behaviour A/~⁻ᵒʳᵈ) ⁻¹

\end{code}

Finally, using that the total space of (𝕍-set {A} f) and A/~ are equal as
(large) ordinals we distill a proof that 𝕍ᵒʳᵈ-to-Ord x is isomorphic as an
ordinal to the total space 𝕋xᵒʳᵈ of x.

\begin{code}

module _
(sq : set-quotients-exist)
where

open total-space-of-an-element-of-𝕍
open 𝕍-to-Ord-construction sq

𝕍ᵒʳᵈ-to-Ord-is-isomorphic-to-total-space :
(x : 𝕍) (σ : is-set-theoretic-ordinal x)
→ 𝕍ᵒʳᵈ-to-Ord (x , σ) ≃ₒ total-spaceᵒʳᵈ x σ
𝕍ᵒʳᵈ-to-Ord-is-isomorphic-to-total-space = 𝕍-prop-simple-induction _
prop-valued γ
where
prop-valued : (x : 𝕍)
→ is-prop ((σ : is-set-theoretic-ordinal x) → 𝕍ᵒʳᵈ-to-Ord (x , σ)
≃ₒ total-spaceᵒʳᵈ x σ)
prop-valued x = Π-is-prop fe (λ σ → ≃ₒ-is-prop-valued fe _ _)
γ : {A : 𝓤 ̇ } (f : A → 𝕍) (σ : is-set-theoretic-ordinal (𝕍-set f))
→ 𝕍ᵒʳᵈ-to-Ord (𝕍-set f , σ) ≃ₒ total-spaceᵒʳᵈ (𝕍-set f) σ
γ {A} f σ = ≃ₒ-trans (𝕍ᵒʳᵈ-to-Ord (𝕍-set f , σ))
A/~⁻ᵒʳᵈ
(total-spaceᵒʳᵈ (𝕍-set f) σ)
⦅1⦆ ⦅2⦆
where
open 𝕍-set-carrier-quotient sq f
open small-quotient-as-ordinal σ
open quotient-as-ordinal σ
⦅1⦆ : 𝕍ᵒʳᵈ-to-Ord (𝕍-set f , σ) ≃ₒ A/~⁻ᵒʳᵈ
⦅1⦆ = idtoeqₒ _ _ 𝕍ᵒʳᵈ-to-Ord-is-quotient-of-carrier
⦅2⦆ : A/~⁻ᵒʳᵈ ≃ₒ total-spaceᵒʳᵈ (𝕍-set f) σ
⦅2⦆ = ≃ₒ-sym _ _ (≃ₒ-trans (total-spaceᵒʳᵈ (𝕍-set f) σ)
A/~ᵒʳᵈ
A/~⁻ᵒʳᵈ
⦅3⦆ ⦅4⦆)
where
⦅3⦆ : total-spaceᵒʳᵈ (𝕍-set f) σ ≃ₒ A/~ᵒʳᵈ
⦅3⦆ = idtoeqₒ _ _ total-space-is-quotientᵒʳᵈ
⦅4⦆ : A/~ᵒʳᵈ ≃ₒ A/~⁻ᵒʳᵈ
⦅4⦆ = A/~ᵒʳᵈ--≃ₒ-A/~⁻ᵒʳᵈ

\end{code}