{-# 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

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 successor universe.

The mere fibres in the extensionality constructor, as weβll see in a bit, are exactly the normal forms of the propositions and You should think of ext as an instance of the axiom of extensionality, specialised for values which are βexplicitβ sets: If every element is somewhere in and every is somewhere in then and 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 holds of assuming that it holds for every value of 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 and over under the assumption of and

    from : β₯ fibre f e β₯ β β₯ fibre g e β₯
to   : β₯ fibre g e β₯ β β₯ fibre f e β₯


In one direction, assume weβre given Since weβre mapping into a proposition, we may take where We may then use to get a fibre of over i.e., a pair where We wanted to construct a fibre of over we have 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 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 and are subsets of eachother, they must be the same set. By induction (now using our elimination principle), it suffices to show this when and 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 together with the symmetric condition on

  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 so it suffices to show i.e. to find an such that Nothing stops us from taking

  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 as a literal set. Using our eliminator into propositions, we can establish that every set is merely equal to one of the form 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 could be said to βpresentβ a set β the literal β, we shall only say βpresentationβ when is an embedding into the universe of material sets. Note that any presentation has an underlying set which we call the type of members of the associated set. Put explicitly, a presentation for a set 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 Write and for the presentations. Since they both present the same set, by extensionality for material sets, we have equivalences Since and 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 induces an equivalence a fibrewise equivalence of functions induces an equivalence between their domains.

  TβS : T β S
TβS =
Ξ£ (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 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 is a literal set. Factor 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 and the image of would live in 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 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 as an The rest of the construction is then straightforward: the type of members is the image of the embedding comes from the image factorisation.

The nontrivial part is showing the logical equivalence between mere fibres of and mere fibres of this follows from the map 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 and fibres of 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 if that was unclear. A class is a family of propositions on by propositional resizing, any class is equivalent to one in We may say that a class is a material set if we are given with Finally, we will denote the presentation of a material set by

## Empty setπ

The empty set is implemented by the empty type. No set is an empty of the empty type, since from the type 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 we can make a set whose elements are exactly and Its implementation is indexed by the type of booleans, mapping (arbitrarily) true to and false to

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


The proof that 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 is the set we want to union over, let be its embedding into The βbranching factorβ of our union is given by a pair where is a member of and is a member of element named by

  β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 iff is an element of an element of This is essentially reassociation modulo the equivalence

  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 we find that it consists of a value a value and a proof The member becomes a material set the member a material set and the values pair into a fibre i.e.Β a proof that

Conversely, assume weβre given material sets and The first corresponds to a fibre from which we get an index and a proof The latter corresponds to a fibre which we can transport to a fibre i.e.Β an index and a proof

    (β₯-β₯-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 and the successor operation

  _βͺ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 we (merely) have w/ so

  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 are either zero or the successor of another element of 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 is an object in type theory, it takes the following form: Given a map and a material set the βimageβ is a pure set, with equivalent to

Let be the presentation of then 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 and material set we can form the set ββ. 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 for the presentation of as usual. We define a set by taking with projection function

  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 consists of a fibre and a witness that holds of The former corresponds to a proof of and transporting the latter along a proof that holds of

  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 be a material set with its presentation β I promise thatβs the last time Iβll say this.

To every predicate we can associate the class given by

which weβve already established is separable. The reason for this dance is that is much too large to use as the branching factor of a material set; but is just perfect. By promoting a predicate on 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 1) 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 we must prove that By definition, the assumption means that 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 weβll prove that the predicate corresponds, as a pure subset of to By a consequence of separation, we have an equivalence  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 split it into By transporting this last proof along the middle path, we conclude  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 Since we can promote this to which corresponds to a fibre It remains to show but this is equal to by 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 1) p1) p2  ## Set inductionπ The last thing weβll prove about is the principle of an easy consequence of our eliminator from into props. If is a proposition that holds of a material set as soon as it holds for every then 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)