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 =
(οΌβ»-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)
(Ξ -is-set fe (Ξ» _ β Ξ©-is-set fe pe))
οΌβ»-auxβ
οΌβ»-auxβ-respects-β'

_οΌβ»[Ξ©]_ : π β π β Ξ© π€

_οΌβ»_ : π β π β π€ Μ
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}