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}