We show that ๐• is locally small, following Section 10.5 of the HoTT Book.

\begin{code}

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

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

module 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.Subsingletons-FunExt

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 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 fe pe
     (๏ผโป-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 fe pe
            (๏ผโป-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 = back-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}