{-# 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 =
    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 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 (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 .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)