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
$β-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
$β.$
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
$ββ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)βset(B,g)$
and
$g(b)βset(A,f).$
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,$
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 $set(A,f),$ assuming that it holds for every value of $f,$ 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

##
The implementation of `V-elim-prop`

is entirely
routine.

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,$ under the assumption of $p:β_{a:A}β₯g_{β}(f(a))β₯$ and $q:β_{b:B}β₯f_{β}(g(b))β₯.$

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,Ξ±),$ where $Ξ±:f(a)=e.$ We may then use $p$ to get a fibre of $g$ over $f(a),$ i.e., a pair $(b,Ξ²),$ where $Ξ²:g(b)=f(a).$ We wanted to construct a fibre of $g$ over $e:$ we have $b:B$ and

$g(b)Ξ²f(a)Ξ±e.$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 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`

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 eachother, they must be the same set. By induction (now using our elimination principle), it suffices to show this when $A=set(A,f)$ and $B=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
$β_{a:A}f(a)βset(B,g),$
together with the symmetric condition on
$f.$

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

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!) Ξ» { (a , b) β extensionality _ _ a b }

## Presentationsπ

Above, we have referred to an inhabitant
$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
$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
$set(A,f)$
β, we shall only say βpresentationβ when
$f:Aβͺ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:

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βͺV$ and $h:SβͺV$ for the presentations. Since they both present the same set, by extensionality for material sets, we have equivalences $β₯g_{β}(x)β₯ββ₯f_{β}(x)β₯ββ₯h_{β}(x)β₯.$ 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 β β₯-β₯-proj (hm x) (v' .fst x (u' .snd x (inc fib)))) (Ξ» fib β β₯-β₯-proj (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βB$ induces an equivalence $Eββ_{i:B}f_{β}(x),$ 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.$ 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 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=set(A,f)$ is a literal set. Factor $f$ through its image as

$Aβimfβͺ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:Type_{β}$ and $V:Type_{lsucΒβ},$ the image of $f$ would live in $lsucΒβ,$ 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 $β-type.$ The rest of the construction is then straightforward: the type of members is the image of $f,$ the embedding $imfβͺV$ comes from the image factorisation.

The nontrivial part is showing the logical equivalence between mere fibres of $f$ and mere fibres of $imf;$ this follows from the map $Aβimf$ 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β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 β β₯-β₯-proj (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βΞ©.$
We may say that a class
$C$
**is a material set** if we are given
$x:V$
with
$aβxβC(a).$
Finally, we will denote the presentation of a material set
$X$
by
$m_{X}:[X]βͺ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ββ,$ one can project a value of $β₯.$

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`

to
$A,$
and `false`

to
$B.$

pair : V β β V β β V β pair a b = set (Lift β Bool) Ξ» (lift x) β if x then a else b

The proof that $xβ{A,B}β(x=Aβ¨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]βͺV$ be its embedding into $V.$ The βbranching factorβ of our union $β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.$

β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ββF$ iff $x$ is an element of an element of $u.$ This is essentially reassociation modulo the equivalence $xβFβm_{F}(x).$

union : β {x F} β x β βV F β β (V β) Ξ» u β x β u Γ u β F union {x} {F} = prop-ext hlevel! squash (β₯-β₯-map Ξ» { ((i , j) , p) β Members.elem F i , Members.contains' (Members.elem F i) (sym p) , Members.contains F })

Investigating a proof $xββ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)βF,$ the member $j$ a material set $m_{m_{F(i)}}(j)βm_{F}(i),$ and the values $(j,p)$ pair into a fibre $m_{m_{F(i)}}(x),$ i.e.Β a proof that $xβm_{F}(i).$

Conversely, assume weβre given material sets $uβF$ and $xβ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.$

(β₯-β₯-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β¦{x},$ and the successor operation $xβ¦xβͺ{x}.$

_βͺ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 (Lift.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βN,$ we (merely) have $i:N$ w/ $suc_{i}(β)=x,$ so $suc_{i+1}(β)=suc_{V}(x).$

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
$N$
are either zero or the successor of another element of
$N.$
While the axiom of infinity only requires the existence of *a*
set containing
$β$
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 .Lift.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βV$ and a material set $x:V,$ the βimageβ $r(x)$ is a pure set, with $yβr(x)$ equivalent to $β_{z:V}(zβxβ§y=rz).$

Let $m_{x}:[x]βͺV$ be the presentation of $x;$ then $set([x],rβ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βΞ©$
and material set
$a:V,$
we can form the set
β${aβAβ§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]βͺV$ for the presentation of $a,$ as usual. We define a set by taking $A=β_{i:[a]}C(m_{a}(i)),$ with projection function $f=(i,c)β¦m_{a}(i).$

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β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βa,$ and transporting the latter along $p,$ a proof that $C$ holds of $x.$

separation : β a C (x : V β) β (x β subset a C) β (x β a Γ x β C) separation a C x = prop-ext squash hlevel! (β₯-β₯-rec hlevel! Ξ» { ((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]βͺV$ its presentation β I promise thatβs the last time Iβll say this.

To every predicate $p:[a]βΞ©,$ we can associate the class $p_{β²}:VβΞ©$ given by

$xβ¦(i,_{)}:m_{a}(x)ββp(i),$which weβve already established is separable. The reason for this dance is that $VβΞ©$ is much too large to use as the branching factor of a material set; but $[a]βΞ©$ 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 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! hp (Ξ» { (_ , pcx) β out! {pa = hp} 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βa_{Ξ©},$
we must prove that
$iβa.$
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βa,$ weβll prove that the predicate $B(x)=m_{a}(x)βi$ corresponds, as a pure subset of $a,$ to $i.$ By a consequence of separation, we have an equivalence $(xβB)β(β_{(k,_{)}}:m_{a}(x))m_{a}(k)βi.$

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βB,$ split it into $k:[a],$ $m_{a}(i)=x,$ $m_{a}(k)βi.$ By transporting this last proof along the middle path, we conclude $xβi.$

to : subset a (predicateβclass belongs) β i to e eβsub = subst (_β i) (Equiv.to (subset-separation belongs e) eβsub .fst .snd) (out! {pa = is-member _ i .is-tr} (Equiv.to (subset-separation belongs e) eβsub .snd))

In the other direction, weβre given $xβi.$ Since $iβa,$ we can promote this to $xβa,$ which corresponds to a fibre $(k,p):m_{a}(x).$ It remains to show $m_{a}(k)βi;$ but this is equal to $xβi$ by $p,$ 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 squash hlevel! (β₯-β₯-rec hlevel! p1) p2

## Set inductionπ

The last thing weβll prove about $V$ is the principle of $β-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βa,$ 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)