---
title: "Structures"
module: FOL.ZFStructure
lang: en
site: "Bedrock"
description: "Structures"
stage: "First-order logic"
reading_order: 7
canonical: https://bedrock.institute/en/FOL.ZFStructure.html
html: FOL.ZFStructure.html
agda_source: https://github.com/BedrockInstitute/Bedrock/blob/main/src/FOL/ZFStructure.lagda.md
prerequisites: [Base.Prelude]
routes: [common-foundations]
translations: [https://bedrock.institute/zh/FOL.ZFStructure.md, https://bedrock.institute/ja/FOL.ZFStructure.md]
agent_guide: /llms.txt
license: CC-BY-NC-SA-4.0
---
# 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.

```agda
{-# 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.

```agda
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.

```agda
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 ℓ)`.

```agda
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.

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

  infix 20 _≈ˢ_ _∈ˢ_
```

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".

```agda
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.

```agda
  infix 20 _∈ᵗ_
```

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

```agda
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.

```agda
_↾_ : ∀ {ℓ} (𝒮 : 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.

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

infixl 21 _↾_
```

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.

```agda
↾-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.