Tom de Jong, 28 October 2022 - 7 November 2022.
In collaboration with Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu.

Following [Pow75], in constructive set theory an ordinal is [Def. 9.4.1, AR10],
defined as a transitive set of transitive sets.

We consider the subtype π•α΅’Κ³α΅ˆ of the cumulative hierarchy 𝕍 of set theoretic
ordinals in 𝕍 (see UF/CumulativeHierarchy.lagda and [Section 10.5, Uni13] for
more on 𝕍).

We show that (π•α΅’Κ³α΅ˆ,∈) is a ordinal, in the type theoretic sense of [Uni13],
i.e. it is a well-founded, extensional and transitive order. Moreover, we prove
that (π•α΅’Κ³α΅ˆ,∈) and the ordinal Ord of type theoretic ordinals are isomorphic.

This is interesting for at least two reasons:
(1) It shows that the set theoretic and type theoretic notions of ordinal
    coincide in HoTT.
(2) It shows that a nontrivial subtype of 𝕍, a complicated HIT, can be defined
    internally in univalent type theory without HITs (†) other than set
    quotients.

    (†): This was also done through other means by Gylterud [Gyl18] who gave a
         non-HIT construction of the cumulative hiearchy 𝕍.

After Fredrik Nordvall Forsberg's talk at the workshop in honour of Thorsten
Altenkirch's 60th birthday
(https://www.cs.nott.ac.uk/~psznk/events/thorsten60/#fred), Andreas Abel asked
how/whether we can relate set theoretic ordinals and type theoretic ordinals
through Aczel's [Acz78] type theoretic interpretation of set theory. Since the
cumulative hierarchy 𝕍 may be seen as an internal refinement of Aczel's
interpretation in HoTT, the theorem announced above provides an answer to
Andreas' question.

There are some directions for future work recorded at the end of this file.

References
----------

[Acz77] Peter Aczel
        An introduction to inductive definitions
        In Jon Barwise (ed.) Handbook of Mathematical Logic
        Volume 90 of Studies in Logic and the Foundations of Mathematics
        Pages 739─782
        North-Holland Publishing Company
        1977
        doi:10.1016/S0049-237X(08)71120-0

[Acz78] Peter Aczel
        The type theoretic interpretation of constructive set theory
        In A. MacIntyre, L. Pacholski, and J. Paris (eds.) Logic Colloquium ’77
        Volume 96 of Studies in Logic and the Foundations of Mathematics
        Pages 55–66
        North-Holland Publishing Company
        1978
        doi:10.1016/S0049-237X(08)71989-X

[AR10] Peter Aczel and Michael Rathjen
       Notes on Constructive Set Theory
       Book draft
       https://www1.maths.leeds.ac.uk/~rathjen/book.pdf
       2010

[Pow75] William C. Powell
        Extending GΓΆdel’s negative interpretation to ZF
        Volume 40, Issue 2 of Journal of Symbolic Logic
        Pages 221─229
        1975
        doi:10.2307/2271902

[Gyl18] HΓ₯kon Robbestad Gylterud
        From Multisets to Sets in Homotopy Type Theory
        Volue 83, Issue 3 of The Journal of Symbolic Logic
        Pages 1132─1146
        2018
        doi:10.1017/jsl.2017.84

[Uni13] The Univalent Foundations Program
        Homotopy Type Theory: Univalent Foundations of Mathematics
        https://homotopytypetheory.org/book
        Institute for Advanced Study
        2013

\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 Ordinals.CumulativeHierarchy
        (pt : propositional-truncations-exist)
        (ua : Univalence)
        (𝓀 : Universe)
       where

open PropositionalTruncation pt

open import UF.Base hiding (_β‰ˆ_)
open import UF.Equiv
open import UF.FunExt
open import UF.Subsingletons
open import UF.Subsingletons-FunExt
open import UF.UA-FunExt

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 Ordinals.Notions
open import Ordinals.OrdinalOfOrdinals ua
open import Ordinals.Type hiding (Ord)
open import Ordinals.Underlying

open import UF.CumulativeHierarchy pt fe pe

module ordinal-of-set-theoretic-ordinals
        (ch : cumulative-hierarchy-exists 𝓀)
       where

 open cumulative-hierarchy-exists ch

\end{code}

We start by defining a set theoretic ordinal to be a transitive set whose
elements are again transitive sets, as announced above.

\begin{code}

 is-transitive-set : 𝕍 β†’ 𝓀 ⁺ Μ‡
 is-transitive-set x = (u : 𝕍) (v : 𝕍) β†’ u ∈ x β†’ v ∈ u β†’ v ∈ x

 being-transitive-set-is-prop : {x : 𝕍} β†’ is-prop (is-transitive-set x)
 being-transitive-set-is-prop = Ξ β‚„-is-prop fe (Ξ» _ _ _ _ β†’ ∈-is-prop-valued)

 is-set-theoretic-ordinal : 𝕍 β†’ 𝓀 ⁺ Μ‡
 is-set-theoretic-ordinal x = is-transitive-set x
                            Γ— ((y : 𝕍) β†’ y ∈ x β†’ is-transitive-set y)

 being-set-theoretic-ordinal-is-prop : {x : 𝕍} β†’ is-prop (is-set-theoretic-ordinal x)
 being-set-theoretic-ordinal-is-prop =
  Γ—-is-prop being-transitive-set-is-prop
            (Ξ β‚‚-is-prop fe (Ξ» _ _ β†’ being-transitive-set-is-prop))

 transitive-set-if-set-theoretic-ordinal : {x : 𝕍}
                                         β†’ is-set-theoretic-ordinal x
                                         β†’ is-transitive-set x
 transitive-set-if-set-theoretic-ordinal = pr₁

 transitive-set-if-element-of-set-theoretic-ordinal : {x : 𝕍}
                                                    β†’ is-set-theoretic-ordinal x
                                                    β†’ {y : 𝕍} β†’ y ∈ x
                                                    β†’ is-transitive-set y
 transitive-set-if-element-of-set-theoretic-ordinal Οƒ {y} m = prβ‚‚ Οƒ y m

 being-set-theoretic-ordinal-is-hereditary : {x : 𝕍} β†’ is-set-theoretic-ordinal x
                                           β†’ {y : 𝕍}
                                           β†’ y ∈ x β†’ is-set-theoretic-ordinal y
 being-set-theoretic-ordinal-is-hereditary {x} (t , Ο„) {y} m =
  Ο„ y m , (Ξ» z n β†’ Ο„ z (t y z m n))

\end{code}

Restricting our attention to those elements of 𝕍 that are set theoretic
ordinals, we show that the membership relation ∈ makes this subtype into a type
theoretic ordinal.

\begin{code}

 π•α΅’Κ³α΅ˆ : 𝓀 ⁺ Μ‡
 π•α΅’Κ³α΅ˆ = Ξ£ x κž‰ 𝕍 , is-set-theoretic-ordinal x

 π•α΅’Κ³α΅ˆ-is-subtype : {x y : π•α΅’Κ³α΅ˆ} β†’ pr₁ x = pr₁ y β†’ x = y
 π•α΅’Κ³α΅ˆ-is-subtype = to-subtype-= (Ξ» _ β†’ being-set-theoretic-ordinal-is-prop)

 _βˆˆα΅’Κ³α΅ˆ_ : π•α΅’Κ³α΅ˆ β†’ π•α΅’Κ³α΅ˆ β†’ 𝓀 ⁺  Μ‡
 _βˆˆα΅’Κ³α΅ˆ_ (x , _) (y , _) = x ∈ y

 βˆˆα΅’Κ³α΅ˆ-is-extensional : is-extensional _βˆˆα΅’Κ³α΅ˆ_
 βˆˆα΅’Κ³α΅ˆ-is-extensional (x , u) (y , v) s t =
  π•α΅’Κ³α΅ˆ-is-subtype
   (∈-extensionality
     x y
     (Ξ» z m β†’ s (z , being-set-theoretic-ordinal-is-hereditary u m) m)
     (Ξ» z m β†’ t (z , being-set-theoretic-ordinal-is-hereditary v m) m))

 βˆˆα΅’Κ³α΅ˆ-is-transitive : is-transitive _βˆˆα΅’Κ³α΅ˆ_
 βˆˆα΅’Κ³α΅ˆ-is-transitive (x , _) (y , _) (z , Ο„) x-in-y y-in-z =
  transitive-set-if-set-theoretic-ordinal Ο„ y x y-in-z x-in-y

 ∈-is-well-founded : is-well-founded _∈_
 ∈-is-well-founded = ∈-induction (is-accessible _∈_)
                                 (Ξ» x β†’ accessibility-is-prop _∈_ fe' x)
                                 (Ξ» x IH β†’ step IH)

 βˆˆα΅’Κ³α΅ˆ-is-well-founded : is-well-founded _βˆˆα΅’Κ³α΅ˆ_
 βˆˆα΅’Κ³α΅ˆ-is-well-founded = transfinite-induction-converse _βˆˆα΅’Κ³α΅ˆ_ W
  where
   W : Well-founded _βˆˆα΅’Κ³α΅ˆ_
   W P IH = (Ξ» (x , Οƒ) β†’ Q-holds-everywhere x Οƒ)
    where
     Q : 𝕍 β†’ 𝓀 ⁺ Μ‡
     Q x = (Οƒ : is-set-theoretic-ordinal x) β†’ P (x , Οƒ)
     Q-holds-everywhere : (x : 𝕍) β†’ Q x
     Q-holds-everywhere = transfinite-induction _∈_ ∈-is-well-founded Q f
      where
       f : (x : 𝕍) β†’ ((y : 𝕍) β†’ y ∈ x β†’ Q y) β†’ Q x
       f x IH' Οƒ = IH (x , Οƒ) g
        where
         g : (y : π•α΅’Κ³α΅ˆ) β†’ y βˆˆα΅’Κ³α΅ˆ (x , Οƒ) β†’ P y
         g (y , Ο„) y-in-x = IH' y y-in-x Ο„

 𝕍ᴼᴿᴰ : Ordinal (𝓀 ⁺)
 𝕍ᴼᴿᴰ = π•α΅’Κ³α΅ˆ , _βˆˆα΅’Κ³α΅ˆ_
             , (Ξ» x y β†’ ∈-is-prop-valued)
             , βˆˆα΅’Κ³α΅ˆ-is-well-founded
             , βˆˆα΅’Κ³α΅ˆ-is-extensional
             , βˆˆα΅’Κ³α΅ˆ-is-transitive

\end{code}

We now work towards proving that 𝕍ᴼᴿᴰ and Ord, the ordinal of type theoretic
ordinals, are isomorphic (as type theoretic ordinals).

We start by defining a map Ord β†’ 𝕍 by transfinite recursion on Ord.

\begin{code}

 private
  Ord : 𝓀 ⁺ Μ‡
  Ord = Ordinal 𝓀

 Ord-to-𝕍 : Ord β†’ 𝕍
 Ord-to-𝕍 = transfinite-recursion-on-OO 𝕍 (Ξ» Ξ± f β†’ 𝕍-set f)

 Ord-to-𝕍-behaviour : (Ξ± : Ord) β†’ Ord-to-𝕍 Ξ± = 𝕍-set (Ξ» a β†’ Ord-to-𝕍 (Ξ± ↓ a))
 Ord-to-𝕍-behaviour = transfinite-recursion-on-OO-behaviour 𝕍 (Ξ» a f β†’ 𝕍-set f)

 ∈-of-Ord-to-𝕍 : (Ξ± : Ord) (x : 𝕍)
                β†’ x ∈ Ord-to-𝕍 Ξ± = (βˆƒ a κž‰ ⟨ Ξ± ⟩ , Ord-to-𝕍 (Ξ± ↓ a) = x)
 ∈-of-Ord-to-𝕍 Ξ± x =
  x ∈ Ord-to-𝕍 Ξ±                        =⟨ ap (x ∈_) (Ord-to-𝕍-behaviour Ξ±) ⟩
  x ∈ 𝕍-set (Ξ» a β†’ Ord-to-𝕍 (Ξ± ↓ a))    =⟨ ∈-for-𝕍-sets x _ ⟩
  (βˆƒ a κž‰ ⟨ Ξ± ⟩ , Ord-to-𝕍 (Ξ± ↓ a) = x) ∎

 to-∈-of-Ord-to-𝕍 : (Ξ± : Ord) {x : 𝕍}
                  β†’ (βˆƒ a κž‰ ⟨ Ξ± ⟩ , Ord-to-𝕍 (Ξ± ↓ a) = x) β†’ x ∈ Ord-to-𝕍 Ξ±
 to-∈-of-Ord-to-𝕍 Ξ± {x} = back-Idtofun (∈-of-Ord-to-𝕍 Ξ± x)

 from-∈-of-Ord-to-𝕍 : (Ξ± : Ord) {x : 𝕍}
                    β†’ x ∈ Ord-to-𝕍 Ξ± β†’ (βˆƒ a κž‰ ⟨ Ξ± ⟩ , Ord-to-𝕍 (Ξ± ↓ a) = x)
 from-∈-of-Ord-to-𝕍 Ξ± {x} = Idtofun (∈-of-Ord-to-𝕍 Ξ± x)

\end{code}

The map Ord β†’ 𝕍 preserves the strict and weak order.

\begin{code}

 Ord-to-𝕍-preserves-strict-order : (Ξ± Ξ² : Ord) β†’ Ξ± ⊲ Ξ² β†’ Ord-to-𝕍 Ξ± ∈ Ord-to-𝕍 Ξ²
 Ord-to-𝕍-preserves-strict-order Ξ± Ξ² (b , refl) = to-∈-of-Ord-to-𝕍 Ξ² ∣ b , refl ∣

 Ord-to-𝕍-preserves-weak-order : (Ξ± Ξ² : Ord) β†’ Ξ± ⊴ Ξ² β†’ Ord-to-𝕍 Ξ± βŠ† Ord-to-𝕍 Ξ²
 Ord-to-𝕍-preserves-weak-order Ξ± Ξ² l x m = to-∈-of-Ord-to-𝕍 Ξ² m'
  where
   l' : (a : ⟨ Ξ± ⟩) β†’ Ξ£ b κž‰ ⟨ Ξ² ⟩ , Ξ± ↓ a = Ξ² ↓ b
   l' = from-β‰Ό (⊴-gives-β‰Ό Ξ± Ξ² l)
   m' : βˆƒ b κž‰ ⟨ Ξ² ⟩ , Ord-to-𝕍 (Ξ² ↓ b) = x
   m' = βˆ₯βˆ₯-functor h (from-∈-of-Ord-to-𝕍 Ξ± m)
    where
     h : (Ξ£ a κž‰ ⟨ Ξ± ⟩ , Ord-to-𝕍 (Ξ± ↓ a) = x)
       β†’ (Ξ£ b κž‰ ⟨ Ξ² ⟩ , Ord-to-𝕍 (Ξ² ↓ b) = x)
     h (a , refl) = (b , ap Ord-to-𝕍 (e ⁻¹))
      where
       b : ⟨ β ⟩
       b = pr₁ (l' a)
       e : Ξ± ↓ a = Ξ² ↓ b
       e = prβ‚‚ (l' a)

\end{code}

An argument by transfinite induction shows that the map Ord-to-𝕍 is left
cancellable, which yields a quick proof that Ord-to-𝕍 not only preserves the
strict order, but also reflects it. It follows that Ord-to-𝕍 also reflects the
weak order.

\begin{code}

 Ord-to-𝕍-is-left-cancellable : (Ξ± Ξ² : Ord) β†’ Ord-to-𝕍 Ξ± = Ord-to-𝕍 Ξ² β†’ Ξ± = Ξ²
 Ord-to-𝕍-is-left-cancellable = transfinite-induction-on-OO _ f
  where
   f : (Ξ± : Ord)
     β†’ ((a : ⟨ Ξ± ⟩) (Ξ² : Ord) β†’ Ord-to-𝕍 (Ξ± ↓ a) = Ord-to-𝕍 Ξ² β†’ (Ξ± ↓ a) = Ξ²)
     β†’ (Ξ² : Ord) β†’ Ord-to-𝕍 Ξ± = Ord-to-𝕍 Ξ² β†’ Ξ± = Ξ²
   f Ξ± IH Ξ² e = ⊴-antisym Ξ± Ξ² (to-⊴ Ξ± Ξ² g₁) (to-⊴ Ξ² Ξ± gβ‚‚)
    where
     g₁ : (a : ⟨ Ξ± ⟩) β†’ (Ξ± ↓ a) ⊲ Ξ²
     g₁ a = βˆ₯βˆ₯-rec (⊲-is-prop-valued (Ξ± ↓ a) Ξ²) h (from-∈-of-Ord-to-𝕍 Ξ² m)
      where
       h : (Ξ£ b κž‰ ⟨ Ξ² ⟩ , Ord-to-𝕍 (Ξ² ↓ b) = Ord-to-𝕍 (Ξ± ↓ a)) β†’ (Ξ± ↓ a) ⊲ Ξ²
       h (b , e) = (b , (IH a (Ξ² ↓ b) (e ⁻¹)))
       m : Ord-to-𝕍 (Ξ± ↓ a) ∈ Ord-to-𝕍 Ξ²
       m = transport (Ord-to-𝕍 (Ξ± ↓ a) ∈_) e
                     (to-∈-of-Ord-to-𝕍 Ξ± ∣ a , refl ∣)
     gβ‚‚ : (b : ⟨ Ξ² ⟩) β†’ (Ξ² ↓ b) ⊲ Ξ±
     gβ‚‚ b = βˆ₯βˆ₯-rec (⊲-is-prop-valued (Ξ² ↓ b) Ξ±) h (from-∈-of-Ord-to-𝕍 Ξ± m)
      where
       h : (Ξ£ a κž‰ ⟨ Ξ± ⟩ , Ord-to-𝕍 (Ξ± ↓ a) = Ord-to-𝕍 (Ξ² ↓ b)) β†’ (Ξ² ↓ b) ⊲ Ξ±
       h (a , e) = (a , ((IH a (Ξ² ↓ b) e) ⁻¹))
       m : Ord-to-𝕍 (Ξ² ↓ b) ∈ Ord-to-𝕍 Ξ±
       m = transport (Ord-to-𝕍 (Ξ² ↓ b) ∈_) (e ⁻¹)
                     (to-∈-of-Ord-to-𝕍 Ξ² ∣ b , refl ∣)

 Ord-to-𝕍-reflects-strict-order : (Ξ± Ξ² : Ord) β†’ Ord-to-𝕍 Ξ± ∈ Ord-to-𝕍 Ξ² β†’ Ξ± ⊲ Ξ²
 Ord-to-𝕍-reflects-strict-order Ξ± Ξ² m = βˆ₯βˆ₯-rec (⊲-is-prop-valued Ξ± Ξ²) h m'
  where
   h : (Ξ£ b κž‰ ⟨ Ξ² ⟩ , Ord-to-𝕍 (Ξ² ↓ b) = Ord-to-𝕍 Ξ±) β†’ Ξ± ⊲ Ξ²
   h (b , e) = (b , ((Ord-to-𝕍-is-left-cancellable (Ξ² ↓ b) Ξ± e) ⁻¹))
   m' : βˆƒ b κž‰ ⟨ Ξ² ⟩ , Ord-to-𝕍 (Ξ² ↓ b) = Ord-to-𝕍 Ξ±
   m' = from-∈-of-Ord-to-𝕍 Ξ² m

 Ord-to-𝕍-reflects-weak-order : (Ξ± Ξ² : Ord) β†’ Ord-to-𝕍 Ξ± βŠ† Ord-to-𝕍 Ξ² β†’ Ξ± ⊴ Ξ²
 Ord-to-𝕍-reflects-weak-order Ξ± Ξ² s = to-⊴ Ξ± Ξ² h
  where
   h : (a : ⟨ Ξ± ⟩) β†’ (Ξ± ↓ a) ⊲ Ξ²
   h a = Ord-to-𝕍-reflects-strict-order (Ξ± ↓ a) Ξ² m
    where
     m : Ord-to-𝕍 (Ξ± ↓ a) ∈ Ord-to-𝕍 Ξ²
     m = s (Ord-to-𝕍 (Ξ± ↓ a)) (to-∈-of-Ord-to-𝕍 Ξ± ∣ a , refl ∣)

\end{code}

The map Ord β†’ 𝕍 constructed above actually factors through the subtype π•α΅’Κ³α΅ˆ.

(The proof is quite straightforward, but the formal proof is slightly long,
because we need to use from-∈-of-Ord-to-𝕍 and to-∈-of-Ord-to-𝕍 as we don't have
judgemental computation rules for 𝕍.)

\begin{code}

 Ord-to-π•α΅’Κ³α΅ˆ : Ord β†’ π•α΅’Κ³α΅ˆ
 Ord-to-π•α΅’Κ³α΅ˆ Ξ± = (Ord-to-𝕍 Ξ± , ρ Ξ±)
  where
   Ο„ : (Ξ² : Ord) β†’ is-transitive-set (Ord-to-𝕍 Ξ²)
   Ο„ Ξ² x y x-in-Ξ² y-in-x = to-∈-of-Ord-to-𝕍 Ξ² (βˆ₯βˆ₯-rec βˆƒ-is-prop lemma x-in-Ξ²')
    where
     x-in-Ξ²' : βˆƒ b κž‰ ⟨ Ξ² ⟩ , Ord-to-𝕍 (Ξ² ↓ b) = x
     x-in-Ξ²' = from-∈-of-Ord-to-𝕍 Ξ² x-in-Ξ²
     lemma : (Ξ£ b κž‰ ⟨ Ξ² ⟩ , Ord-to-𝕍 (Ξ² ↓ b) = x)
           β†’ βˆƒ c κž‰ ⟨ Ξ² ⟩ , Ord-to-𝕍 (Ξ² ↓ c) = y
     lemma (b , refl) = βˆ₯βˆ₯-functor h y-in-β↓b
      where
       h : (Ξ£ c κž‰ ⟨ Ξ² ↓ b ⟩ , Ord-to-𝕍 ((Ξ² ↓ b) ↓ c) = y)
         β†’ Ξ£ d κž‰ ⟨ Ξ² ⟩ , Ord-to-𝕍 (Ξ² ↓ d) = y
       h ((c , l) , refl) = (c , ap Ord-to-𝕍 ((iterated-↓ Ξ² b c l) ⁻¹))
       y-in-β↓b : βˆƒ c κž‰ ⟨ Ξ² ↓ b ⟩ , Ord-to-𝕍 ((Ξ² ↓ b) ↓ c) = y
       y-in-β↓b = from-∈-of-Ord-to-𝕍 (Ξ² ↓ b) y-in-x

   ρ : (Ξ² : Ord) β†’ is-set-theoretic-ordinal (Ord-to-𝕍 Ξ²)
   ρ = transfinite-induction-on-OO
        (Ξ» - β†’ is-set-theoretic-ordinal (Ord-to-𝕍 -))
        ρ'
    where
     ρ' : (β : Ord)
        β†’ ((b : ⟨ Ξ² ⟩) β†’ is-set-theoretic-ordinal (Ord-to-𝕍 (Ξ² ↓ b)))
        β†’ is-set-theoretic-ordinal (Ord-to-𝕍 Ξ²)
     ρ' Ξ² IH = (Ο„ Ξ² , Ο„')
      where
       Ο„' : (y : 𝕍) β†’ y ∈ Ord-to-𝕍 Ξ² β†’ is-transitive-set y
       Ο„' y m = βˆ₯βˆ₯-rec being-transitive-set-is-prop h (from-∈-of-Ord-to-𝕍 Ξ² m)
        where
         h : (Ξ£ b κž‰ ⟨ Ξ² ⟩ , Ord-to-𝕍 (Ξ² ↓ b) = y) β†’ is-transitive-set y
         h (b , refl) = Ο„ (Ξ² ↓ b)

 Ord-to-π•α΅’Κ³α΅ˆ-is-left-cancellable : {Ξ± Ξ² : Ord}
                                 β†’ Ord-to-π•α΅’Κ³α΅ˆ Ξ± = Ord-to-π•α΅’Κ³α΅ˆ Ξ² β†’ Ξ± = Ξ²
 Ord-to-π•α΅’Κ³α΅ˆ-is-left-cancellable {Ξ±} {Ξ²} e =
  Ord-to-𝕍-is-left-cancellable Ξ± Ξ² (ap pr₁ e)

\end{code}

To show that Ord-to-π•α΅’Κ³α΅ˆ is an isomorphism of ordinals it now suffices to prove
that it is split surjective.

We construct a map 𝕍 β†’ Ord by recursion on 𝕍 by sending 𝕍-set {A} f to the
supremum of ordinals ⋁ (ψ (f a) + πŸ™) indexed by a : A.

This is a familiar construction in set theory, see e.g. [Def. 9.3.4, AR10],
where the ordinal above is the "rank" of the set. This map (but with the domain
an arbitrary well founded order) also appears at the bottom of [Acz77, p. 743].

\begin{code}

 open import Ordinals.Arithmetic fe'
 open import Ordinals.Arithmetic-Properties ua hiding (lemma₁ ; lemmaβ‚‚)
 open import Ordinals.OrdinalOfOrdinalsSuprema ua

 open import UF.Quotient hiding (is-prop-valued)

 module 𝕍-to-Ord-construction
         (sq : set-quotients-exist)
        where

  open suprema pt (set-replacement-from-set-quotients sq pt)

  private
   𝕍-to-Ord-aux : {A : 𝓀 Μ‡ } β†’ (A β†’ 𝕍) β†’ (A β†’ Ord) β†’ Ord
   𝕍-to-Ord-aux _ r = sup (Ξ» a β†’ r a +β‚’ πŸ™β‚’)

   𝕍-to-Ord-packaged : Ξ£ Ο• κž‰ (𝕍 β†’ Ord) , ({A : 𝓀 Μ‡} (f : A β†’ 𝕍)
                                          (r : A β†’ Ordinal 𝓀)
                                       β†’ Ο• (𝕍-set f) = 𝕍-to-Ord-aux f r)
   𝕍-to-Ord-packaged =
    𝕍-recursion-with-computation the-type-of-ordinals-is-a-set ρ Ο„
    where
     ρ = 𝕍-to-Ord-aux
     monotone-lemma : {A B : 𝓀 Μ‡} (f : A β†’ 𝕍) (g : B β†’ 𝕍)
                    β†’ (r₁ : A β†’ Ord) (rβ‚‚ : B β†’ Ord)
                    β†’ ((a : A) β†’ βˆ₯ Ξ£ b κž‰ B , Ξ£ p κž‰ f a = g b , r₁ a = rβ‚‚ b βˆ₯)
                    β†’ ρ f r₁ ⊴ ρ g rβ‚‚
     monotone-lemma {A} {B} f g r₁ rβ‚‚ e =
      sup-is-lower-bound-of-upper-bounds (Ξ» a β†’ r₁ a +β‚’ πŸ™β‚’) (ρ g rβ‚‚) Ο•
       where
        Ο• : (a : A) β†’ (r₁ a +β‚’ πŸ™β‚’) ⊴ ρ g rβ‚‚
        Ο• a = βˆ₯βˆ₯-rec (⊴-is-prop-valued _ _) ψ (e a)
         where
          ψ : (Ξ£ b κž‰ B , Ξ£ p κž‰ f a = g b , r₁ a = rβ‚‚ b)
            β†’ (r₁ a +β‚’ πŸ™β‚’) ⊴ ρ g rβ‚‚
          ψ (b , _ , q) = ⊴-trans _ (rβ‚‚ b +β‚’ πŸ™β‚’) _ k l
           where
            k : (r₁ a +β‚’ πŸ™β‚’) ⊴ (rβ‚‚ b +β‚’ πŸ™β‚’)
            k = ≃ₒ-to-⊴ _ _ (idtoeqβ‚’ _ _ (ap (_+β‚’ πŸ™β‚’) q))
            l : (rβ‚‚ b +β‚’ πŸ™β‚’) ⊴ ρ g rβ‚‚
            l = sup-is-upper-bound _ b
     Ο„ : {A B : 𝓀 Μ‡} (f : A β†’ 𝕍) (g : B β†’ 𝕍)
       β†’ (r₁ : A β†’ Ord) (rβ‚‚ : B β†’ Ord)
       β†’ ((a : A) β†’ βˆ₯ Ξ£ b κž‰ B , Ξ£ p κž‰ f a = g b , r₁ a = rβ‚‚ b βˆ₯)
       β†’ ((b : B) β†’ βˆ₯ Ξ£ a κž‰ A , Ξ£ p κž‰ g b = f a , rβ‚‚ b = r₁ a βˆ₯)
       β†’ f β‰ˆ g
       β†’ ρ f r₁ = ρ g rβ‚‚
     Ο„ {A} {B} f g r₁ rβ‚‚ e₁ eβ‚‚ _ =
      ⊴-antisym (ρ f r₁) (ρ g rβ‚‚)
                (monotone-lemma f g r₁ rβ‚‚ e₁)
                (monotone-lemma g f rβ‚‚ r₁ eβ‚‚)

  𝕍-to-Ord : 𝕍 β†’ Ord
  𝕍-to-Ord = pr₁ (𝕍-to-Ord-packaged)

\end{code}

The below records the behaviour on 𝕍-sets that we announced above.

\begin{code}

  𝕍-to-Ord-behaviour-on-𝕍-sets :
     {A : 𝓀 Μ‡ } (f : A β†’ 𝕍)
   β†’ 𝕍-to-Ord (𝕍-set f) = sup (Ξ» a β†’ 𝕍-to-Ord (f a) +β‚’ πŸ™β‚’)
  𝕍-to-Ord-behaviour-on-𝕍-sets f = prβ‚‚ 𝕍-to-Ord-packaged f (Ξ» a β†’ 𝕍-to-Ord (f a))

  π•α΅’Κ³α΅ˆ-to-Ord : π•α΅’Κ³α΅ˆ β†’ Ord
  π•α΅’Κ³α΅ˆ-to-Ord = 𝕍-to-Ord ∘ pr₁

\end{code}

We show that Ord-to-𝕍 is a split surjection by showing that π•α΅’Κ³α΅ˆ-to-Ord is a
section of it. The fact that we are restricting the inputs to set theoretic
ordinals is crucial in proving one of the inequalities.

\begin{code}

  𝕍-to-Ord-is-section-of-Ord-to-𝕍 : (x : 𝕍)
                                  β†’ is-set-theoretic-ordinal x
                                  β†’ Ord-to-𝕍 (𝕍-to-Ord x) = x
  𝕍-to-Ord-is-section-of-Ord-to-𝕍 =
   𝕍-prop-induction _ (Ξ» x β†’ Ξ -is-prop fe (Ξ» _ β†’ 𝕍-is-large-set)) ρ
    where
     ρ : {A : 𝓀 Μ‡} (f : A β†’ 𝕍)
       β†’ ((a : A) β†’ is-set-theoretic-ordinal (f a)
                  β†’ Ord-to-𝕍 (𝕍-to-Ord (f a)) = f a)
       β†’ is-set-theoretic-ordinal (𝕍-set f)
       β†’ Ord-to-𝕍 (𝕍-to-Ord (𝕍-set f)) = 𝕍-set f
     ρ {A} f IH Οƒ =
      Ord-to-𝕍 (𝕍-to-Ord (𝕍-set f))  =⟨ β¦…1⦆ ⟩
      Ord-to-𝕍 s                     =⟨ β¦…2⦆ ⟩
      𝕍-set (Ξ» y β†’ Ord-to-𝕍 (s ↓ y)) =⟨ β¦…3⦆ ⟩
      𝕍-set f                        ∎
       where
        s : Ord
        s = sup (Ξ» a β†’ 𝕍-to-Ord (f a) +β‚’ πŸ™β‚’)
        β¦…1⦆ = ap Ord-to-𝕍 (𝕍-to-Ord-behaviour-on-𝕍-sets f)
        β¦…2⦆ = Ord-to-𝕍-behaviour s
        β¦…3⦆ = 𝕍-set-ext _ _ (e₁ , eβ‚‚)
          {- The proof of eβ‚‚ and especially e₁ are the only hard parts. We set
             up two lemmas and some abbreviations to get e₁ and eβ‚‚. -}
         where
          c : (a : A) β†’ Ord
          c a = 𝕍-to-Ord (f a) +β‚’ πŸ™β‚’
          abstract -- For performance
           u : (a : A) β†’ ⟨ c a ⟩  β†’ ⟨ s ⟩
           u a = pr₁ (sup-is-upper-bound _ a)

           IH' : (a : A) β†’ Ord-to-𝕍 (𝕍-to-Ord (f a)) = f a
           IH' a = IH a (being-set-theoretic-ordinal-is-hereditary Οƒ
                          (to-∈-of-𝕍-set ∣ a , refl ∣))

           lemma₁ : (a : A) β†’ Ord-to-𝕍 (c a ↓ inr ⋆) = f a
           lemma₁ a = Ord-to-𝕍 (c a ↓ inr ⋆)     =⟨ ap Ord-to-𝕍 β¦…e⦆ ⟩
                      Ord-to-𝕍 (𝕍-to-Ord (f a)) =⟨ IH' a            ⟩
                      f a ∎
            where
             β¦…e⦆ : c a ↓ inr ⋆ = 𝕍-to-Ord (f a)
             β¦…e⦆ = +β‚’-πŸ™β‚’-↓-right (𝕍-to-Ord (f a))

           lemmaβ‚‚ : (a : A) β†’ Ord-to-𝕍 (s ↓ u a (inr ⋆)) = f a
           lemmaβ‚‚ a = Ord-to-𝕍 (s ↓ u a (inr ⋆)) =⟨ ap Ord-to-𝕍 β¦…e⦆ ⟩
                      Ord-to-𝕍 (c a ↓ inr ⋆)     =⟨ lemma₁ a ⟩
                      f a                        ∎
            where
             β¦…e⦆ : s ↓ u a (inr ⋆) = c a ↓ inr ⋆
             β¦…e⦆ = initial-segment-of-sup-at-component _ a (inr ⋆)

          eβ‚‚ : f ≲ (Ξ» y β†’ Ord-to-𝕍 (s ↓ y))
          eβ‚‚ a = ∣ u a (inr ⋆) , lemmaβ‚‚ a ∣

          e₁ : (Ξ» y β†’ Ord-to-𝕍 (s ↓ y)) ≲ f
          e₁ y =
           βˆ₯βˆ₯-rec βˆƒ-is-prop h
            (initial-segment-of-sup-is-initial-segment-of-some-component _ y)
            where
             h : (Ξ£ a κž‰ A , Ξ£ x κž‰ ⟨ c a ⟩ , s ↓ y = c a ↓ x)
               β†’ βˆƒ a κž‰ A , f a = Ord-to-𝕍 (s ↓ y)
             h (a , inr ⋆ , e) = ∣ a , (e' ⁻¹) ∣
              where
               e' = Ord-to-𝕍 (s ↓ y)       =⟨ ap Ord-to-𝕍 e ⟩
                    Ord-to-𝕍 (c a ↓ inr ⋆) =⟨ lemma₁ a ⟩
                    f a                    ∎
             h (a , inl x , e) = goal
              where
               ∈-claim₁ : Ord-to-𝕍 (𝕍-to-Ord (f a) ↓ x) ∈ f a
               ∈-claim₁ = transport (Ord-to-𝕍 (𝕍-to-Ord (f a) ↓ x) ∈_)
                                    (IH' a)
                                    (Ord-to-𝕍-preserves-strict-order
                                      (𝕍-to-Ord (f a) ↓ x)
                                      (𝕍-to-Ord (f a))
                                      (x , refl))
               ∈-claimβ‚‚ : Ord-to-𝕍 (𝕍-to-Ord (f a) ↓ x) ∈ 𝕍-set f
               ∈-claimβ‚‚ = transitive-set-if-set-theoretic-ordinal Οƒ
                            (f a)
                            (Ord-to-𝕍 (𝕍-to-Ord (f a) ↓ x))
                            (to-∈-of-𝕍-set ∣ a , refl ∣)
                            ∈-claim₁

               goal : βˆƒ a' κž‰ A , f a' = Ord-to-𝕍 (s ↓ y)
               goal = βˆ₯βˆ₯-functor g (from-∈-of-𝕍-set ∈-claimβ‚‚)
                where
                 g : (Ξ£ a' κž‰ A , f a' = Ord-to-𝕍 (𝕍-to-Ord (f a) ↓ x))
                   β†’ Ξ£ a' κž‰ A , f a' = Ord-to-𝕍 (s ↓ y)
                 g (a' , p) = (a' , q)
                  where
                   q = f a'                          =⟨ p  ⟩
                       Ord-to-𝕍 (𝕍-to-Ord (f a) ↓ x) =⟨ e' ⟩
                       Ord-to-𝕍 (s ↓ y)              ∎
                    where
                     ↓-fact : c a ↓ inl x = 𝕍-to-Ord (f a) ↓ x
                     ↓-fact = +β‚’-↓-left x ⁻¹
                     e' = ap Ord-to-𝕍 (↓-fact ⁻¹ βˆ™ e ⁻¹)


  π•α΅’Κ³α΅ˆ-to-Ord-is-section-of-Ord-to-π•α΅’Κ³α΅ˆ : Ord-to-π•α΅’Κ³α΅ˆ ∘ π•α΅’Κ³α΅ˆ-to-Ord ∼ id
  π•α΅’Κ³α΅ˆ-to-Ord-is-section-of-Ord-to-π•α΅’Κ³α΅ˆ (x , Οƒ) =
   π•α΅’Κ³α΅ˆ-is-subtype (𝕍-to-Ord-is-section-of-Ord-to-𝕍 x Οƒ)

\end{code}

Finally we obtain the result that ordinal of type theoretic ordinals is
isomorphic to the (type theoretic) ordinal 𝕍ᴼᴿᴰ of set theoretic ordinals.

\begin{code}

  π•α΅’Κ³α΅ˆ-isomorphic-to-Ord : OO 𝓀 ≃ₒ 𝕍ᴼᴿᴰ
  π•α΅’Κ³α΅ˆ-isomorphic-to-Ord =
   Ord-to-π•α΅’Κ³α΅ˆ , order-preserving-reflecting-equivs-are-order-equivs
                  (OO 𝓀) 𝕍ᴼᴿᴰ Ord-to-π•α΅’Κ³α΅ˆ
                  Ord-to-π•α΅’Κ³α΅ˆ-is-equiv
                  Ord-to-𝕍-preserves-strict-order
                  Ord-to-𝕍-reflects-strict-order
    where
     Ord-to-π•α΅’Κ³α΅ˆ-is-split-surjective : (x : π•α΅’Κ³α΅ˆ)
                                     β†’ Ξ£ Ξ± κž‰ Ord , Ord-to-π•α΅’Κ³α΅ˆ Ξ± = x
     Ord-to-π•α΅’Κ³α΅ˆ-is-split-surjective x = π•α΅’Κ³α΅ˆ-to-Ord x
                                       , π•α΅’Κ³α΅ˆ-to-Ord-is-section-of-Ord-to-π•α΅’Κ³α΅ˆ x

     Ord-to-π•α΅’Κ³α΅ˆ-is-equiv : is-equiv (Ord-to-π•α΅’Κ³α΅ˆ)
     Ord-to-π•α΅’Κ³α΅ˆ-is-equiv = lc-split-surjections-are-equivs
                             Ord-to-π•α΅’Κ³α΅ˆ
                             Ord-to-π•α΅’Κ³α΅ˆ-is-left-cancellable
                             Ord-to-π•α΅’Κ³α΅ˆ-is-split-surjective


\end{code}

Further work
------------

(1) 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. It is possible to give a more direct presentation of
  𝕍-to-Ord (𝕍-set {A} f)
however, that is nonrecursive.

Namely, we can show that 𝕍-to-Ord (𝕍-set {A} f) = (A/~ , <), where ~ identifies
elements of A that have the same image under f and [a] < [a'] is defined to hold
when f a ∈ f a'.

It is straightforward to see that (A/~ , <) is in fact equivalent (but not equal
for size reasons) to the image of f, which in turn is equivalent to the total
space (Ξ£ y κž‰ 𝕍 , y ∈ 𝕍-set f), so that the map 𝕍-to-Ord can be described (up to
equivalence) as x ↦ Ξ£ y κž‰ 𝕍 , y ∈ x.

These observations are fully formalised in the file
Ordinals/CumulativeHierarchy-Addendum.lagda.

(2) On a separate note, we are currently working out the details of a related
presentation for all of 𝕍.