\begin{code}

{-# OPTIONS --without-K --exact-split --safe --auto-inline --experimental-lossy-unification #-}

open import MLTT.Spartan

open import UF.PropTrunc
open import UF.Univalence

module OrdinalCumulativeHierarchy-Addendum
        (pt : propositional-truncations-exist)
        (ua : Univalence)
        (𝓀 : Universe)
       where

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.Size
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.Quotient hiding (is-prop-valued)
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 CumulativeHierarchy pt fe pe
open import CumulativeHierarchy-LocallySmall pt fe pe
open import OrdinalCumulativeHierarchy pt ua 𝓀

open import Ordinals.Notions
open import Ordinals.OrdinalOfOrdinals ua
open import Ordinals.Type
open import Ordinals.WellOrderTransport fe'
open import Ordinals.Underlying

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 = step (Ξ» (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 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}

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 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 fe pe (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-β‰Ί = back-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 =
       step (/-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β‚’ 𝕋xα΅’Κ³α΅ˆ image-fα΅’Κ³α΅ˆ 𝕋xα΅’Κ³α΅ˆ-≃-image-fα΅’Κ³α΅ˆ
     β¦…2⦆ = eqtoidβ‚’ 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 Ξ¨α΅’Κ³α΅ˆ (𝕍-set f).

This is indeed the case and because Ξ¦α΅’Κ³α΅ˆ is left-cancellable, it suffices
to show that
  Ξ¦ (A/~α΅’Κ³α΅ˆ) ＝ 𝕍-set f.
This boils down to proving the equality
  f a ＝ Ξ¦ (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 ]⁻
    β†’ Ξ¦ (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 ]⁻
                               β†’ Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ [ b ]⁻) ＝ f b)
                β†’ (a : A) β†’ a' ＝ [ a ]⁻ β†’ Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ [ a ]⁻) ＝ f a
      ind-proof a' IH a refl = ∈-extensionality _ _ β¦…1⦆ β¦…2⦆
       where
        ↓a : Ordinal 𝓀
        ↓a = A/~β»α΅’Κ³α΅ˆ ↓ [ a ]⁻

        β¦…1⦆ : Ξ¦ ↓a βŠ† f a
        β¦…1⦆ x m = βˆ₯βˆ₯-rec ∈-is-prop-valued β¦…1⦆' fact
         where
          lemma : (b : A)
                β†’ f b ∈ f a
                β†’ x ＝ Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ [ b ]⁻)
                β†’ x ∈ f a
          lemma b n e = transport (_∈ f a) (e' ⁻¹) n
           where
            e' = x                   ＝⟨ e                            ⟩
                 Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ [ b ]⁻) ＝⟨ IH [ b ]⁻ (∈-to-≺⁻ n) b refl ⟩
                 f b                ∎

          fact : βˆƒ b' κž‰ ⟨ ↓a ⟩ , Ξ¦ (↓a ↓ b') ＝ x
          fact = from-∈-of-𝕍-set (transport (x ∈_) (Ξ¦-behaviour ↓a) m)

          β¦…1⦆' : (Ξ£ b' κž‰ ⟨ A/~β»α΅’Κ³α΅ˆ ↓ [ a ]⁻ ⟩ , Ξ¦ (↓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 ⁻¹ ⟩
                   Ξ¦ (↓a ↓ ([ b ]⁻ , l)) ＝⟨ e''  ⟩
                   Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ [ b ]⁻)  ∎
               where
                e'' = ap Ξ¦ (iterated-↓ A/~β»α΅’Κ³α΅ˆ [ a ]⁻ [ b ]⁻ l)

        β¦…2⦆ : f a βŠ† Ξ¦ ↓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
                β†’ Ξ¦ (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 ∈ Ξ¦ ↓a
          β¦…2⦆' b n e = transport (_∈ Ξ¦ ↓a) (lemma b n e) mem
           where
            mem' : Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ [ b ]⁻) ∈ 𝕍-set (Ξ» b' β†’ Ξ¦ (↓a ↓ b'))
            mem' = to-∈-of-𝕍-set ∣ ([ b ]⁻ , ∈-to-≺⁻ n) , e' ∣
             where
              e' : Ξ¦ (↓a ↓ ([ b ]⁻ , ∈-to-≺⁻ n))
                 ＝ Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ [ b ]⁻)
              e' = ap Ξ¦ (iterated-↓ A/~β»α΅’Κ³α΅ˆ [ a ]⁻ [ b ]⁻ (∈-to-≺⁻ n))
            mem : Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ [ b ]⁻) ∈ Ξ¦ ↓a
            mem = transport⁻¹ (Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ [ b ]⁻) ∈_)
                              (Ξ¦-behaviour ↓a)
                              mem'

\end{code}

Using that Ξ¦α΅’Κ³α΅ˆ is left-cancellable and a retraction of Ξ¨α΅’Κ³α΅ˆ, we
now prove that the recursive supremum given by Ξ¨α΅’Κ³α΅ˆ (𝕍-set f) is equal to
the nonrecursive set quotient A/~β»α΅’Κ³α΅ˆ.

\begin{code}

   open Ξ¨-construction sq

   Ξ¨α΅’Κ³α΅ˆ-is-quotient-of-carrier : Ξ¨α΅’Κ³α΅ˆ (𝕍-set f , Οƒ) ＝ A/~β»α΅’Κ³α΅ˆ
   Ξ¨α΅’Κ³α΅ˆ-is-quotient-of-carrier =
    Ξ¦-is-left-cancellable (Ξ¨α΅’Κ³α΅ˆ (𝕍-set f , Οƒ)) A/~β»α΅’Κ³α΅ˆ e
     where
      e = Ξ¦ (Ξ¨α΅’Κ³α΅ˆ (𝕍-set f , Οƒ))          ＝⟨ ap pr₁ β¦…1⦆        ⟩
          𝕍-set f                         ＝⟨ 𝕍-set-ext _ _ β¦…2⦆ ⟩
          𝕍-set (Ξ» a' β†’ Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ a')) ＝⟨ β¦…3⦆               ⟩
          Ξ¦ A/~β»α΅’Κ³α΅ˆ                       ∎
       where
        β¦…1⦆ : Ξ¦α΅’Κ³α΅ˆ (Ξ¨α΅’Κ³α΅ˆ (𝕍-set f , Οƒ)) ＝ 𝕍-set f , Οƒ
        β¦…1⦆ = Ξ¨α΅’Κ³α΅ˆ-is-section-of-Ξ¦α΅’Κ³α΅ˆ (𝕍-set f , Οƒ)
        β¦…2⦆ : f β‰ˆ (Ξ» a' β†’ Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ a'))
        β¦…2⦆ = β¦…2⦆ˑ , β¦…2⦆ʳ
         where
          β¦…2⦆ˑ : f ≲ (Ξ» a' β†’ Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ a'))
          β¦…2⦆ˑ a =
           ∣ [ a ]⁻ , initial-segments-of-A/~β»α΅’Κ³α΅ˆ-are-given-by-f [ a ]⁻ a refl ∣
          β¦…2⦆ʳ : (Ξ» a' β†’ Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ a')) ≲ f
          β¦…2⦆ʳ a' = βˆ₯βˆ₯-functor h ([]⁻-is-surjection a')
           where
            h : (Ξ£ a κž‰ A , [ a ]⁻ ＝ a')
              β†’ (Ξ£ a κž‰ A , f a ＝ Ξ¦ (A/~β»α΅’Κ³α΅ˆ ↓ a'))
            h (a , refl) =
             a , ((initial-segments-of-A/~β»α΅’Κ³α΅ˆ-are-given-by-f a' a refl) ⁻¹)
        β¦…3⦆ = (Ξ¦-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 Ξ¨α΅’Κ³α΅ˆ 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 Ξ¨-construction sq

  Ξ¨α΅’Κ³α΅ˆ-is-isomorphic-to-total-space :
     (x : 𝕍) (Οƒ : is-set-theoretic-ordinal x)
   β†’ Ξ¨α΅’Κ³α΅ˆ (x , Οƒ) ≃ₒ total-spaceα΅’Κ³α΅ˆ x Οƒ
  Ξ¨α΅’Κ³α΅ˆ-is-isomorphic-to-total-space = 𝕍-prop-simple-induction _ prop-valued Ξ³
   where
    prop-valued : (x : 𝕍)
                β†’ is-prop ((Οƒ : is-set-theoretic-ordinal x) β†’ Ξ¨α΅’Κ³α΅ˆ (x , Οƒ)
                                                            ≃ₒ total-spaceα΅’Κ³α΅ˆ x Οƒ)
    prop-valued x = Ξ -is-prop fe (Ξ» Οƒ β†’ ≃ₒ-is-prop-valued _ _)
    Ξ³ : {A : 𝓀 Μ‡ } (f : A β†’ 𝕍) (Οƒ : is-set-theoretic-ordinal (𝕍-set f))
      β†’ Ξ¨α΅’Κ³α΅ˆ (𝕍-set f , Οƒ) ≃ₒ total-spaceα΅’Κ³α΅ˆ (𝕍-set f) Οƒ
    Ξ³ {A} f Οƒ = ≃ₒ-trans (Ξ¨α΅’Κ³α΅ˆ (𝕍-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⦆ : Ξ¨α΅’Κ³α΅ˆ (𝕍-set f , Οƒ) ≃ₒ A/~β»α΅’Κ³α΅ˆ
      β¦…1⦆ = idtoeqβ‚’ _ _ Ξ¨α΅’Κ³α΅ˆ-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}