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

We define the induction principle (with a non-judgemental computation principle)
of the cumulative hierarchy π (with respect to a type universe π€) as introduced
in Section 10.5 of the HoTT Book [1]. Using the induction principle we formulate
what it means for the cumulative hierarchy to exist, so that can use it as an
(module) assumption in further developments.

For example, in Ordinals/CumulativeHierarchy we show that the (type theoretic)
ordinal of set theoretic ordinals in π (w.r.t. π€) is isomorphic to the ordinal
of ordinals in π€.

This file has three parts:
(I)    Introduction of the cumulative hierarchy π and the statement of its
(most general) induction principle.
(II)   Statements and proofs of some simpler, more specialised, induction and
recursion principles for π.
(III)  Basic constructions and proofs for π, i.e. the definition of set
membership (β), subset relation (β) and proofs of β-extensionality and
β-induction.

The cumulative hierarchy π can be seen as a HoTT-refined version of Aczel's [2]
type theoretic interpretation of constructive set theory and draws inspiration
form Joyal and Moerdijk's [3] algebraic set theory.

References
----------

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

[2] 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

[3] A. Joyal and I. Moerdijk
Algebraic set theory
Volume 220 of London Mathematical Society Lecture Note Series
Cambridge University Press
1995
doi:10.1017/CBO9780511752483

\begin{code}

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

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

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

open PropositionalTruncation pt

open import MLTT.Spartan
open import UF.Base hiding (_β_)
open import UF.Sets
open import UF.SubtypeClassifier
open import UF.SubtypeClassifier-Properties
open import UF.Subsingletons-FunExt
open import UF.Subsingletons-Properties

_β²_ : {A : π€ Μ } {B : π₯ Μ } {X : π£ Μ } β (A β X) β (B β X) β π€ β π₯ β π£ Μ
_β²_ {π€} {π₯} {π£} {A} {B} f g = (a : A) β β b κ B , g b οΌ f a

-- Note that _β_ says that f and g have equal images
_β_ : {A : π€ Μ } {B : π₯ Μ } {X : π£ Μ } β (A β X) β (B β X) β π€ β π₯ β π£ Μ
f β g = f β² g Γ g β² f

β-sym : {A : π€ Μ } {B : π₯ Μ } {X : π£ Μ } {f : A β X} {g : B β X}
β f β g β g β f
β-sym (u , v) = (v , u)

\end{code}

Part I
------

Introduction of the cumulative hierarchy π and the statement of its (most
general) induction principle.

See Section 10.5 of the HoTT Book [1] for more of an explanation regarding the
induction principle of π.

For comparison, the higher inductive type (HIT) presentation of π (w.r.t. π€) is:
β For every A : π€ and f : A β π, we have an element π-set f : π
β For every A, B : π€, f : A β π and g : B β π, if f β g, then π-set f οΌ π-set g
β π is set-truncated: for every x, y : π and p, q : x οΌ y, we have p οΌ q.

We require that the type π is a set in the sense of HoTT, i.e. its elements are
equal in at most one way. In the set theoretic sense it is of course a proper
class and not a set: the type π lives in the next type universe π€ βΊ. To try to
avoid confusion, we explicitly introduce the definition "is-large-set" below, as
suggested by MartΓ­n EscardΓ³.

\begin{code}

module _ (π€ : Universe) where

is-large-set : π€ βΊ Μ β π€ βΊ Μ
is-large-set = is-set

record cumulative-hierarchy-exists : π€Ο where
field
π : π€ βΊ Μ
π-is-large-set : is-large-set π
π-set : {A : π€ Μ } β (A β π) β π
π-set-ext : {A B : π€ Μ } (f : A β π) (g : B β π) β f β g β π-set f οΌ π-set g
π-induction : {π£ : Universe} (P : π β π£ Μ )
β ((x : π) β is-set (P x))
β (Ο : {A : π€ Μ } (f : A β π ) β ((a : A) β P (f a)) β P (π-set f))
β ({A B : π€ Μ } (f : A β π) (g : B β π) (e : f β g)
β (IHβ : (a : A) β P (f a))
β (IHβ : (b : B) β P (g b))
β ((a : A) β β₯ Ξ£ b κ B , Ξ£ p κ f a οΌ g b ,
transport P p (IHβ a) οΌ IHβ b β₯)
β ((b : B) β β₯ Ξ£ a κ A , Ξ£ p κ g b οΌ f a ,
transport P p (IHβ b) οΌ IHβ a β₯)
β transport P (π-set-ext f g e) (Ο f IHβ) οΌ Ο g IHβ)
β (x : π) β P x
π-induction-computes : {π£ : Universe} (P : π β π£ Μ )
β (Ο : (x : π) β is-set (P x))
β (Ο : {A : π€ Μ } (f : A β π ) β ((a : A) β P (f a))
β P (π-set f))
β (Ο : {A B : π€ Μ } (f : A β π) (g : B β π) (e : f β g)
β (IHβ : (a : A) β P (f a))
β (IHβ : (b : B) β P (g b))
β ((a : A) β β₯ Ξ£ b κ B , Ξ£ p κ f a οΌ g b ,
transport P p (IHβ a) οΌ IHβ b β₯)
β ((b : B) β β₯ Ξ£ a κ A , Ξ£ p κ g b οΌ f a ,
transport P p (IHβ b) οΌ IHβ a β₯)
β transport P (π-set-ext f g e) (Ο f IHβ) οΌ Ο g IHβ)
β {A : π€ Μ } (f : A β π) (IH : (a : A) β P (f a))
β π-induction P Ο Ο Ο (π-set f) οΌ Ο f IH

\end{code}

Part II
-------

Statements and proofs of some simpler, more specialised, induction and recursion
principles for π.

We start with deriving the recursion principle for π, i.e. its nondependent
induction principle. It should be noted that this is completely routine.

\begin{code}

π-recursion-with-computation :
{π£ : Universe} {X : π£ Μ }
β (Ο : is-set X)
β (Ο : {A : π€ Μ } (f : A β π) β (A β X) β X)
β (Ο : {A B : π€ Μ } (f : A β π) (g : B β π)
β (IHβ : A β X)
β (IHβ : B β X)
β ((a : A) β β₯ Ξ£ b κ B , Ξ£ p κ f a οΌ g b , IHβ a οΌ IHβ b β₯)
β ((b : B) β β₯ Ξ£ a κ A , Ξ£ p κ g b οΌ f a , IHβ b οΌ IHβ a β₯)
β f β g β Ο f IHβ οΌ Ο g IHβ)
β Ξ£ Ο κ (π β X) , ({A : π€ Μ } (f : A β π)
(IH : A β X) β Ο (π-set f) οΌ Ο f IH)
π-recursion-with-computation {π£} {X} Ο Ο Ο =
( π-induction (Ξ» _ β X) (Ξ» _ β Ο) Ο Ο'
, π-induction-computes (Ξ» _ β X) (Ξ» _ β Ο) Ο Ο')
where
Ο' : {A B : π€ Μ } (f : A β π) (g : B β π)
β (e : f β g) (IHβ : A β X) (IHβ : B β X)
β ((a : A) β β₯ Ξ£ b κ B , Ξ£ p κ f a οΌ g b ,
transport (Ξ» _ β X) p (IHβ a) οΌ IHβ b β₯)
β ((b : B) β β₯ Ξ£ a κ A , Ξ£ p κ g b οΌ f a ,
transport (Ξ» _ β X) p (IHβ b) οΌ IHβ a β₯)
β transport (Ξ» _ β X) (π-set-ext f g e) (Ο f IHβ) οΌ Ο g IHβ
Ο' {A} {B} f g e IHβ IHβ hIHβ hIHβ =
transport (Ξ» _ β X) e' (Ο f IHβ) οΌβ¨ transport-const e'          β©
Ο f IHβ                          οΌβ¨ Ο f g IHβ IHβ hIHβ' hIHβ' e β©
Ο g IHβ                          β
where
e' = π-set-ext f g e
hIHβ' : (a : A) β β₯ Ξ£ b κ B , Ξ£ p κ f a οΌ g b , IHβ a οΌ IHβ b β₯
hIHβ' a = β₯β₯-functor
(Ξ» (b , p , q) β (b , p , ((transport-const p) β»ΒΉ β q)))
(hIHβ a)
hIHβ' : (b : B) β β₯ Ξ£ a κ A , Ξ£ p κ g b οΌ f a , IHβ b οΌ IHβ a β₯
hIHβ' b = β₯β₯-functor
(Ξ» (a , p , q) β (a , p , ((transport-const p) β»ΒΉ β q)))
(hIHβ b)

π-recursion : {π£ : Universe} {X : π£ Μ }
β is-set X
β (Ο : ({A : π€ Μ } (f : A β π) β (A β X) β X))
β ({A B : π€ Μ } (f : A β π) (g : B β π)
β (IHβ : A β X) (IHβ : B β X)
β ((a : A) β β₯ Ξ£ b κ B , Ξ£ p κ f a οΌ g b , IHβ a οΌ IHβ b β₯)
β ((b : B) β β₯ Ξ£ a κ A , Ξ£ p κ g b οΌ f a , IHβ b οΌ IHβ a β₯)
β f β g β Ο f IHβ οΌ Ο g IHβ)
β π β X
π-recursion Ο Ο Ο = prβ (π-recursion-with-computation Ο Ο Ο)

π-recursion-computes :
{π£ : Universe} {X : π£ Μ }
β (Ο : is-set X)
β (Ο : {A : π€ Μ } (f : A β π) β (A β X) β X)
β (Ο : {A B : π€ Μ } (f : A β π) (g : B β π)
β (IHβ : A β X) (IHβ : B β X)
β ((a : A) β β₯ Ξ£ b κ B , Ξ£ p κ f a οΌ g b , IHβ a οΌ IHβ b β₯)
β ((b : B) β β₯ Ξ£ a κ A , Ξ£ p κ g b οΌ f a , IHβ b οΌ IHβ a β₯)
β f β g β Ο f IHβ οΌ Ο g IHβ)
β ({A : π€ Μ } (f : A β π) (IH : A β X)
β π-recursion Ο Ο Ο (π-set f) οΌ Ο f IH)
π-recursion-computes Ο Ο Ο f = prβ (π-recursion-with-computation Ο Ο Ο) f

\end{code}

Next, we observe that when P is a family of propositions, then the induction
principle simplifies significantly.

\begin{code}

π-prop-induction : {π£ : Universe} (P : π β π£ Μ )
β ((x : π) β is-prop (P x))
β ({A : π€ Μ } (f : A β π) β ((a : A) β P (f a)) β P (π-set f))
β (x : π) β P x
π-prop-induction {π£} P P-is-prop-valued Ο =
π-induction P (Ξ» x β props-are-sets (P-is-prop-valued x)) Ο
(Ξ» f g e IHβ IHβ _ _ β P-is-prop-valued _ _ _)

π-prop-simple-induction : {π£ : Universe} (P : π β π£ Μ )
β ((x : π) β is-prop (P x))
β ({A : π€ Μ } (f : A β π) β P (π-set f))
β (x : π) β P x
π-prop-simple-induction P Ο Ο = π-prop-induction P Ο (Ξ» f _ β Ο f)

\end{code}

Because implication makes the set Ξ© into a poset, we can give specialised
recursion principles for π β Ξ© by (roughly) asking that β² is mapped to
implication.

\begin{code}

private
π-prop-recursion-with-computation :
{π£ : Universe}
β (Ο : ({A : π€ Μ } (f : A β π) β (A β Ξ© π£) β Ξ© π£))
β (Ο : {A B : π€ Μ } (f : A β π) (g : B β π)
β (IHβ : A β Ξ© π£) (IHβ : B β Ξ© π£)
β ((a : A) β β₯ Ξ£ b κ B , Ξ£ p κ f a οΌ g b , IHβ a οΌ IHβ b β₯)
β f β² g β Ο f IHβ holds β Ο g IHβ holds)
β Ξ£ Ο κ (π β Ξ© π£) , ({A : π€ Μ } (f : A β π) (IH : A β Ξ© π£)
β Ο (π-set f) οΌ Ο f IH)
π-prop-recursion-with-computation {π£} Ο Ο =
( π-recursion (Ξ©-is-set fe pe) Ο Ο'
, π-recursion-computes (Ξ©-is-set fe pe) Ο Ο')
where
Ο' : {A B : π€ Μ } (f : A β π) (g : B β π)
β (IHβ : A β Ξ© π£) (IHβ : B β Ξ© π£)
β ((a : A) β β₯ Ξ£ b κ B , Ξ£ p κ f a οΌ g b , IHβ a οΌ IHβ b β₯)
β ((b : B) β β₯ Ξ£ a κ A , Ξ£ p κ g b οΌ f a , IHβ b οΌ IHβ a β₯)
β f β g β Ο f IHβ οΌ Ο g IHβ
Ο' f g IHβ IHβ hIHβ hIHβ (mβ , mβ) =
Ξ©-extensionality pe fe (Ο f g IHβ IHβ hIHβ mβ)
(Ο g f IHβ IHβ hIHβ mβ)

π-prop-recursion : {π£ : Universe}
β (Ο : ({A : π€ Μ } (f : A β π) β (A β Ξ© π£) β Ξ© π£))
β ({A B : π€ Μ } (f : A β π) (g : B β π)
β (IHβ : A β Ξ© π£) (IHβ : B β Ξ© π£)
β ((a : A) β β₯ Ξ£ b κ B ,
Ξ£ p κ f a οΌ g b , IHβ a οΌ IHβ b β₯)
β f β² g β Ο f IHβ holds β Ο g IHβ holds)
β π β Ξ© π£
π-prop-recursion {π£} Ο Ο =
prβ (π-prop-recursion-with-computation Ο Ο)

π-prop-recursion-computes : {π£ : Universe}
β (Ο : ({A : π€ Μ } (f : A β π) β (A β Ξ© π£) β Ξ© π£))
β (Ο : {A B : π€ Μ } (f : A β π) (g : B β π)
β (IHβ : A β Ξ© π£) (IHβ : B β Ξ© π£)
β ((a : A) β β₯ Ξ£ b κ B , Ξ£ p κ f a οΌ g b ,
IHβ a οΌ IHβ b β₯)
β f β² g β Ο f IHβ holds β Ο g IHβ holds)
β ({A : π€ Μ } (f : A β π) (IH : A β Ξ© π£)
β π-prop-recursion Ο Ο (π-set f) οΌ Ο f IH)
π-prop-recursion-computes Ο Ο f =
prβ (π-prop-recursion-with-computation Ο Ο) f

\end{code}

We also have a simpler version of the above in the case that we don't need to
make recursive calls.

\begin{code}

π-prop-simple-recursion : {π£ : Universe}
β (Ο : ({A : π€ Μ } β (A β π) β Ξ© π£))
β ({A B : π€ Μ } (f : A β π) (g : B β π)
β f β² g β Ο f holds β Ο g holds)
β π β Ξ© π£
π-prop-simple-recursion {π£} Ο Ο =
π-prop-recursion (Ξ» f _ β Ο f) (Ξ» f g _ _ _ β Ο f g)

π-prop-simple-recursion-computes :
{π£ : Universe}
β (Ο : ({A : π€ Μ } β (A β π) β Ξ© π£))
β (Ο : {A B : π€ Μ } (f : A β π) (g : B β π)
β f β² g β Ο f holds β Ο g holds)
β ({A : π€ Μ } (f : A β π) β π-prop-simple-recursion Ο Ο (π-set f) οΌ Ο f)
π-prop-simple-recursion-computes Ο Ο f =
π-prop-recursion-computes (Ξ» f _ β Ο f) (Ξ» f g _ _ _ β Ο f g)
f (Ξ» _ β π , π-is-prop)

\end{code}

Part III
--------

Basic constructions and proofs for π, i.e. the definition of set membership (β),
subset relation (β) and proofs of β-extensionality and β-induction.

\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 , (q β p)) (s a))

_β_ : π β π β π€ βΊ Μ
x β y = (x β[Ξ©] y) holds

β-is-prop-valued : {x y : π} β is-prop (x β y)
β-is-prop-valued {x} {y} = holds-is-prop (x β[Ξ©] y)

β-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)

from-β-of-π-set : {x : π} {A : π€ Μ } {f : A β π}
β (x β π-set f) β (β a κ A , f a οΌ x)
from-β-of-π-set {x} {A} {f} = Idtofun (β-for-π-sets x f)

to-β-of-π-set : {x : π} {A : π€ Μ } {f : A β π}
β (β a κ A , f a οΌ x) β (x β π-set f)
to-β-of-π-set {x} {A} {f} = Idtofunβ»ΒΉ (β-for-π-sets x f)

_β_ : π β π β π€ βΊ Μ
x β y = (v : π) β v β x β v β y

β-to-β² : {A B : π€ Μ } (f : A β π) (g : B β π)
β π-set f β π-set g β f β² g
β-to-β² {A} {B} f g s a = from-β-of-π-set m
where
m : f a β π-set g
m = s (f a) (to-β-of-π-set β£ a , refl β£)

β²-to-β : {A B : π€ Μ } (f : A β π) (g : B β π)
β f β² g β π-set f β π-set g
β²-to-β {A} {B} f g s x m = to-β-of-π-set n
where
m' : β a κ A , f a οΌ x
m' = from-β-of-π-set m
n : β b κ B , g b οΌ x
n = β₯β₯-rec β-is-prop
(Ξ» (a , p) β β₯β₯-functor (Ξ» (b , q) β b , (q β p)) (s a)) m'

β-is-prop-valued : {x y : π} β is-prop (x β y)
β-is-prop-valued = Ξ β-is-prop fe (Ξ» _ _ β β-is-prop-valued)

β-is-reflexive : {x : π} β x β x
β-is-reflexive _ = id

οΌ-to-β : {x y : π} β x οΌ y β x β y
οΌ-to-β refl = β-is-reflexive

\end{code}

We now prove, using the induction principles of π above, two simple
set-theoretic axioms: β-extensionality and β-induction.

\begin{code}

pre-extensionality : {A : π€ Μ } (f : A β π) (x : π)
β x β π-set f β π-set f β x β x οΌ π-set f
pre-extensionality f =
π-prop-simple-induction (Ξ» x β x β π-set f β π-set f β x β x οΌ π-set f)
(Ξ» _ β Ξ β-is-prop fe (Ξ» _ _ β π-is-large-set))
Ξ³
where
Ξ³ : {B : π€ Μ } (g : B β π)
β π-set g β π-set f β π-set f β π-set g β π-set g οΌ π-set f
Ξ³ g s t = π-set-ext g f (β-to-β² g f s , β-to-β² f g t)

β-extensionality : (x y : π) β x β y β y β x β x οΌ y
β-extensionality x y =
π-prop-simple-induction (Ξ» v β x β v β v β x β x οΌ v)
(Ξ» _ β Ξ β-is-prop fe (Ξ» _ _ β π-is-large-set))
(Ξ» f β pre-extensionality f x)
y

β-induction : {π£ : Universe} (P : π β π£ Μ )
β ((x : π) β is-prop (P x))
β ((x : π) β ((y : π) β y β x β P y) β P x)
β (x : π) β P x
β-induction P P-is-prop-valued h = π-prop-induction P P-is-prop-valued Ξ³
where
Ξ³ : {A : π€ Μ } (f : A β π) β ((a : A) β P (f a)) β P (π-set f)
Ξ³ {A} f IH = h (π-set f) c
where
c : (y : π) β y β π-set f β P y
c y m = β₯β₯-rec (P-is-prop-valued y) (Ξ» (a , p) β transport P p (IH a)) m'
where
m' : β a κ A , f a οΌ y
m' = from-β-of-π-set m

\end{code}