module Data.Set.Material where

The cumulative hierarchy of iterative sets🔗

Following Gylterud and Stenholm (2024), we define the cumulative hierarchy of material sets as a subtype of a W-type, giving us better definitional control of the type of members of a set than is possible with the higher-inductive construction. The type of sets we construct here will then be useful as a set-truncated universe of sets, since (unlike an inductive-recursive universe), it can be populated post-hoc with a definitional encoding for any type which injects into a material set.

Throughout this page, we will occasionally need to explicitly refer to universe levels, but at most one; we will reserve the cursive for this. We start by defining the type of “multisets” as a W-type with labels given by an arbitrary type and where the branching factor for the constructor labelled is just itself.

private
  V' : (l : Level)  Type (lsuc l)
  V' l = W (Type l)  x  x)

We have a good understanding of paths in W-types, but for this specific construction, univalence lets us do better: the type of identities between multisets is given by the fibrewise equivalences between their subtrees.

  veq : V'   V'   Type _
  veq w w' = (x : V' _)  fibre (subtree w) x  fibre (subtree w') x

For a multiset we think of the fibres of its subtree function as a membership correspondence, where records “the ways for to belong to ”. At this stage, there may be multiple such ways, but we can still think of veq as saying that and agree on their containment of all other sets. The theorem that veq is the identity family for multisets is then a sort of extensionality principle.

The proof that veq is the identity family for V' is a lengthy, but uninspiring, calculation.
  abstract
    path≃veq : (x y : V' )  (x  y)  veq x y
    path≃veq (sup x f) (sup y g) =
      sup x f  sup y g
        ≃⟨ WPath.Path≃Code (sup x f) (sup y g) 
      Σ[ p  x  y ] (∀ {x y}  PathP  i  p i) x y  WPath.Code (f x) (g y))
        ≃˘⟨ Σ-ap-fst (ua , univalence⁻¹) ≃˘
      Σ[ e  x  y ] (∀ {x y}  PathP  i  ua e i) x y  WPath.Code (f x) (g y))
        ≃⟨ Σ-ap-snd  e  Π'-ap-cod λ x  Π'-ap-cod λ y  Π-ap-dom (ua-pathp≃path _)) 
      Σ[ e  x  y ] (∀ {x y}  e .fst x  y  WPath.Code (f x) (g y))
        ≃⟨ Σ-ap-snd  e  Π'-ap-cod λ x  Π'-ap-cod λ y  Π-ap-cod λ p  Equiv.inverse (WPath.Path≃Code (f x) (g y))) 
      Σ[ e  x  y ] (∀ {x y}  e .fst x  y  f x  g y)
        ≃˘⟨ Σ-ap-snd  e  Π²-impl≃) ≃˘
      Σ[ e  x  y ] (∀ x y  e .fst x  y  f x  g y)
        ≃˘⟨ Σ-ap-snd  e  Π-ap-cod λ x  curry≃) ≃˘
      Σ[ e  x  y ] (∀ x  ((y , _) : Σ[ y  y ] (e .fst x  y))  f x  g y)
        ≃⟨ Σ-ap-snd  e  Π-ap-cod λ x  Π-contr-eqv (hlevel 0)) 
      Σ[ e  x  y ] (∀ x  f x  g (e .fst x))
        ≃⟨ equiv-over≃fibrewise-equiv f g 
      veq (sup x f) (sup y g)
        ≃∎

If we are to carve out a subtype of V' which is a set, then, it will suffice to find one for which the membership correspondence is valued in propositions, i.e. is a relation. The fibrewise-propositional functions are called embeddings, so it suffices to consider the subtype V of V' consisting of the multisets which are everywhere embeddings: the iterative embeddings.

is-iterative-embedding : V'   Type (lsuc )
is-iterative-embedding (sup x f) = is-embedding f × (∀ y  is-iterative-embedding (f y))

By induction, being an iterative embedding is a proposition, because it pairs a proposition (the outermost subtree-assigning function is an embedding) with a product of propositions (each subtree is an iterative embedding).

We can then prove that V is a set, since veq for iterative embeddings is a proposition.

instance abstract
  H-Level-V :  { n}  H-Level (V ) (2 + n)
  H-Level-V = basic-instance 2 $ retract→is-hlevel 2
    (uncurry V.constructor)  v  v .tree , v .uniq)  x  ap-set refl)
    λ (x , α) (y , β)  Equiv→is-hlevel 1 (Equiv.inverse Σ-pathp≃)
      (Σ-is-hlevel 1 (Equiv→is-hlevel 1 (path≃veq x y)
      (Π-is-hlevel 1  v  ≃-is-hlevel 1 (prj _ α _) (prj _ β _))))
      λ _  hlevel 1)
abstract
  tree-is-embedding : is-embedding {A = V } V.tree
  tree-is-embedding x (s , α) (t , β) = Σ-prop-path
     y  Equiv→is-hlevel 1 (path≃veq _ _) (Π-is-hlevel 1 λ z 
      ≃-is-hlevelˡ 0 (prj _ (y .uniq) _)))
    (ap-set (α  sym β))

-- We redefine these so we can be precise about the hlevel-projection
-- instance for El on V (we need an explicit matching function instead
-- of using a with-abstraction to refer to it by name) instead of
-- thinking that *every* label must be a set because it comes from V
-- and then having a really mysterious error message.
--
-- They can't be private because they're used in the Automation module.
--
-- It's also defined for an entire S : V with a named local helper
-- (instead of for S .tree : V') so we can write a DISPLAY form to print
-- v-label as El.
--
-- It's important that S is bound in the lhs of v-label
-- (thus again in the λ-lifting of v-label.impl) so the normal form of
-- v-label looks like
--
--    v-label.impl {ℓ} S (S .tree)
-- whence we can recover ℓ and S with a display form.

v-label : V   Type 
v-label { = } S = impl (S .tree) module v-label where
  impl : V'   Type 
  impl (sup x f) = x

pattern v-label-args S = _ h∷ S v∷ def (quote tree) _ v∷ []

private
  v-subtree : (x : V )  v-label x  V' 
  v-subtree S with S .tree
  ... | sup x f = f

instance
  Underlying-V : Underlying (V )
  Underlying-V = record { ⌞_⌟ = λ v  v-label v }

_∈ⱽ_ : (x y : V )  Type (lsuc )
x ∈ⱽ y with y .tree
... | sup A f = fibre f (x .tree)

instance
  Membership-V : Membership (V ) (V ) _
  Membership-V = record { _∈_ = _∈ⱽ_ }

We can define a “constructor” for V which takes the supremum of an embedding into V. We could then go on to show that supⱽ actually does generate V, i.e. exhibit an induction principle saying that covering supⱽ suffices to cover all of V, but this will not be necessary.

supⱽ : (T : Type ) (f : T  V )  V 
{-# INLINE supⱽ #-}
supⱽ T f = record
  { tree = sup T  x  f .fst x .tree)
  ; uniq = ∘-is-embedding tree-is-embedding (f .snd) , λ y  f .fst y .uniq
  }
When formalising constructions with material sets, it will be convenient to have syntax for supⱽ where the function is only assumed to be an injection (which suffices since V is a set), and which lets us specify this data separately from the function.
-- Efficiency note: because composing embeddings generates pretty
-- horrible stuff, this module *needs* the function above (and mkⱽ
-- below) to be INLINE, so the normal forms of codes in V are compact.

record mkV  : Type (lsuc ) where
  field
    Elt : Type 
    idx : Elt  V 
    inj : injective idx

  mkⱽ : V 
  {-# INLINE mkⱽ #-}
  mkⱽ = supⱽ Elt (idx , injective→is-embedding! inj)

open mkV public

We will, however, define a principle of “”, saying that, if you can show under the assumption that for every then holds of arbitrary sets — in order words, that the relation is well-founded. As usual, this implies that the membership relation is irreflexive.

∈-induction
  :  {ℓ'} (P : V   Type ℓ')
   ({a : V }  ({x : V }  x  a  x  P)  a  P)
   (x : V )  x  P
∈-induction { = } P pmem S = subst P (ap-set refl) (go (S .tree) (S .uniq)) where
  go : (x : V' ) (iie : is-iterative-embedding x)  P (set x iie)
  go (sup x f) (fe , su) = pmem λ {y} (j , α) 
    subst P (ap-set α) (go (f j) (su j))

∈-irrefl : (x : V )  x  x  
∈-irrefl = ∈-induction _ λ {a} ind a∈a  ind a∈a a∈a

Finally, we can also define pattern-matching functions to project the “label” and “subtree” from a material set. The subtree function _!_ is, by construction, an embedding (hence, an injection), and we can pair it with that proof to obtain for each material set an embedding lookup from its type of members back into the cumulative hierarchy.

_!_ : (S : V )   S   V 
S ! x with S .tree | S .uniq
... | sup A f | _ , φ = set (f x) (φ x)

!-inj : (S : V ) {x y :  S }  S ! x  S ! y  x  y
!-inj S α with S .tree | S .uniq
... | sup x f | φ , _ = ap fst (φ _ (_ , ap tree α) (_ , refl))

lookup : (S : V )   S   V 
lookup S .fst = S !_
lookup S .snd = injective→is-embedding! (!-inj S)

as a universe🔗

The “type-of-members” projection from allows us to think of it as a universe of h-sets, though one which, unlike the built-in universes of Agda, requires us to explicitly decode an element of the universe into a type.1 To make this interpretation explicit, we will sometimes refer to the type-of-members projection by El, which is the traditional name for the decoding family of a Tarski universe.

Elⱽ : V   Type 
Elⱽ V =  V 

abstract
  El-is-set : (x : V )  is-set (Elⱽ x)
  El-is-set x = embedding→is-hlevel 1 (lookup x .snd) (hlevel 2)

From this perspective, we think of constructing a material set with a specific type of members as showing that V is closed under a specific type-theoretic connective. To this end, the following “realignment” principle will be useful: it says that if is a material set and is an injection, we can obtain a material set which definitionally decodes to

realignⱽ : (x : V ) {T : Type } (e : T  Elⱽ x)  injective e  V 
{-# INLINE realignⱽ #-}
realignⱽ x {T} f α = mkⱽ λ where
  .Elt    T
  .idx i  x ! f i
  .inj i  α (!-inj x i)

_ :  {x : V } {T} {e : T  Elⱽ x} {p : injective e}
   Elⱽ (realignⱽ x e p)  T
_ = refl

Constructing material sets🔗

Since the empty function is an embedding, the empty type has a code in V, which is ‘the empty set’ — it has no members.

∅ⱽ : V 
∅ⱽ = supⱽ (Lift _ ) ((λ ()) ,  { _ (() , _) }))

Similarly, since any function from the unit type is injective, if you already have a material set you can construct the set Note that this is itself an embedding into V.

oneⱽ : V   V 
oneⱽ v = mkⱽ λ where
  .Elt    Lift _ 
  .idx _  v
  .inj _  refl

one-inj : {x y : V }  oneⱽ x  oneⱽ y  x  y
one-inj x = ap-set (ap₂  e y  (e ! y) .tree) x (to-pathp refl))

Moreover, we can prove that is distinct from by showing that identifying them would contradict irreflexivity of the

x≠[x] : (x : V )  x  oneⱽ x  
x≠[x] x p = ∈-irrefl x (subst (x ∈_) (sym p) (lift tt , refl))

We can’t, in general, write a function that puts two arguments into a material set: if you fed it the same set twice, it would end up constructing “”, and we can not show that the member function for this pathological example is an injection. However, we can write a function that packs two distinct values into a material set — forming under the assumption that

twoⱽ : (x y : V )  x  y  V 
twoⱽ x y d = mkⱽ λ where
  .Elt  Lift _ Bool
  .idx (lift true)   x
  .idx (lift false)  y

  .inj {lift true}  {lift true}  p  refl
  .inj {lift true}  {lift false} p  absurd (d p)
  .inj {lift false} {lift true}  p  absurd (d (sym p))
  .inj {lift false} {lift false} p  refl
We will need later that two is almost an injection, i.e. that if you have then implies and
two-inj
  : {x₀ x₁ y₀ y₁ : V } {p : x₀  y₀} {q : x₁  y₁} (r : x₁  y₀)
   twoⱽ x₀ y₀ p  twoⱽ x₁ y₁ q
   (x₀  x₁) × (y₀  y₁)
two-inj {x₀ = x₀} {x₁} {y₀} {y₁} {d₀} {d₁} ah α = done where
  p : Lift _ Bool  Lift _ Bool
  p = ap Elⱽ α

  q : {a b : Lift _ Bool}  transport p a  b
     subtree (twoⱽ x₀ y₀ d₀ .tree) a  subtree (twoⱽ x₁ y₁ d₁ .tree) b
  q a i = v-subtree (α i) (to-pathp {A = λ i  p i} a i)

  rem₁ :  x  transport p (lift x)  lift x
  rem₁ x =
    let
      e = ≃-ap Lift-≃ Lift-≃ .fst (path→equiv p)

      β : transport p (lift false) .lower  false
      β = dec→dne λ pt≠t  ah (sym (ap-set (q (ap lift (ne→is-not pt≠t)))))
    in ap lift $ bool-equiv-id e _ x β

  abstract
    done : (x₀  x₁) × (y₀  y₁)
    done = ap-set (q (rem₁ true)) , ap-set (q (rem₁ false))

We can construct a successor operation on material sets, too, such that if or This is a legitimate construction because is distinct from all of its members.

sucⱽ : V   V 
sucⱽ x = mkⱽ λ where
  .Elt    Elⱽ x

  .idx (inl tt)  x
  .idx (inr j)   x ! j

  .inj {inl _} {inl _} p  refl
  .inj {inl _} {inr _} p  absurd (∈-irrefl x (lookup→member x (sym p)))
  .inj {inr _} {inl _} p  absurd (∈-irrefl x (lookup→member x p))
  .inj {inr _} {inr _} p  ap inr (!-inj x p)

By iterating successors of the empty set, we can accurately encode the natural numbers. We note that the type of members of encoden at is equivalent to and, since Fin is also injective, we can show encoden is itself injective.

Natⱽ : V lzero
Natⱽ = mkⱽ (mkV.constructor _ encoden encoden-inj) where
  encoden : Nat  V 
  encoden zero    = ∅ⱽ
  encoden (suc x) = sucⱽ (encoden x)

  encoden-inj :  {}  injective (encoden {})
  encoden-inj {} p = Fin-injective (Equiv.inverse (lemma _) ∙e path→equiv (ap Elⱽ p) ∙e lemma _) where
    lemma :  n  Elⱽ (encoden {} n)  Fin n
    lemma zero    =  ()) , record { is-eqv = λ x  absurd (Fin-absurd x) }
    lemma (suc n) = ⊎-ap id≃ (lemma n) ∙e Equiv.inverse Finite-successor

Pairing🔗

Using the constructors ∅ⱽ, oneⱽ and twoⱽ, we can construct the ordered pairing of any two material sets by wrapping them in sufficient brackets to make them distinct. Specifically, we code for as

This construction requires a few annoying lemmas distinguishing ∅ⱽ, oneⱽ and twoⱽ, which are all by how we can distinguish their types of members.
abstract
  one≠∅ : {x : V }  oneⱽ x  ∅ⱽ
  one≠∅ p = subst ⌞_⌟ (ap Elⱽ p) (lift tt) .lower

  one≠two :  {x y z : V } {p}  oneⱽ x  twoⱽ y z p
  one≠two p = true≠false (ap lower (subst is-prop (ap Elⱽ p) (hlevel 1) _ _))
pair : V   V   V 
pair a b =
  twoⱽ
    (twoⱽ (oneⱽ a) ∅ⱽ one≠∅)
    (oneⱽ (oneⱽ b))
  (one≠two  sym)

The absurd number of brackets is required to meet the side-condition for two-inj, which lets us show that this is an injection from into

abstract
  pair-inj
    : {x x' y y' : V }
     pair x y  pair x' y'  Path (V  × V ) (x , y) (x' , y')
  pair-inj α =
    let
      (p1 , p2) = two-inj (one≠two  sym) α
      (p1' , _) = two-inj one≠∅ p1
    in one-inj p1' ,ₚ one-inj (one-inj p2)

Using this ordered pairing structure, we can show that is closed under dependent sum: if is a and is a family of over the type injects into by sending each to The proof that this is an injection is slightly complicated by the type dependency, but it’s not unmanageable.

Σⱽ : (X : V ) (Y : Elⱽ X  V )  V 
Σⱽ x y = mkⱽ λ where
  .Elt          Σ[ i  Elⱽ x ] Elⱽ (y i)
  .idx (a , b)  pair (x ! a) (y a ! b)
We leave the proof that this is an injection in this <details> block.
  .inj {a , b} {a' , b'} α 
    let
      p1 , p2 = Σ-pathp.from (pair-inj α)

      p : a  a'
      p = !-inj x p1

      q : (y a ! b)  (y a ! subst (Elⱽ  y) (sym p) b')
      q = subst₂  e b'  (y a ! b)  (y e ! b')) (sym p) (to-pathp refl) p2
    in Σ-pathp (!-inj x p1) (to-pathp⁻ (!-inj (y a) q))
_ :  {A : V } {B}  Elⱽ (Σⱽ A B)  (Σ[ a  Elⱽ A ] Elⱽ (B a))
_ = refl

Separation and power sets🔗

Under our assumption of propositional resizing, we can show that any property of a is separable: we have a set whose elements are precisely the elements of that satisfy

subsetⱽ : (x : V )  (Elⱽ x  Ω)  V 
subsetⱽ v f = mkⱽ λ where
  .Elt          Σ[ i  v ] (i  f)
  .idx (x , _)  v ! x
  .inj α        Σ-prop-path! (!-inj v α)

More importantly, if we fix then we can recover the proposition we started with as “”. This shows that, if is held fixed, then subsetⱽ is an injection of into and the entire power set of has a

subsetⱽ-inj : (x : V ) (p q : Elⱽ x  Ω)  subsetⱽ x p  subsetⱽ x q  p  q
subsetⱽ-inj x p q α = funext λ ex 
  let
    same-ix :  {a b} (p : PathP  i  Elⱽ (α i)) a b)  a .fst  b .fst
    same-ix p = !-inj x (ap-set  i  (α i ! p i) .tree))
  in Ω-ua
     a 
      let (ix , pix) = subst Elⱽ α (ex , a)
       in subst (_∈ q) (sym (same-ix {ex , a} {ix , pix} (to-pathp refl))) pix)
     a 
      let (ix , pix) = subst Elⱽ (sym α) (ex , a)
       in subst (_∈ p) (same-ix {ix , pix} {ex , a} (to-pathp⁻ refl)) pix)

ℙⱽ : V   V 
ℙⱽ x = mkⱽ λ where
  .Elt            Elⱽ x  Ω
  .idx p          subsetⱽ x p
  .inj {p} {q} α  subsetⱽ-inj _ _ _ α

Function sets🔗

To encode function sets, we will make use of realignⱽ and closure of under power sets. When the codomain is a (family of) sets, the (dependent) function type embeds into the type of predicates on by the map which sends each function to its graph.

module _ {A : Type } {B : A  Type } where
  graph : (∀ x  B x)  (Σ[ a  A ] B a  Ω)
  graph f (x , y) = elΩ (f x  y)

  graph-inj
    :  _ :  {x}  H-Level (B x) 2 
     (f g : (x : A)  B x)  graph f  graph g  f  g
  graph-inj f g α = funext λ a 
    case subst  e  (a , f a)  e) α (inc refl) of sym

The realignment principle then lets us obtain a definitional encoding for dependent function types as a subset of the encoding of relations.

Πⱽ : (A : V ) (B : Elⱽ A  V )  V 
Πⱽ A B = realignⱽ (ℙⱽ (Σⱽ A B))
  graph (graph-inj _ _)

_ :  {A : V } {B}  Elⱽ (Πⱽ A B)  ((x : Elⱽ A)  Elⱽ (B x))
_ = refl

Lifting and a for 🔗

Agda universes are not cumulative, but we can define a Lifting operation which codes for a type in some higher-levelled universe, which we generically write as being By inserting these Lifts at every sup of a we can also lift

liftⱽ :  ℓ'  V   V (  ℓ')
liftⱽ { = } ℓ' = wrap module liftⱽ where
  liftⱽ' : V'   V' (  ℓ')
  liftⱽ' (sup x f) = sup (Lift ℓ' x)  (lift i)  liftⱽ' (f i))
Using that Lift is an embedding, we can prove by an inductive calculation that the recursive lifting liftⱽ' is also an embedding.
  module l {x} {y} = Equiv (ap (Lift {} ℓ') {x} {y} , embedding→cancellable (Lift-is-embedding ℓ'))

  abstract
    inj' : (x y : V' )  (liftⱽ' x  liftⱽ' y)  (x  y)
    inj' (sup x f) (sup y g) =
      liftⱽ' (sup x f)  liftⱽ' (sup y g)
        ≃⟨ ap-equiv W-fixpoint 
      (Lift ℓ' x , liftⱽ'  f  lower)  (Lift ℓ' y , liftⱽ'  g  lower)
        ≃˘⟨ Σ-pathp≃ ≃˘
      (Σ (Lift ℓ' x  Lift ℓ' y)  p  PathP  i  p i  V' (  ℓ')) (liftⱽ'  f  lower) (liftⱽ'  g  lower)))
        ≃˘⟨ Σ-ap-fst (Equiv.inverse l.inverse) ≃˘
      (Σ (x  y) λ p  PathP  i  Lift ℓ' (p i)  V' (  ℓ')) (liftⱽ'  f  lower) (liftⱽ'  g  lower))
        ≃˘⟨ Σ-ap-snd  p  apd-equiv  i  Π-ap-dom Lift-≃)) ≃˘
      (Σ (x  y) λ p  PathP  i  p i  V' (  ℓ')) (liftⱽ'  f) (liftⱽ'  g))
        ≃⟨ Σ-ap-snd
             p  funext-dep≃ e⁻¹ ∙e Π'-ap-cod  x  Π'-ap-cod λ _  Π-ap-cod λ _  inj' (f x) _) ∙e funext-dep≃) 
      (Σ (x  y) λ p  PathP  i  p i  V' ) f g)
        ≃⟨ Σ-pathp≃ 
      (x , f)  (y , g)
        ≃˘⟨ ap-equiv W-fixpoint ≃˘
      sup x f  sup y g
        ≃∎

  emb : is-embedding liftⱽ'
  emb = cancellable→embedding (inj' _ _)

Because of our definition of we need a wrapper saying that liftⱽ' sends iterative embeddings to iterative embeddings.

  go  : (w : V' ) (u : is-iterative-embedding w)  V (  ℓ')
  goβ : (w : V' ) (u : is-iterative-embedding w)  go w u .tree  liftⱽ' w

  go (sup x f) (φ , r) .tree = liftⱽ' (sup x f)
  go (sup x f) (φ , r) .uniq =
    ∘-is-embedding (∘-is-embedding emb φ) (is-equiv→is-embedding (Lift-≃ .snd))
    , λ (lift y)  let it = go (f y) (r y) .uniq in subst is-iterative-embedding (goβ (f y) (r y)) it

  goβ (sup x f) (_ , _) = refl

  wrap : V   V (  ℓ')
  wrap S = go (S .tree) (S .uniq)

  is-inj : injective wrap
  is-inj α = ap-set (ap fst (emb _ (_ , sym (goβ _ _)  ap tree α  goβ _ _) (_ , refl)))

  ungo : (w : V' ) (u : is-iterative-embedding w)  v-label (go w u)  v-label (set w u)
  ungo (sup x f) u .fst = lower
  ungo (sup x f) u .snd = is-iso→is-equiv (iso lift  _  refl) λ _  refl)

  unraise :  x  Elⱽ (wrap x)  Elⱽ x
  unraise x = ungo (x .tree) (x .uniq)
  module unraise x = Equiv (unraise x)

Since liftⱽ is itself an embedding of onto for any we can obtain a definitional for

Vⱽ :  {}  V (lsuc )
Vⱽ {} = mkⱽ λ where
  .Elt  V 
  .idx  liftⱽ _
  .inj  liftⱽ.is-inj _

  1. In the type-theoretic literature, these universes are termed “à la Tarski”, or simply “Tarski universes”. If there is no decoding type family, and the elements of a universe are literally types, then they are called “à la Russell”, or “Russell universes”.↩︎


References