{-# OPTIONS --lossy-unification #-}
open import 1Lab.Prelude hiding (ext)

open import Data.Sum.Base
open import Data.Image
open import Data.Bool

module Data.Set.Material where

The cumulative hierarchy🔗

This module defines the cumulative hierarchy of material sets, as a recursive higher inductive type, following §10.5 of the HoTT book. We then prove that our model V (at any universe level) is a model of the theory IZF: it validates the axioms of empty set, pairing, union, infinity, replacement, separation, power set, and $\in \text{-induction.}$

Our higher inductive type is generated by the constructor set, together with the extensionality constructor ext, and the necessary set-truncation.

data V ℓ : Type (lsuc ℓ) where
  set : (A : Type ℓ) → (A → V ℓ) → V ℓ
  ext
    : ∀ {A B : Type ℓ} (f : A → V ℓ) (g : B → V ℓ)
    → ((a : A) → ∥ fibre g (f a) ∥)
    → ((b : B) → ∥ fibre f (g b) ∥)
    → set A f ≡ set B g
  squash : is-set (V ℓ)

The type V resembles a W-type: the constructor set corresponds to the “supremum” of a family of sets, where the “branching factor” of the family is allowed to be any type in the universe $\ell \text{.}$ Of course, if we could take the supremum of V-many sets, we could reproduce Russell’s paradox, so Agda rightly forces us to put V in $\ell \text{’s}$ successor universe.

The mere fibres in the extensionality constructor, as we’ll see in a bit, are exactly the normal forms of the propositions $f(a)\in \mathrm{set}(B,g)$ and $g(b)\in \mathrm{set}(A,f)\text{.}$ You should think of ext as an instance of the axiom of extensionality, specialised for values which are “explicit” sets: If every element $f(a)$ is somewhere in $g\text{,}$ and every $g(b)$ is somewhere in $f\text{,}$ then $f$ and $g$ present the same sets.

As usual for higher inductive types, we have an elimination principle into families of propositions, which allows us to ignore all the higher constructors. If $P$ holds of $\mathrm{set}(A,f)\text{,}$ assuming that it holds for every value of $f\text{,}$ then it holds for any set.

V-elim-prop
  : ∀ {ℓ ℓ'} (P : V ℓ → Type ℓ')
  → (∀ x → is-prop (P x))
  → (∀ {A} (f : A → V ℓ) → (∀ x → P (f x)) → P (set A f))
  → ∀ x → P x

V-elim-prop P p-prop p-set (set A x) = p-set x λ a → V-elim-prop P p-prop p-set (x a)
V-elim-prop P p-prop p-set (ext f g x y i) =
  is-prop→pathp (λ i → p-prop (ext f g x y i))
    (p-set f λ a → V-elim-prop P p-prop p-set (f a))
    (p-set g λ a → V-elim-prop P p-prop p-set (g a)) i
V-elim-prop P p-prop p-set (squash x y p q i j) =
  is-prop→squarep (λ i j → p-prop (squash x y p q i j))
    (λ _ → go x) (λ i → go (p i)) (λ i → go (q i)) (λ _ → go y) i j
  where go = V-elim-prop P p-prop p-set

V-elim-prop'
  : ∀ {ℓ ℓ'} (P : V ℓ → Type ℓ')
  → (∀ {A} (f : A → V ℓ) → is-prop (P (set A f)))
  → (∀ {A} (f : A → V ℓ) → (∀ x → P (f x)) → P (set A f))
  → ∀ x → P x
V-elim-prop' P pprop pset = V-elim-prop P pprop' pset where abstract
  pprop' : ∀ x → is-prop (P x)
  pprop' = V-elim-prop _ (λ _ → is-prop-is-prop) (λ f _ → pprop f)

Setting this recursion principle aside for a moment, we must define the membership relation between material sets. Here, we must handle the set constructor and the ext constructor, since squash is taken care of by mapping into Prop, which is a set.

On the sets, we define membership exactly as we have for the extensionality constructor.

is-member : ∀ {ℓ} → V ℓ → V ℓ → Prop (lsuc ℓ)
is-member e (set A f) = el ∥ fibre f e ∥ squash
is-member e (ext {A} {B} f g p q i) =
  n-ua {X = el _ squash} {Y = el _ squash} (prop-ext squash squash from to) i where

The extensionality constructor requires that we show a logical equivalence (since we’re mapping into propositions) between the mere fibres of $f$ and $g$ over $e\text{,}$ under the assumption of $p:{\forall }_{a:A}\Vert g^{\ast }(f(a))\Vert$ and $q:{\forall }_{b:B}\Vert f^{\ast }(g(b))\Vert \text{.}$

    from : ∥ fibre f e ∥ → ∥ fibre g e ∥
    to   : ∥ fibre g e ∥ → ∥ fibre f e ∥

In one direction, assume we’re given $w:\Vert f^{\ast }(e)\Vert \text{.}$ Since we’re mapping into a proposition, we may take $w=(a,\alpha )\text{,}$ where $\alpha :f(a)=e\text{.}$ We may then use $p$ to get a fibre of $g$ over $f(a)\text{,}$ i.e., a pair $(b,\beta )\text{,}$ where $\beta :g(b)=f(a)\text{.}$ We wanted to construct a fibre of $g$ over $e\text{:}$ we have $b:B$ and

The other half of the equivalence is symmetric.

    from w = do
      (a , fa=e)  ← w
      (b , gb=fa) ← p a
      pure (b , gb=fa ∙ fa=e)

    to w = do
      (b , gb=e)  ← w
      (a , fa=gb) ← q b
      pure (a , fa=gb ∙ gb=e)

is-member e (squash x y p q i j) =
  n-Type-is-hlevel  (is-member e x) (is-member e y)
    (λ j → is-member e (p j))
    (λ j → is-member e (q j)) i j

Having completed the construction of the membership proposition, we define an instance of Membership for the set-theoretic universe. This will allow us to use the overloaded membership operator to mean membership of material sets, and similarly for non-membership (∉) and subset (⊆).

instance
  Membership-V : ∀ {ℓ} → Membership (V ℓ) (V ℓ) (lsuc ℓ)
  Membership-V = record { _∈_ = λ x y → ⌞ is-member x y ⌟ }

Extensionality🔗

We can now prove our material sets satisfy the axiom of extensionality: if $A$ and $B$ are subsets of each other, they must be the same set. By induction (now using our elimination principle), it suffices to show this when $A=\mathrm{set}(A,f)$ and $B=\mathrm{set}(B,f)$ are literal sets.

extensionality : ∀ {ℓ} (A B : V ℓ) → A ⊆ B → B ⊆ A → A ≡ B
extensionality = wrapper where

By our ext constructor, it will suffice to show that ${\forall }_{a:A}f(a)\in \mathrm{set}(B,g)\text{,}$ together with the symmetric condition on $f\text{.}$

  worker
    : ∀ {A B} (f : A → V _) (g : B → V _)
    → ((a : V _) → a ∈ set A f → a ∈ set B g)
    → ((a : V _) → a ∈ set B g → a ∈ set A f)
    → set A f ≡ set B g
  worker f g f<g g<f = ext f g
    (λ a → f<g (f a) (inc (a , refl)))
    (λ b → g<f (g b) (inc (b , refl)))

We have an assumption of $f(a)\in \mathrm{set}(A,f)\to f(a)\in \mathrm{set}(B,f)\text{,}$ so it suffices to show $f(a)\in \mathrm{set}(A,f)\text{,}$ i.e. to find an $i:A$ such that $f(i)=f(a)\text{.}$ Nothing stops us from taking $i=a\text{!}$

  wrapper =
    V-elim-prop _ (λ A → Π-is-hlevel³  λ _ _ _ → squash _ _) λ {A} f ext B a<b b<a →
      V-elim-prop (λ B → set A f ⊆ B → B ⊆ set A f → (set A f) ≡ B)
      (λ _ → Π-is-hlevel²  λ _ _ → squash _ _)
      (λ g ext' a<b b<a → worker f g a<b b<a)
      B a<b b<a

V-identity-system
  : ∀ {ℓ} → is-identity-system {A = V ℓ}
    (λ A B → A ⊆ B × B ⊆ A) λ a → (λ _ w → w) , λ _ w → w
V-identity-system = set-identity-system (λ x y → hlevel )
  λ { (a , b) → extensionality _ _ a b }

Presentations🔗

Above, we have referred to an inhabitant $\mathrm{set}(A,f):V$ as a literal set. Using our eliminator into propositions, we can establish that every set is merely equal to one of the form $\mathrm{set}(A,f)\text{.}$ In this section, we’ll show that every set is a literal set, without the propositional truncation, by defining a notion of presentation, and showing that each set has exactly one presentation.

Whereas any pair $(A,f)$ could be said to “present” a set — the literal $\mathrm{set}(A,f)$ —, we shall only say “presentation” when $f:A\hookrightarrow V$ is an embedding into the universe of material sets. Note that any presentation has an underlying set $A\text{,}$ which we call the type of members of the associated set. Put explicitly, a presentation for a set $X$ consists of the following data:

record Presentation {ℓ} (X : V ℓ) : Type (lsuc ℓ) where
  field
    members  : Type ℓ
    elem     : members → V ℓ
    embeds   : is-embedding elem

    presents : X ≡ set members elem

We start by showing that presentations are unique. It’ll suffice to do this for a presentation of a literal, material set $(A,f)\text{.}$ Write $g:T\hookrightarrow V$ and $h:S\hookrightarrow V$ for the presentations. Since they both present the same set, by extensionality for material sets, we have equivalences $\Vert g^{\ast }(x)\Vert \simeq \Vert f^{\ast }(x)\Vert \simeq \Vert h^{\ast }(x)\Vert \text{.}$ Since $g$ and $h$ are embeddings, we can drop the truncations around their fibres.

Presentation-is-prop
  : ∀ {ℓ} {A : Type ℓ} (f : A → V ℓ) → is-prop (Presentation (set A f))
Presentation-is-prop {ℓ} {A} f P1 P2 = done where
  open Presentation P1
    renaming (members to T ; elem to g ; embeds to gm ; presents to u)
  open Presentation P2
    renaming (members to S ; elem to h ; embeds to hm ; presents to v)

  v' : set A f ⊆ set S h × set S h ⊆ set A f
  v' = Equiv.from (identity-system-gives-path V-identity-system) v

  u' : set A f ⊆ set T g × set T g ⊆ set A f
  u' = Equiv.from (identity-system-gives-path V-identity-system) u

  eqv : ∀ x → fibre g x ≃ fibre h x
  eqv x = prop-ext (gm x) (hm x)
    (λ fib → ∥-∥-out (hm x) (v' .fst x (u' .snd x (inc fib))))
    (λ fib → ∥-∥-out (gm x) (u' .fst x (v' .snd x (inc fib))))

This pointwise equivalence between fibres extends to an equivalence between types: Since every function $f:E\to B$ induces an equivalence $E\simeq {\sum }_{i:B}{f}^{\ast }(x)\text{,}$ a fibrewise equivalence of functions induces an equivalence between their domains.

  T≃S : T ≃ S
  T≃S =
    T                 ≃⟨ Total-equiv g ⟩≃
    Σ (V ℓ) (fibre g) ≃⟨ Σ-ap-snd eqv ⟩≃
    Σ (V ℓ) (fibre h) ≃⟨ Total-equiv h e⁻¹ ⟩≃
    S                 ≃∎

By construction, the equivalence between domains commutes with the functions we started with. Adjusting this for univalence, we get an identification between the types of members, and over this, an identification between the embeddings into $V\text{.}$ Since the other two components are propositions, that is exactly what we needed to establish uniqueness of presentations.

  g≡h : PathP (λ i → ua T≃S i → V ℓ) g h
  g≡h = ua→ λ a → sym (Equiv.to (eqv _) (a , refl) .snd)

  open Presentation
  done : P1 ≡ P2
  done i .members = ua T≃S i
  done i .elem = g≡h i
  done i .embeds =
    is-prop→pathp (λ i → Π-is-hlevel  λ x → is-prop-is-prop {A = fibre (g≡h i) x}) gm hm i
  done i .presents = is-prop→pathp
    (λ i → V.squash (set A f) (set (ua T≃S i) (g≡h i))) u v i

We now construct a presentation for any given material set. We’re free to assume $X=\mathrm{set}(A,f)$ is a literal set. Factor $f$ through its image as

using image resizing to work around the following slight size issue: the traditional construction of images lives in the largest universe between the domain and codomain of the function. Since $A:{\mathrm{Type}}_{\ell }$ and $V:{\mathrm{Type}}_{\mathrm{lsuc}\ell }\text{,}$ the image of $f$ would live in $\mathrm{lsuc}\ell \text{,}$ which would preclude it from being the type of members of a set.

presentation : ∀ {ℓ} (X : V ℓ) → Presentation X
presentation {ℓ} =
  V-elim-prop' Presentation Presentation-is-prop λ f _ → present f
  where

Since $V$ is a set, by propositional resizing, its identity type can be made to live in the smallest universe, meaning we can construct the image of $f$ as an $\ell \text{-type.}$ The rest of the construction is then straightforward: the type of members is the image of $f\text{,}$ the embedding $\mathrm{im}f\hookrightarrow V$ comes from the image factorisation.

The nontrivial part is showing the logical equivalence between mere fibres of $f$ and mere fibres of $\mathrm{im}f\text{;}$ this follows from the map $A\twoheadrightarrow \mathrm{im}f$ being a surjection.

  present : {A : Type ℓ} (f : A → V ℓ) → Presentation (set A f)
  present {A} f = done where
    module Im = Replacement (is-set→locally-small V.squash) f

    path : set A f ≡ set Im.Image Im.embed
    path = ext _ _ (λ a → inc (Im.inc a , refl)) λ b → do
      (f⁻¹b , p) ← Im.inc-is-surjective b
      pure (f⁻¹b , ap Im.embed p)

    done : Presentation (set A f)
    done .Presentation.members  = Im.Image
    done .Presentation.elem     = Im.embed
    done .Presentation.embeds   = Im.embed-is-embedding
    done .Presentation.presents = path

We wrap this data up in a convenient interface, the module of members of a material set. Other than unpacking the data of the presentation, we also make explicit the equivalence between membership in $X$ and fibres of $X\text{’s}$ presentation.

module Members {ℓ} (X : V ℓ) where
  open Presentation (presentation X) public

  memb : ∀ {x} → x ∈ X ≃ fibre elem x
  memb {x = x} = prop-ext (is-member _ X .is-tr) (embeds _)
    (λ a → ∥-∥-out (embeds _) (subst (x ∈_) presents a))
    (λ a → subst (x ∈_) (sym presents) (inc a))

  module memb {x} = Equiv (memb {x})

  contains : ∀ {i} → elem i ∈ X
  contains = memb.from (_ , refl)

  contains' : ∀ {i x} → x ≡ elem i → x ∈ X
  contains' p = subst (_∈ X) (sym p) contains

Modelling IZF🔗

We now establish that the axioms of intuitionistic ZF hold in our model. These are twofold: first constructing a given set, then showing that this set satisfies its associated axiom.

Before that, let’s get the terminology in order: A material set is an inhabitant of $V\text{,}$ if that was unclear. A class is a family of propositions on $V\text{;}$ by propositional resizing, any class is equivalent to one in $V\to \Omega \text{.}$ We may say that a class $C$ is a material set if we are given $x:V$ with $a\in x\simeq C(a)\text{.}$ Finally, we will denote the presentation of a material set $X$ by $m_X:[X]\hookrightarrow V\text{.}$

Empty set🔗

The empty set is implemented by the empty type. No set is an empty of the empty type, since from the type $x\in \varnothing \text{,}$ one can project a value of $\perp \text{.}$

module _ {ℓ} where
  ∅V : V ℓ
  ∅V = set (Lift ℓ ⊥) (λ ())

  empty-set : (x : V ℓ) → x ∉ ∅V
  empty-set x = ∥-∥-rec (hlevel ) (λ ())

Pairing🔗

The axiom of pairing says that, given material sets $A\text{,}$ $B\text{,}$ we can make a set $\{A,B\}$ whose elements are exactly $A$ and $B\text{.}$ Its implementation is indexed by the type of booleans, mapping (arbitrarily) true to $A\text{,}$ and false to $B\text{.}$

  pair : V ℓ → V ℓ → V ℓ
  pair a b = set (Lift ℓ Bool) λ (lift x) → if x then a else b

The proof that $x\in \{A,B\}\simeq (x=A\vee x=B)$ is essentially the implementation of binary coproducts in terms of arbitrary sum types.

  pairing : ∀ {a b x} → x ∈ pair a b ≃ ∥ (x ≡ a) ⊎ (x ≡ b) ∥
  pairing = prop-ext squash squash
    (∥-∥-rec squash λ where
      (lift true , p) → inc (inl (sym p))
      (lift false , p) → inc (inr (sym p)))
    (∥-∥-rec squash λ where
      (inl x) → inc (lift true , sym x)
      (inr x) → inc (lift false , sym x))

Union🔗

The union of a material set is the first construction in which we employ the presentation machinery. If $F$ is the set we want to union over, let $m_f:[F]\hookrightarrow V$ be its embedding into $V\text{.}$ The “branching factor” of our union $\bigcup F$ is given by a pair $(i,j)$ where $i:[F]$ is a member of $F\text{,}$ and $j:[m_f(i)]$ is a member of $F\text{’s}$ element named by $i\text{.}$

  ⋃V : V ℓ → V ℓ
  ⋃V F =
    set (Σ F.members λ a → Members.members (F.elem a))
      λ { (a , w) → Members.elem (F.elem a) w }
    where module F = Members F

We must show that $x\in \bigcup F$ iff $x$ is an element of an element of $u\text{.}$ This is essentially reassociation modulo the equivalence $x\in F\simeq m_F^{\ast }(x)\text{.}$

  union : ∀ {x F} → x ∈ ⋃V F ≃ ∃ (V ℓ) λ u → x ∈ u × u ∈ F
  union {x} {F} = prop-ext!
    (∥-∥-map λ { ((i , j) , p) →
        Members.elem F i
      , Members.contains' (Members.elem F i) (sym p)
      , Members.contains F
      })

Investigating a proof $x\in \bigcup F\text{,}$ we find that it consists of a value $i:[F]\text{,}$ a value $j:[m_F(i)]\text{,}$ and a proof $p:m_{m_{F(i)}}(j)=x\text{.}$ The member $i$ becomes a material set $m_F(i)\in F\text{,}$ the member $j$ a material set $m_{m_{F(i)}}(j)\in m_F(i)\text{,}$ and the values $(j,p)$ pair into a fibre $m_{m_{F(i)}}^{\ast }(x)\text{,}$ i.e. a proof that $x\in m_F(i)\text{.}$

Conversely, assume we’re given material sets $u\in F$ and $x\in u\text{.}$ The first corresponds to a fibre $m_F^{\ast }(u)\text{,}$ from which we get an index $i:[F]$ and a proof $u=m_F(i)\text{.}$ The latter corresponds to a fibre $m_u^{\ast }(x)\text{,}$ which we can transport to a fibre $m_{m_{F(i)}}^{\ast }(x)\text{,}$ i.e. an index $j:[m_F(i)]$ and a proof $m_{m_{F(i)}}(j)=x\text{.}$

    (∥-∥-map λ { (u , x-u , u-F) →
      let
        s' : fibre _ x
        s' = subst (λ e → fibre (Members.elem e) x)
              (sym (Members.memb.to F u-F .snd))
              (Members.memb.to u x-u)
      in (Members.memb.to F u-F .fst , s' .fst) , s' .snd })

Infinity & the natural numbers🔗

Union is by far the most complicated construction, so let’s take a breather with something simpler: infinity. We begin by defining the binary union of material sets, the map $x\mapsto \{x\}\text{,}$ and the successor operation $x\mapsto x\cup \{x\}\text{.}$

  _∪V_ : V ℓ → V ℓ → V ℓ
  X ∪V Y = ⋃V (pair X Y)

  singleton : V ℓ → V ℓ
  singleton v = set (Lift ℓ ⊤) λ _ → v

  suc-V : V ℓ → V ℓ
  suc-V x = x ∪V singleton x

The material set of natural numbers is built recursively from the type of natural numbers, sending zero to the empty set, and the successor constructor to the successor set.

  ℕV : V ℓ
  ℕV = set (Lift ℓ Nat) λ x → go (lower x) where
    go : Nat → V ℓ
    go zero    = ∅V
    go (suc x) = suc-V (go x)

  zero∈ℕ : ∅V ∈ ℕV
  zero∈ℕ = inc (lift zero , refl)

We can immediately conclude that the material set of natural numbers contains the empty set and is closed under successor, for if $x\in \mathbb{N}\text{,}$ we (merely) have $i:\mathbb{N}$ w/ ${\mathrm{suc}}^i(\varnothing )=x\text{,}$ so ${\mathrm{suc}}^{i+1}(\varnothing )={\mathrm{suc}}_V(x)\text{.}$

  suc∈ℕ : ∀ {X} → X ∈ ℕV → suc-V X ∈ ℕV
  suc∈ℕ = ∥-∥-map λ (lift i , x) → lift (suc i) , ap₂ _∪V_ x (ap singleton x)

Slightly more involved (and, strictly speaking, not necessary), we can prove that the elements of $\mathbb{N}$ are either zero or the successor of another element of $\mathbb{N}\text{.}$ While the axiom of infinity only requires the existence of a set containing $\varnothing$ and closed under successor, our construction immediately provides the smallest such set.

  ℕ-induction
    : ∀ x → x ∈ ℕV ≃ ∥ (x ≡ ∅V) ⊎ (∃ (V ℓ) λ y → y ∈ ℕV × (x ≡ suc-V y)) ∥
  ℕ-induction x = prop-ext squash squash
    (∥-∥-map λ where
      (lift zero , w)    → inl (sym w)
      (lift (suc n) , w) → inr (inc (_ , inc (lift n , refl) , sym w)))
    (λ x → x >>= λ where
      (inl w) → pure (lift zero , sym w)
      (inr w) → do
        (pred , ix , w) ← w
        (ix , x) ← ix
        pure (lift (suc (ix .lower)) , ap₂ _∪V_ x (ap singleton x) ∙ sym w))

Replacement🔗

The replacement axiom is gnarly to state in the language of FOL, but when $V$ is an object in type theory, it takes the following form: Given a map $r:V\to V$ and a material set $x:V\text{,}$ the “image” $r(x)$ is a pure set, with $y\in r(x)$ equivalent to ${\exists }_{z:V}(z\in x\wedge y=rz)\text{.}$

Let $m_x:[x]\hookrightarrow V$ be the presentation of $x\text{;}$ then $\mathrm{set}([x],r\circ m_x)$ is the desired set.

  V-image : (r : V ℓ → V ℓ) (x : V ℓ) → V ℓ
  V-image r x = set (Members.members x) λ i → r (Members.elem x i)

This is a straightforward computation.

  replacement
    : ∀ (r : V ℓ → V ℓ) x i
    → i ∈ V-image r x
    ≃ ∃ (V ℓ) λ z → z ∈ x × (i ≡ r z)
  replacement r x i = prop-ext squash squash
    (∥-∥-map λ { (i , p) → _ , Members.contains x , sym p })
    (∥-∥-map λ { (z , z∈x , i=rz) →
      Members.memb.to x z∈x .fst ,
      ap r (Members.memb.to x z∈x .snd) ∙ sym i=rz })

Separation🔗

In contrast to the predicative theory CZF, in IZF, we have full separation: given any predicate $C:V\to \Omega$ and material set $a:V\text{,}$ we can form the set “$\{a\in A\wedge C(a)\}$”. This is because our ambient type theory has propositional resizing: every proposition, no matter the universe it lives in, is equivalent to a proposition in the smallest universe.

Write $m_a:[a]\hookrightarrow V$ for the presentation of $a\text{,}$ as usual. We define a set by taking $A={\sum }_{i:[a]}C(m_a(i))\text{,}$ with projection function $f=(i,c)\mapsto m_a(i)\text{.}$

  subset : V ℓ → (V ℓ → Ω) → V ℓ
  subset a C = set
    (Σ (Members.members a) λ i → ∣ C (Members.elem a i) ∣)
    (Members.elem a ∘ fst)

By computation, an element of $x\in \mathrm{set}(A,f)$ consists of a fibre $(i,p):m_a^{\ast }(x)$ and a witness that $C$ holds of $m_a(i)\text{.}$ The former corresponds to a proof of $x\in a\text{,}$ and transporting the latter along $p\text{,}$ a proof that $C$ holds of $x\text{.}$

  separation : ∀ a C (x : V ℓ) → (x ∈ subset a C) ≃ (x ∈ a × x ∈ C)
  separation a C x = prop-ext!
    (rec! λ j w p →
      Members.contains' a (sym p) , subst (λ e → ∣ C e ∣) p w )
    (λ { (i∈a , Ci) → inc (
      ( Members.memb.to a i∈a .fst
      , subst (λ e → ∣ C e ∣) (sym (Members.memb.to a i∈a .snd)) Ci)
      , Members.memb.to a i∈a .snd)
      })

Power sets🔗

The axiom of power sets also relies on propositional resizing in the ambient type theory. Let $a$ be a material set with $m_a:[a]\hookrightarrow V$ its presentation — I promise that’s the last time I’ll say this.

To every predicate $p:[a]\to \Omega \text{,}$ we can associate the class $p^{\prime }:V\to \Omega$ given by

which we’ve already established is separable. The reason for this dance is that $V\to \Omega$ is much too large to use as the branching factor of a material set; but $[a]\to \Omega$ is just perfect. By promoting a predicate on $[a]$ to one on V$, we can appeal to separation in our construction of power set.

  predicate→class : ∀ {a} (p : Members.members a → Ω) → V ℓ → Ω
  predicate→class {a = a} p i =
    elΩ (Σ (fibre (Members.elem a) i) λ f → f .fst ∈ p)

  subset-separation
    : ∀ {a} (p : Members.members a → Ω) x
    → x ∈ subset a (predicate→class p)
    ≃ (Σ (fibre (Members.elem a) x) λ f → f .fst ∈ p)

  subset-separation {a} p x =
    x ∈ subset a (predicate→class p)                ≃⟨ separation _ (predicate→class p) x ⟩≃
    x ∈ a × (x ∈ predicate→class p)                 ≃⟨ deduplicate ⟩≃
    Σ (fibre (Members.elem a) x) (λ f → f .fst ∈ p) ≃∎
    where
      hp = Σ-is-hlevel  (Members.embeds a x) λ f → p (f .fst) .is-tr

      deduplicate
        : (x ∈ a × x ∈ predicate→class p)
        ≃ Σ (fibre (Members.elem a) x) (λ f → f .fst ∈ p)
      deduplicate = prop-ext (hlevel ) hp
        (λ { (_ , pcx) → □-rec hp id pcx })
        λ { (f , p) → Members.memb.from a f , inc (f , p) }

  power : V ℓ → V ℓ
  power a = set (Members.members a → Ω) λ p → subset a (predicate→class p)

  power-set : ∀ a i → i ∈ power a ≃ (i ⊆ a)
  power-set a i = done where

This construction is up there with the union in terms of complexity. Let us tackle the simpler direction first: If $i\in a^{\Omega }\text{,}$ we must prove that $i\subseteq a\text{.}$ By definition, the assumption means that $i$ comes from separating a subset, and the axiom of separation guarantees that these are actually subsets.

    p1 : fibre (subset a ∘ predicate→class) i → i ⊆ a
    p1 (pred , p) =
      let
        worker : subset a (predicate→class pred) ⊆ a
        worker a∈sub wit = Equiv.to (separation _ (predicate→class pred) _) wit .fst
      in subst (_⊆ a) p worker

Now the opposite direction. It needs a bit more shuffling of data, but not a lot. Given $i\subseteq a\text{,}$ we’ll prove that the predicate $B(x)=m_a(x)\in i$ corresponds, as a pure subset of $a\text{,}$ to $i\text{.}$ By a consequence of separation, we have an equivalence $(x\in B)\simeq ({\sum }_{(k{,}_{)}}:m_a^{\ast }(x))m_a(k)\in i\text{.}$

    p2 : i ⊆ a → ∥ fibre (subset a ∘ predicate→class) i ∥
    p2 i⊆a = inc (belongs , extensionality _ _ to fro) where
      belongs : Members.members a → Ω
      belongs m = elΩ (Members.elem a m ∈ i)

Given $x\in B\text{,}$ split it into $k:[a]\text{,}$ $m_a(i)=x\text{,}$ $m_a(k)\in i\text{.}$ By transporting this last proof along the middle path, we conclude $x\in i\text{.}$

      to : subset a (predicate→class belongs) ⊆ i
      to e e∈sub = subst (_∈ i)
        (Equiv.to (subset-separation belongs e) e∈sub .fst .snd)
        (□-rec (is-member _ i .is-tr) id
          (Equiv.to (subset-separation belongs e) e∈sub .snd))

In the other direction, we’re given $x\in i\text{.}$ Since $i\subseteq a\text{,}$ we can promote this to $x\in a\text{,}$ which corresponds to a fibre $(k,p):m_a^{\ast }(x)\text{.}$ It remains to show $m_a(k)\in i\text{;}$ but this is equal to $x\in i$ by $p\text{,}$ concluding the argument.

      fro : i ⊆ subset a (predicate→class belongs)
      fro e e∈i = Equiv.from (subset-separation belongs _)
        ( Members.memb.to a (i⊆a _ e∈i)
        , inc (subst (_∈ i) (sym (Members.memb.to a (i⊆a _ e∈i) .snd)) e∈i))

    done = prop-ext! (∥-∥-rec (hlevel ) p1) p2

Set induction🔗

The last thing we’ll prove about $V$ is the principle of $\in \text{-induction,}$ an easy consequence of our eliminator from $V$ into props. If $P$ is a proposition that holds of a material set $a$ as soon as it holds for every $x\in a\text{,}$ then $P$ holds of any material set.

  ∈-induction
    : ∀ {ℓ'} (P : V ℓ → Prop ℓ')
    → ({a : V ℓ} → ({x : V ℓ} → x ∈ a → x ∈ P) → a ∈ P)
    → (x : V ℓ) → x ∈ P
  ∈-induction P ps = V-elim-prop (λ z → z ∈ P) (λ _ → P _ .is-tr) $ λ f i →
    ps λ {x} → rec! λ a p → subst (_∈ P) p (i a)