Tom de Jong, 29 November 2022.
In collaboration with Nicolai Kraus, Fredrik Nordvall Forsberg and Chuangjie Xu.

Cleaned up on 16 and 19 December 2022.

The cumulative hierarchy 𝕍 with respect to a universe 𝓀 is a large type, meaning
it lives in the next universe 𝓀 ⁺. Hence, for elements x, y : 𝕍, the identity type
x ＝ y of 𝕍 also lives in 𝓀 ⁺. However, as pointed out in the HoTT Book
[Section 10.5, 1], it is possible to define a binary relation on 𝕍 that takes
values in 𝓀 and prove it equivalent to the identity type of 𝕍. This makes 𝕍 an
example of a locally 𝓀-small type.

The membership relation on 𝕍 makes use of equality on 𝕍, and hence, has values
in 𝓀 ⁺ too. But, using that 𝕍 is locally 𝓀-small we can define an equivalent
𝓀-small membership relation.

These facts are used in our development relating set theoretic and type
theoretic ordinals, see Ordinals/CumulativeHierarchy-Addendum.lagda.

References
----------

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

\begin{code}

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

open import UF.FunExt
open import UF.PropTrunc
open import UF.Subsingletons

module UF.CumulativeHierarchy-LocallySmall
        (pt : propositional-truncations-exist)
        (fe : Fun-Ext)
        (pe : Prop-Ext)
       where

open import MLTT.Spartan
open import UF.Base hiding (_β‰ˆ_)
open import UF.Equiv
open import UF.EquivalenceExamples
open import UF.Equiv-FunExt
open import UF.Logic
open import UF.Size
open import UF.Sets-Properties
open import UF.Subsingletons-FunExt
open import UF.SubtypeClassifier
open import UF.SubtypeClassifier-Properties

open AllCombinators pt fe
open PropositionalTruncation pt

\end{code}

The idea is to have a 𝓀-valued equality relation on 𝕍 by defining:
  𝕍-set {A} f ＝⁻ 𝕍-set {B} g
inductively as
    (Ξ  a : A , βˆƒ b : B , f a ＝⁻ g b)
  Γ— (Ξ  b : B , βˆƒ a : A , g b ＝⁻ f a).

Of course, we need to formally check that this definition respects the 𝕍-set-ext
constructor of 𝕍 in both arguments, which is provided by the setup below.

\begin{code}

open import UF.CumulativeHierarchy pt fe pe

module 𝕍-is-locally-small
        {𝓀 : Universe}
        (ch : cumulative-hierarchy-exists 𝓀)
       where

 open cumulative-hierarchy-exists ch

 private
  module _
          {A : 𝓀 Μ‡ }
          (f : A β†’ 𝕍)
          (r : A β†’ 𝕍 β†’ Ξ© 𝓀)
         where

   ＝⁻-aux₁ : {B : 𝓀 Μ‡ } β†’ (B β†’ 𝕍) β†’ Ξ© 𝓀
   ＝⁻-aux₁ {B} g = (β±― a κž‰ A , Ǝ b κž‰ B , r a (g b) holds)
                  ∧ (β±― b κž‰ B , Ǝ a κž‰ A , r a (g b) holds)

   ＝⁻-aux₁-respects-β‰ˆ : {B' B : 𝓀 Μ‡ } (g' : B' β†’ 𝕍) (g : B β†’ 𝕍)
                       β†’ g' β‰ˆ g
                       β†’ ＝⁻-aux₁ g' holds
                       β†’ ＝⁻-aux₁ g  holds
   ＝⁻-aux₁-respects-β‰ˆ {B'} {B} g' g (s , t) (u , v) = β¦…1⦆ , β¦…2⦆
    where
     β¦…1⦆ : (a : A) β†’ βˆƒ b κž‰ B , r a (g b) holds
     β¦…1⦆ a = βˆ₯βˆ₯-rec βˆƒ-is-prop h₁ (u a)
      where
       h₁ : (Ξ£ b' κž‰ B' , r a (g' b') holds) β†’ βˆƒ b κž‰ B , r a (g b) holds
       h₁ (b' , p) = βˆ₯βˆ₯-functor hβ‚‚ (s b')
        where
         hβ‚‚ : (Ξ£ b κž‰ B , g b ＝ g' b') β†’ Ξ£ b κž‰ B , r a (g b) holds
         hβ‚‚ (b , e) = b , transport (Ξ» - β†’ (r a -) holds) (e ⁻¹) p
     β¦…2⦆ : (b : B) β†’ βˆƒ a κž‰ A , r a (g b) holds
     β¦…2⦆ b = βˆ₯βˆ₯-rec βˆƒ-is-prop h₁ (t b)
      where
       h₁ : (Ξ£ b' κž‰ B' , g' b' ＝ g b) β†’ βˆƒ a κž‰ A , r a (g b) holds
       h₁ (b' , e) = βˆ₯βˆ₯-functor hβ‚‚ (v b')
        where
         hβ‚‚ : (Ξ£ a κž‰ A , r a (g' b') holds) β†’ Ξ£ a κž‰ A , r a (g b) holds
         hβ‚‚ (a , p) = a , transport (Ξ» - β†’ (r a -) holds) e p

   ＝⁻-aux₁-respects-β‰ˆ' : {B' B : 𝓀 Μ‡ } (g' : B' β†’ 𝕍) (g : B β†’ 𝕍)
                        β†’ g' β‰ˆ g
                        β†’ ＝⁻-aux₁ g' ＝ ＝⁻-aux₁ g
   ＝⁻-aux₁-respects-β‰ˆ' {B'} {B} g' g e =
    Ξ©-extensionality pe fe
     (＝⁻-aux₁-respects-β‰ˆ g' g e)
     (＝⁻-aux₁-respects-β‰ˆ g g' (β‰ˆ-sym e))

   ＝⁻-auxβ‚‚ : 𝕍 β†’ Ξ© 𝓀
   ＝⁻-auxβ‚‚ = 𝕍-recursion (Ξ©-is-set fe pe) (Ξ» g _ β†’ ＝⁻-aux₁ g)
                          (Ξ» g' g _ _ _ _ e β†’ ＝⁻-aux₁-respects-β‰ˆ' g' g e)

   ＝⁻-auxβ‚‚-behaviour : {B : 𝓀 Μ‡ } (g : B β†’ 𝕍) β†’ ＝⁻-auxβ‚‚ (𝕍-set g) ＝ ＝⁻-aux₁ g
   ＝⁻-auxβ‚‚-behaviour g =
    𝕍-recursion-computes (Ξ©-is-set fe pe) (Ξ» g₁ _ β†’ ＝⁻-aux₁ g₁)
                         (Ξ» g' g _ _ _ _ e β†’ ＝⁻-aux₁-respects-β‰ˆ' g' g e)
                         g (Ξ» _ β†’ πŸ™ , πŸ™-is-prop)

  ＝⁻-auxβ‚‚-respects-β‰ˆ : {A B : 𝓀 Μ‡ } (f : A β†’ 𝕍) (g : B β†’ 𝕍)
                      β†’ (r₁ : A β†’ 𝕍 β†’ Ξ© 𝓀) (rβ‚‚ : B β†’ 𝕍 β†’ Ξ© 𝓀)
                      β†’ ((a : A) β†’ βˆƒ b κž‰ B , (f a ＝ g b) Γ— (r₁ a ＝ rβ‚‚ b))
                      β†’ ((b : B) β†’ βˆƒ a κž‰ A , (g b ＝ f a) Γ— (rβ‚‚ b ＝ r₁ a))
                      β†’ {C : 𝓀 Μ‡ } (h : C β†’ 𝕍)
                      β†’ ＝⁻-aux₁ f r₁ h holds
                      β†’ ＝⁻-aux₁ g rβ‚‚ h holds
  ＝⁻-auxβ‚‚-respects-β‰ˆ {A} {B} f g r₁ rβ‚‚ s t {C} h (u , v) = β¦…1⦆ , β¦…2⦆
   where
    β¦…1⦆ : (b : B) β†’ βˆƒ c κž‰ C , rβ‚‚ b (h c) holds
    β¦…1⦆ b = βˆ₯βˆ₯-rec βˆƒ-is-prop m (t b)
     where
      m : (Ξ£ a κž‰ A , (g b ＝ f a) Γ— (rβ‚‚ b ＝ r₁ a))
        β†’ βˆƒ c κž‰ C , rβ‚‚ b (h c) holds
      m (a , _ , q) = βˆ₯βˆ₯-functor n (u a)
       where
        n : (Ξ£ c κž‰ C , r₁ a (h c) holds)
          β†’ Ξ£ c κž‰ C , rβ‚‚ b (h c) holds
        n (c , w) = c , Idtofun (ap _holds (happly (q ⁻¹) (h c))) w
    β¦…2⦆ : (c : C) β†’ βˆƒ b κž‰ B , rβ‚‚ b (h c) holds
    β¦…2⦆ c = βˆ₯βˆ₯-rec βˆƒ-is-prop n (v c)
     where
      n : (Ξ£ a κž‰ A , r₁ a (h c) holds)
        β†’ βˆƒ b κž‰ B , rβ‚‚ b (h c) holds
      n (a , w) = βˆ₯βˆ₯-functor m (s a)
       where
        m : (Ξ£ b κž‰ B , (f a ＝ g b) Γ— (r₁ a ＝ rβ‚‚ b))
          β†’ Ξ£ b κž‰ B , rβ‚‚ b (h c) holds
        m (b , _ , q) = b , Idtofun (ap _holds (happly q (h c))) w

  ＝⁻-auxβ‚‚-respects-β‰ˆ' : {A B : 𝓀 Μ‡ } (f : A β†’ 𝕍) (g : B β†’ 𝕍)
                         (r₁ : A β†’ 𝕍 β†’ Ξ© 𝓀) (rβ‚‚ : B β†’ 𝕍 β†’ Ξ© 𝓀)
                       β†’ ((a : A) β†’ βˆƒ b κž‰ B , (f a ＝ g b) Γ— (r₁ a ＝ rβ‚‚ b))
                       β†’ ((b : B) β†’ βˆƒ a κž‰ A , (g b ＝ f a) Γ— (rβ‚‚ b ＝ r₁ a))
                       β†’ f β‰ˆ g
                       β†’ ＝⁻-auxβ‚‚ f r₁ ＝ ＝⁻-auxβ‚‚ g rβ‚‚
  ＝⁻-auxβ‚‚-respects-β‰ˆ' {A} {B} f g r₁ rβ‚‚ IH₁ IHβ‚‚ _ =
   dfunext fe (𝕍-prop-simple-induction (Ξ» x β†’ ＝⁻-auxβ‚‚ f r₁ x ＝ ＝⁻-auxβ‚‚ g rβ‚‚ x)
                                       (Ξ» _ β†’ Ξ©-is-set fe pe)
                                       Οƒ)
    where
     Οƒ : {C : 𝓀 Μ‡ } (h : C β†’ 𝕍)
       β†’ ＝⁻-auxβ‚‚ f r₁ (𝕍-set h) ＝ ＝⁻-auxβ‚‚ g rβ‚‚ (𝕍-set h)
     Οƒ h = ＝⁻-auxβ‚‚ f r₁ (𝕍-set h) ＝⟨ ＝⁻-auxβ‚‚-behaviour f r₁ h      ⟩
           ＝⁻-aux₁ f r₁ h         ＝⟨ e                              ⟩
           ＝⁻-aux₁ g rβ‚‚ h         ＝⟨ (＝⁻-auxβ‚‚-behaviour g rβ‚‚ h) ⁻¹ ⟩
           ＝⁻-auxβ‚‚ g rβ‚‚ (𝕍-set h) ∎
      where
       e = Ξ©-extensionality pe fe
            (＝⁻-auxβ‚‚-respects-β‰ˆ f g r₁ rβ‚‚ IH₁ IHβ‚‚ h)
            (＝⁻-auxβ‚‚-respects-β‰ˆ g f rβ‚‚ r₁ IHβ‚‚ IH₁ h)

\end{code}

We package up the above in the following definition which records the behaviour
of the relation on the 𝕍-set constructor.

\begin{code}

  ＝⁻[Ξ©]-packaged : Ξ£ Ο• κž‰ (𝕍 β†’ 𝕍 β†’ Ξ© 𝓀) , ({A : 𝓀 Μ‡ } (f : A β†’ 𝕍)
                                           (r : A β†’ 𝕍 β†’ Ξ© 𝓀)
                                        β†’ Ο• (𝕍-set f) ＝ ＝⁻-auxβ‚‚ f r)
  ＝⁻[Ξ©]-packaged = 𝕍-recursion-with-computation
                     (Ξ -is-set fe (Ξ» _ β†’ Ξ©-is-set fe pe))
                     ＝⁻-auxβ‚‚
                     ＝⁻-auxβ‚‚-respects-β‰ˆ'

 _＝⁻[Ξ©]_ : 𝕍 β†’ 𝕍 β†’ Ξ© 𝓀
 _＝⁻[Ξ©]_ = pr₁ ＝⁻[Ξ©]-packaged

 _＝⁻_ : 𝕍 β†’ 𝕍 β†’ 𝓀 Μ‡
 x ＝⁻ y = (x ＝⁻[Ω] y) holds

 ＝⁻-is-prop-valued : {x y : 𝕍} β†’ is-prop (x ＝⁻ y)
 ＝⁻-is-prop-valued {x} {y} = holds-is-prop (x ＝⁻[Ω] y)

\end{code}

The following lemma shows that the relation ＝⁻ indeed implements the idea
announced in the comment above.

\begin{code}

 private
  ＝⁻-behaviour : {A B : 𝓀 Μ‡ } (f : A β†’ 𝕍) (g : B β†’ 𝕍)
               β†’ (𝕍-set f ＝⁻ 𝕍-set g)
               ＝ ( ((a : A) β†’ βˆƒ b κž‰ B , f a ＝⁻ g b)
                  Γ— ((b : B) β†’ βˆƒ a κž‰ A , f a ＝⁻ g b))
  ＝⁻-behaviour {A} {B} f g =
   (𝕍-set f ＝⁻ 𝕍-set g)          ＝⟨ β¦…1⦆ ⟩
   (＝⁻-auxβ‚‚ f r (𝕍-set g) holds) ＝⟨ β¦…2⦆ ⟩
   T                              ∎
    where
     T : 𝓀 Μ‡
     T = ((a : A) β†’ βˆƒ b κž‰ B , f a ＝⁻ g b)
       Γ— ((b : B) β†’ βˆƒ a κž‰ A , f a ＝⁻ g b)
     r : A β†’ 𝕍 β†’ Ξ© 𝓀
     r a y = f a ＝⁻[Ω] y
     β¦…1⦆ = ap _holds (happly (prβ‚‚ ＝⁻[Ξ©]-packaged f r) (𝕍-set g))
     β¦…2⦆ = ap _holds (＝⁻-auxβ‚‚-behaviour f r g)

\end{code}

Finally, we show that ＝⁻ and ＝ are equivalent, making 𝕍 a locally small type.

\begin{code}

 ＝⁻-to-＝ : {x y : 𝕍} β†’ x ＝⁻ y β†’ x ＝ y
 ＝⁻-to-＝ {x} {y} =
  𝕍-prop-induction (Ξ» u β†’ ((v : 𝕍) β†’ u ＝⁻ v β†’ u ＝ v))
                   (Ξ» _ β†’ Ξ β‚‚-is-prop fe (Ξ» _ _ β†’ 𝕍-is-large-set))
                   (Ξ» {A} f r β†’ 𝕍-prop-simple-induction _
                                 (Ξ» _ β†’ Ξ -is-prop fe (Ξ» _ β†’ 𝕍-is-large-set))
                                 (Ξ» {B} g β†’ h f g r))
                   x y
   where
    h : {A B : 𝓀 Μ‡ } (f : A β†’ 𝕍) (g : B β†’ 𝕍)
      β†’ ((a : A) (v : 𝕍) β†’ f a ＝⁻ v β†’ f a ＝ v)
      β†’ 𝕍-set f ＝⁻ 𝕍-set g β†’ 𝕍-set f ＝ 𝕍-set g
    h {A} {B} f g r e = 𝕍-set-ext f g (β¦…1⦆ , β¦…2⦆)
     where
      u : (a : A) β†’ βˆƒ b κž‰ B , f a ＝⁻ g b
      u = pr₁ (Idtofun (＝⁻-behaviour f g) e)
      v : (b : B)Β β†’ βˆƒ a κž‰ A , f a ＝⁻ g b
      v = prβ‚‚ (Idtofun (＝⁻-behaviour f g) e)
      β¦…1⦆ : (a : A) β†’ βˆƒ b κž‰ B , g b ＝ f a
      β¦…1⦆ a = βˆ₯βˆ₯-functor (Ξ» (b , p) β†’ b , ((r a (g b) p) ⁻¹)) (u a)
      β¦…2⦆ : (b : B) β†’ βˆƒ a κž‰ A , f a ＝ g b
      β¦…2⦆ b = βˆ₯βˆ₯-functor (Ξ» (a , p) β†’ a , r a (g b) p) (v b)

 ＝⁻-is-reflexive : {x : 𝕍} β†’ x ＝⁻ x
 ＝⁻-is-reflexive {x} = 𝕍-prop-induction (Ξ» - β†’ - ＝⁻ -)
                                         (Ξ» _ β†’ ＝⁻-is-prop-valued)
                                         h x
  where
   h : {A : 𝓀 Μ‡ } (f : A β†’ 𝕍)
     β†’ ((a : A) β†’ f a ＝⁻ f a)
     β†’ 𝕍-set f ＝⁻ 𝕍-set f
   h {A} f r = Idtofun⁻¹ (＝⁻-behaviour f f)
                         ((Ξ» a β†’ ∣ a , r a ∣) , (Ξ» a β†’ ∣ a , r a ∣))

 ＝-to-＝⁻ : {x y : 𝕍} β†’ x ＝ y β†’ x ＝⁻ y
 ＝-to-＝⁻ refl = ＝⁻-is-reflexive

 ＝⁻-≃-＝ : {x y : 𝕍} β†’ (x ＝⁻ y) ≃ (x ＝ y)
 ＝⁻-≃-＝ = logically-equivalent-props-are-equivalent
             ＝⁻-is-prop-valued
             𝕍-is-large-set
             ＝⁻-to-＝
             ＝-to-＝⁻

 𝕍-is-locally-small : is-locally-small 𝕍
 𝕍-is-locally-small x y = (x ＝⁻ y) , ＝⁻-≃-＝

 ＝⁻-is-transitive : {x y z : 𝕍} β†’ x ＝⁻ y β†’ y ＝⁻ z β†’ x ＝⁻ z
 ＝⁻-is-transitive {x} {y} {z} u v = ＝-to-＝⁻ (＝⁻-to-＝ u βˆ™ ＝⁻-to-＝ v)

 ＝⁻-is-symmetric : {x y : 𝕍} β†’ x ＝⁻ y β†’ y ＝⁻ x
 ＝⁻-is-symmetric {x} {y} e = ＝-to-＝⁻ ((＝⁻-to-＝ e)⁻¹)

\end{code}

We now make use of the fact that 𝕍 is locally small by introducing a
small-valued membership relation on 𝕍.

\begin{code}

 _∈⁻[Ξ©]_ : 𝕍 β†’ 𝕍 β†’ Ξ© 𝓀
 _∈⁻[Ξ©]_ x = 𝕍-prop-simple-recursion
              (Ξ» {A} f β†’ (βˆƒ a κž‰ A , f a ＝⁻ x) , βˆƒ-is-prop) e
  where
   e : {A B : 𝓀 Μ‡ } (f : A β†’ 𝕍) (g : B β†’ 𝕍)
     β†’ f ≲ g β†’ (βˆƒ a κž‰ A , f a ＝⁻ x) β†’ (βˆƒ b κž‰ B , g b ＝⁻ x)
   e {A} {B} f g s =
    βˆ₯βˆ₯-rec βˆƒ-is-prop
           (Ξ» (a , p) β†’ βˆ₯βˆ₯-functor (Ξ» (b , q)
                                      β†’ b , ＝-to-＝⁻ (q βˆ™ ＝⁻-to-＝ p))
                                   (s a))

 _∈⁻_ : 𝕍 β†’ 𝕍 β†’ 𝓀 Μ‡
 x ∈⁻ y = (x ∈⁻[Ω] y) holds

 ∈⁻-for-𝕍-sets : (x : 𝕍) {A : 𝓀 Μ‡ } (f : A β†’ 𝕍)
               β†’ (x ∈⁻ 𝕍-set f) ＝ (βˆƒ a κž‰ A , f a ＝⁻ x)
 ∈⁻-for-𝕍-sets x f = ap pr₁ (𝕍-prop-simple-recursion-computes _ _ f)

 ∈⁻-is-prop-valued : {x y : 𝕍} β†’ is-prop (x ∈⁻ y)
 ∈⁻-is-prop-valued {x} {y} = holds-is-prop (x ∈⁻[Ω] y)

 ∈⁻-≃-∈ : {x y : 𝕍} β†’ x ∈⁻ y ≃ x ∈ y
 ∈⁻-≃-∈ {x} {y} =
  𝕍-prop-simple-induction _ (Ξ» _ β†’ ≃-is-prop (Ξ» _ _ β†’ fe) ∈-is-prop-valued) h y
   where
    h : {A : 𝓀 Μ‡ } (f : A β†’ 𝕍) β†’ (x ∈⁻ 𝕍-set f) ≃ (x ∈ 𝕍-set f)
    h {A} f = x ∈⁻ 𝕍-set f          β‰ƒβŸ¨ β¦…1⦆ ⟩
              (βˆƒ a κž‰ A , f a ＝⁻ x) β‰ƒβŸ¨ β¦…2⦆ ⟩
              (βˆƒ a κž‰ A , f a ＝ x)  β‰ƒβŸ¨ β¦…3⦆ ⟩
              x ∈ 𝕍-set f           β– 
     where
      β¦…1⦆ = idtoeq _ _ (∈⁻-for-𝕍-sets x f)
      β¦…2⦆ = βˆƒ-cong pt (Ξ» a β†’ ＝⁻-≃-＝)
      β¦…3⦆ = idtoeq _ _ ((∈-for-𝕍-sets x f) ⁻¹)

 ∈⁻-to-∈ : {x y : 𝕍} β†’ x ∈⁻ y β†’ x ∈ y
 ∈⁻-to-∈ {x} {y} = ⌜ ∈⁻-≃-∈ ⌝

 ∈-to-∈⁻ : {x y : 𝕍} β†’ x ∈ y β†’ x ∈⁻ y
 ∈-to-∈⁻ {x} {y} = ⌜ ∈⁻-≃-∈ ⌝⁻¹

\end{code}