Structures

A first-order language about sets has two primitive predicates: equality and membership. To interpret it, we must choose what its variables range over and what those two predicates mean there. A ZFStructure packages exactly this data: a carrier of "sets", together with proposition-valued interpretations of equality and membership. The record demands that the carrier be an h-set and nothing more; no ZF axiom is built in.

Because both relations take values in hProp, each atomic statement has an underlying type whose inhabitants are its proofs. A class over the carrier can therefore be used to cut out a smaller structure: Transitive expresses that members of members of a class stay in the class, and the restriction 𝒮 ↾ M turns the class into the carrier of a new structure of dependent pairs. Since the membership fibers are propositions, that pair carrier is again an h-set, and equality of first projections already determines equality of the pairs.

Three membership notations must be kept apart throughout: the host-level class membership ∈ᶜ, which tests whether a carrier element satisfies a predicate M; the proposition-valued structure membership ∈ˢ; and the object-language membership symbol ∈̇ introduced in "The object language", which is only given meaning once a structure interprets it.

Membership appears on three distinct levels, and the notation keeps them apart. At the host level, a class is a predicate M valued in hProp, and x ∈ᶜ M is the underlying proposition ⟨ M x ⟩: a type witnessing that x satisfies the predicate. This is a relation between a carrier element and a predicate, not between two sets. At the structure level, x ∈ˢ y is a proposition about two carrier elements. The object level belongs to the syntax introduced in "The object language", where ∈̇ is a mere symbol awaiting interpretation.

{-# OPTIONS --cubical --safe --guardedness #-}

module FOL.ZFStructure where

open import Base.Prelude

The relations of a structure are propositions, so their underlying types may be inhabited by proofs. Gathering the carrier elements that satisfy a class forms a dependent pair type. The carrier S being an h-set does not automatically make such a pair type an h-set; what saves it is that each fiber, the membership evidence at a fixed element, is a proposition, so no two distinct proofs can separate otherwise equal pairs.

open import Cubical.Foundations.HLevels using ( isSetΣSndProp )

Restricting a structure to a class therefore rests on a general principle about dependent pairs. A pair consists of a first projection together with a second component whose type depends on the first. When that second component is proposition-valued, the pair carries no information beyond its first projection up to equality: if fst a ≡ fst b, then already a ≡ b. The chapter closes with a lemma, ↾-reflects, recording this direction for the restricted carrier.

open import Cubical.Data.Sigma using ( Σ≡Prop )

The record

Why should equality of sets be a field rather than the host's fixed path equality? Because the language of set theory treats = and ∈ as primitive symbols, and a structure is precisely a choice of meaning for them. Two carrier elements may be equal according to the structure even when they are distinct as inhabitants of the host type. Making ≈ˢ and ∈ˢ proposition-valued fields states exactly what the structure supplies; the record imposes no compatibility laws between the two relations.

The conventions are book-wide: script 𝒮 stands for a structure, S for its carrier, and x, y, z for carrier elements, the "sets" the language speaks of. The superscript ˢ marks a symbol as a field of the structure at hand, and the membership family on the page now has one glyph per layer: the library's ∈ for the host, ∈ˢ for the structure, and the object-language symbol ∈̇ for the syntax.

The record is deliberately bare model-theoretic data. It requires the carrier to be an h-set and gives the two truth-valued relations; it asserts no extensionality, well-foundedness, or any other ZF axiom. Those belong to the later model chapters, where they appear as further fields.

The carrier S is an ordinary type at level ℓ, and the field isSetS asks that it be an h-set: its equality types are propositions. This is the only constraint on what the language's "sets" may be. The two relation fields take values in hProp ℓ. Since both S : Type ℓ and hProp ℓ live one universe up, the whole record has type Type (ℓ-suc ℓ).

record ZFStructure (ℓ : Level) : Type (ℓ-suc ℓ) where
  field
    S         : Type ℓ
    isSetS    : isSet S

The two relation fields give the structure's equality ≈ˢ and membership ∈ˢ, each a function S → S → hProp ℓ. Thus x ∈ˢ y is a proposition about two carrier elements. The record ends here: the carrier and two relations are data, the h-set condition is a constraint, and no set-theoretic axiom is imposed.

    _≈ˢ_ _∈ˢ_ : S → S → hProp ℓ

  infix  _≈ˢ_ _∈ˢ_

The structure equality ≈ˢ is a field rather than the host's path equality, so an arbitrary structure supplies its own proposition-valued interpretations of equality and membership, with no compatibility laws imposed by the record.

The propositional side

Every structural membership proposition has an underlying type. The notation x ∈ᵗ y names exactly ⟨ x ∈ˢ y ⟩. This Type-valued reading is what lets later definitions use a proof of membership and collect class members into a dependent pair. The module hPropStructure adds this notation on top of the structure's fields.

x ∈ᵗ y is defined as the underlying type ⟨ x ∈ˢ y ⟩, and therefore lies in Type ℓ. This is not a new relation but a Type-valued reading of the existing membership proposition. Note the direction of the arguments, matching the earlier notations: x ∈ᵗ y reads "x is a member of y".

module hPropStructure {ℓ} (𝒮 : ZFStructure ℓ) where
  open ZFStructure 𝒮 public

  _∈ᵗ_ : S → S → Type ℓ
  x ∈ᵗ y = ⟨ x ∈ˢ y ⟩

So y ∈ᵗ x states that y is a member of x, as a proposition of the proposition-valued structure; an inhabitant of this type is evidence that the membership truth value holds.

  infix  _∈ᵗ_

Transitive classes

With membership available as a Type-valued proposition, a class over the carrier becomes something whose elements we can reason about element by element. A class M is transitive when every member of an element of M is itself in M. This is the set-theoretic notion of transitivity, phrased with the two available membership relations: the structure's ∈ᵗ on the left of the implication, and the host-level ∈ᶜ for membership in the class itself.

Transitive takes a proposition-valued structure 𝒮 and a class M : S → hProp ℓ, and states the implication y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M: assuming y is a member of x in the structure, and x belongs to the class M, y belongs to M as well. The direction is closure under members of members, not closure under subsets; the definition quantifies over carrier elements x and y implicitly and asserts nothing beyond this implication.

Transitive : ∀ {ℓ} (𝒮 : ZFStructure ℓ)
           → (ZFStructure.S 𝒮 → hProp ℓ) → Type ℓ
Transitive 𝒮 M = ∀ {x y} → y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M
  where open hPropStructure 𝒮

Substructures

Given a proposition-valued class M, we can now cut a structure down to the part of its carrier that satisfies M. The restriction 𝒮 ↾ M is again a ZFStructure, and its carrier is the type of dependent pairs (x , proof) with x : S and proof : x ∈ᶜ M. Equality and membership on the restricted elements are inherited from 𝒮: both relations look only at the first projections and apply the original relations there. This changes what counts as an element of the structure; it does not construct a set representing M, nor does it by itself fix a syntax or a constant domain.

The new carrier is the Σ-type Σ[ x ∈ S ] (x ∈ᶜ M): an inhabitant is a pair of an underlying carrier element and membership evidence in M, so restricting does not collect M into a set, it only changes which pairs count as elements. The record's isSetS field still must be filled, and here the fiber-wise fact from the chapter opening does the work: since each M x is a proposition by its second component, isSetΣSndProp applied to isSetS proves that this pair type is again an h-set.

_↾_ : ∀ {ℓ} (𝒮 : ZFStructure ℓ)
    → (ZFStructure.S 𝒮 → hProp ℓ) → ZFStructure ℓ
_↾_ {ℓ} 𝒮 M = record
  { S      = Σ[ x ∈ S ] (x ∈ᶜ M)
  ; isSetS = isSetΣSndProp isSetS (λ x → (M x) .snd)

Both relation fields pull the original relations back along the first projection: for restricted elements a and b, the structure evaluates fst a ≈ˢ fst b and fst a ∈ˢ fst b. So membership and equality between restricted elements are evaluated entirely on their underlying carrier elements; whatever evidence the pairs carry in their second components plays no role in the relations.

  ; _≈ˢ_   = λ a b → fst a ≈ˢ fst b
  ; _∈ˢ_   = λ a b → fst a ∈ˢ fst b }
  where open ZFStructure 𝒮

infixl  _↾_

The relations of 𝒮 ↾ M ignore the second components, so one might ask whether the restricted carrier distinguishes pairs at all beyond their first projections. It does not: because each membership type M x is a proposition, a path between the first projections determines a path between the whole pairs. The following lemma records this direction.

↾-reflects has type fst a ≡ fst b → a ≡ b. It applies Σ≡Prop with the family λ x → (M x) .snd, whose value proves pointwise that the membership evidence at x is proposition-valued; the resulting path between pairs is then built from the path between first projections alone. The lemma states this one direction only: it reflects equality of the underlying elements up to equality of the restricted elements, and says nothing about a converse.

↾-reflects : ∀ {ℓ} {𝒮 : ZFStructure ℓ} {M : ZFStructure.S 𝒮 → hProp ℓ}
             {a b : ZFStructure.S (𝒮 ↾ M)}
           → fst a ≡ fst b → a ≡ b
↾-reflects {M = M} = Σ≡Prop (λ x → (M x) .snd)

Recap

A ZFStructure records four fields: a carrier, its h-set proof, and proposition-valued interpretations of equality and membership. It includes no ZF axioms. For proposition-valued structures, ∈ᵗ exposes the underlying membership type, Transitive states closure under members of members, and 𝒮 ↾ M restricts the carrier to a class of dependent pairs. The lemma ↾-reflects lifts equality of first projections to equality in that restricted carrier. The next step is to interpret the object-language formulas themselves inside such a structure.