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

open import Data.Sum.Base
open import Data.Image
open import Data.Bool
```
-->

```agda
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`{.Agda} (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$-induction.

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

```agda
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`{.Agda} resembles a [W-type]: the constructor `set`{.Agda}
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$.
Of course, if we could take the supremum of `V`{.Agda}-many sets, we
could reproduce [Russell's paradox], so Agda rightly forces us to put V
in $\ell$'s successor universe.

[W-type]: Data.Wellfounded.W.html
[Russell's paradox]: 1Lab.Counterexamples.Russell.html

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
\rm{set}(B,g)$ and $g(b) \in \rm{set}(A,f)$. You should think of
`ext`{.Agda} as an instance of the axiom of extensionality, specialised
for values which are "explicit" sets: If every element $f(a)$ is
somewhere in $g$, and every $g(b)$ is somewhere in $f$, 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 $\rm{set}(A, f)$, assuming that it holds
for every value of $f$, then it holds for any set.

```agda
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
```

<details>
<summary>
The implementation of `V-elim-prop`{.Agda} is entirely routine.
</summary>

```agda
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
```

</details>

<!--
```agda
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`{.Agda} constructor and the `ext`{.Agda} constructor, since
`squash`{.Agda} is taken care of by mapping into `Prop`{.Agda}, which is
a set.

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

```agda
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$, under the assumption of
$p : \forall_{a : A} \| g^*(f(a)) \|$ and
$q : \forall_{b : B} \| f^*(g(b)) \|$.

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

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

$$
g(b) \xlongequal{\beta} f(a) \xlongequal{\alpha} e
$$.

The other half of the equivalence is symmetric.

```agda
    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)
```

<!--
```agda
is-member e (squash x y p q i j) =
  n-Type-is-hlevel 1 (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`{.Agda} 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 (`⊆`).

```agda
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 eachother, they must be the same set. By
induction (now using our elimination principle), it suffices to show
this when $A = \rm{set}(A,f)$ and $B = \rm{set}(B,f)$ are literal sets.

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

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

```agda
  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 \rm{set}(A,f) \to f(a) \in
\rm{set}(B,f)$, so it suffices to show $f(a) \in \rm{set}(A, f)$, i.e.
to find an $i : A$ such that $f(i) = f(a)$. Nothing stops us from taking
$i = a$!

<!--
```agda
  wrapper =
    V-elim-prop _ (λ A → Π-is-hlevel³ 1 λ _ _ _ → 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² 1 λ _ _ → 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 1)
  λ { (a , b) → extensionality _ _ a b }
```
-->

## Presentations

Above, we have referred to an inhabitant $\rm{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 $\rm{set}(A, f)$.
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 $\rm{set}(A, f)$ ---, we shall only say "presentation" when $f :
A \mono V$ is an [[embedding]] into the universe of material sets. Note
that any presentation has an underlying _set_ $A$, which we call the
**type of members** of the associated set. Put explicitly, a
presentation for a set $X$ consists of the following data:

```agda
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)$. Write $g : T \mono V$
and $h : S \mono V$ for the presentations. Since they both present the
same set, by extensionality for material sets, we have equivalences $\|
g^*(x) \| \simeq \| f^*(x) \| \simeq \| h^*(x) \|$. Since $g$
and $h$ are embeddings, we can drop the truncations around their fibres.

<!--
```agda
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)
```
-->

```agda
  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^*(x)$, a fibrewise equivalence of functions
induces an equivalence between their domains.

```agda
  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$. Since the other two
components are propositions, that is exactly what we needed to establish
uniqueness of presentations.

```agda
  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 1 λ 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 = \rm{set}(A, f)$ is a literal set. Factor $f$ through its
[[image]] as

$$
A \epi \im f \mono V
$$,

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 : \ty_\ell$
and $V : \ty_{\rm{lsuc}\ \ell}$, the image of $f$ would live in
$\rm{lsuc}\ \ell$, which would preclude it from being the type of
members of a set.

[image resizing]: Data.Image.html

```agda
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$-type. The rest of the construction is then
straightforward: the type of members is the image of $f$, the embedding
$\im f \mono V$ comes from the image factorisation.

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

```agda
  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$'s presentation.

```agda
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$, if that was unclear. A **class** is a family of
propositions on $V$; by propositional resizing, any class is equivalent
to one in $V \to \Omega$. We may say that a class $C$ **is a material
set** if we are given $x : V$ with $a \in x \simeq C(a)$. Finally, we
will denote the presentation of a material set $X$ by $m_X : [X] \mono
V$.

## 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$, one can project
a value of $\bot$.

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

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

## Pairing

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

```agda
  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 \lor x = B)$ is essentially
the implementation of binary coproducts in terms of arbitrary sum types.

```agda
  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] \mono V$ be its embedding into $V$. The "branching factor" of
our union $\bigcup F$ is given by a pair $(i, j)$ where $i : [F]$ is a
member of $F$, and $j : [m_f(i)]$ is a member of $F$'s element named by
$i$.

```agda
  ⋃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$. This is essentially reassociation modulo the equivalence $x \in
F \simeq m_F^*(x)$.

```agda
  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$, we find that it consists of a
value $i : [F]$, a value $j : [m_F(i)]$, and a proof $p :
m_{m_{F(i)}}(j) = x$. The member $i$ becomes a material set $m_F(i) \in F$,
the member $j$ a material set $m_{m_{F(i)}}(j) \in m_F(i)$, and the values
$(j, p)$ pair into a fibre $m_{m_{F(i)}}^*(x)$, i.e. a proof that $x \in
m_F(i)$.

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

```agda
    (∥-∥-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\}$, and the successor
operation $x \mapsto x \cup \{x\}$.

```agda
  _∪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.

```agda
  ℕ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
\NN$, we (merely) have $i : \NN$ w/ $\rm{suc}^i(\varnothing) = x$, so
$\rm{suc}^{i + 1}(\varnothing) = \rm{suc}_V(x)$.

```agda
  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 $\NN$ are either zero or the successor of
another element of $\NN$. 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.

```agda
  ℕ-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$, the "image" $r(x)$ is a pure
set, with $y \in r(x)$ equivalent to $\exists_{z : V} (z \in x \land y
= r z)$.

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

```agda
  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.

```agda
  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$, we can form the set "$\{ a \in A \land 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] \mono V$ for the presentation of $a$, as usual. We
define a set by taking $A = \sum_{i : [a]} C(m_a(i))$, with projection
function $f = (i, c) \mapsto m_a(i)$.

```agda
  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 \rm{set}(A,f)$ consists of a fibre
$(i, p) : m_a^*(x)$ and a witness that $C$ holds of $m_a(i)$. The former
corresponds to a proof of $x \in a$, and transporting the latter along
$p$, a proof that $C$ holds of $x$.

```agda
  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] \mono V$ its
presentation --- I promise that's the last time I'll say this.

To every predicate $p : [a] \to \Omega$, we can associate the class
$p' : V \to \Omega$ given by

$$
x \mapsto \sum_{(i, _) : m_a^*(x)} p(i)
$$,

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.

```agda
  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)
```

<!--
```agda
  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 1 (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 1) hp
        (λ { (_ , pcx) → □-rec hp id pcx })
        λ { (f , p) → Members.memb.from a f , inc (f , p) }
```
-->

```agda
  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$, we must
prove that $i \sube a$. By definition, the assumption means that $i$
comes from separating a `subset`{.Agda}, and the axiom of separation
guarantees that these are actually subsets.

```agda
    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 \sube a$, we'll prove that the predicate $B(x) =
m_a(x) \in i$ corresponds, as a pure subset of $a$, to $i$. By a
consequence of separation, we have an equivalence
$(x \in B) \simeq (\sum_{(k, _)} : m_a^*(x)) m_a(k) \in i$.

```agda
    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$, split it into $k : [a]$, $m_a(i) = x$, $m_a(k) \in i$.
By transporting this last proof along the middle path, we conclude $x
\in i$.

```agda
      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$. Since $i \sube a$, we can
promote this to $x \in a$, which corresponds to a fibre $(k , p) :
m_a^*(x)$. It remains to show $m_a(k) \in i$; but this is equal to $x
\in i$ by $p$, concluding the argument.

```agda
      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 1) p1) p2
```

## Set induction

The last thing we'll prove about $V$ is the principle of
$\in$-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$, then $P$ holds of any material set.

```agda
  ∈-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)
```
