---
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: https://bedrock.institute/llms.txt
license: "CC-BY-NC-SA-4.0"
---


```agda
{-# OPTIONS --cubical --safe --guardedness #-}
module FOL.ZFStructure where
```

# Structures

```agda
open import Base.Prelude
```

The preceding chapter told us which claims about sets can be written, but not what would make one true. Before asking whether a written claim holds, we must decide what objects its expressions can refer to and how to test the two basic claims: that two objects are equal or that one belongs to the other. A **structure** supplies those choices.

This chapter specifies the data of a structure, then constructs its restriction to the objects satisfying a chosen property. No set-theoretic axiom is assumed here.

## Carrier and relations

In the object language, `t ≐ u` and `t ∈̇ u` are formulas, not yet propositions that can be proved. To interpret them, choose a type `S` of objects and two relations on it. We write `𝒮` for the resulting structure and `x`, `y` for elements of its **carrier** `S`. The superscript `ˢ` marks the relations supplied by `𝒮`.

Why supply an equality relation instead of using Agda's path equality `x ≡ y`? The object-language equality sign needs an interpretation of its own. The field `x ≈ˢ y` can assign a truth value even when no path `x ≡ y` is given. At this stage the field is just a binary relation; we have not required the laws of equality or any compatibility with membership.

**Definition** (`ZFStructure`) At carrier level `ℓ`, the `record` takes a truth-value type `Ω` as a parameter. Its fields are a carrier `S : Type ℓ`, a proof that `S` is an h-set, and two relations `S → S → Ω` for equality and membership. The level of `Ω` need not equal `ℓ`. Keeping this underlying definition general lets us choose the truth values separately. No laws for either relation are assumed.

```agda
record ZFStructure (ℓ : Level) {ℓΩ : Level} (Ω : Type ℓΩ)
  : Type (ℓ-max (ℓ-suc ℓ) ℓΩ) where
  field
    S         : Type ℓ
    isSetS    : isSet S
```

The remaining fields give a truth value for each ordered pair of carrier elements. The value `x ∈ˢ y` belongs to `Ω`; `t ∈̇ u` from the previous chapter is still a piece of syntax. The `record` does not yet say how terms denote elements, nor whether either relation obeys a set-theoretic axiom.

```agda
    _≈ˢ_ _∈ˢ_ : S → S → Ω

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

**Definition** (`ZFStructureₕ`) For the proposition-valued structures used below, choose `hProp ℓ` as the truth-value type Ω. The subscript `ₕ` marks this choice at the carrier's level without introducing another `record`.

```agda
ZFStructureₕ : (ℓ : Level) → Type (ℓ-suc ℓ)
ZFStructureₕ ℓ = ZFStructure ℓ (hProp ℓ)
```

The name `ZFStructure` identifies the language whose symbols are to be interpreted, not a model already satisfying ZF. One could, for example, use natural numbers as the carrier and interpret the membership field by their usual order. That supplies the required data, but certainly does not prove the ZF axioms.

## Proposition-valued structures

For a `ZFStructureₕ`, the field `x ∈ˢ y` returns an `hProp`, a proposition together with its proof-irrelevance. To use a proof of that proposition as an argument, we pass to its underlying type `⟨ x ∈ˢ y ⟩`. The submodule `hPropView` keeps a structure `𝒮` fixed and gives this type the notation `x ∈ᵗ y`.

<details open class="submodule-fold">
<summary class="submodule-fold-heading">

```agda
module hPropView {ℓ} (𝒮 : ZFStructureₕ ℓ) where
```

</summary>
<div class="submodule-fold-content">

We first open `ZFStructure 𝒮` with `public`, so that `hPropView` "inherits" all the fields of `ZFStructure` at `𝒮`. They are available inside the submodule and re-exported to modules that open this view; no new structure is created.

```agda
  open ZFStructure 𝒮 public
```

An inhabitant of `y ∈ᵗ x` is a proof that `y` belongs to `x` in this structure. The left argument is the member, just as for `∈ˢ`; we give the two notations the same binding strength.

**Definition** (`_∈ᵗ_`) For carrier elements `x` and `y`, let `x ∈ᵗ y` be the underlying type of `x ∈ˢ y`.

```agda
  infix 20 _∈ᵗ_
  _∈ᵗ_ : S → S → Type ℓ
  x ∈ᵗ y = ⟨ x ∈ˢ y ⟩
```

### Transitive classes

Suppose a class `M` selects some elements of the carrier. If `x` is selected and `y` belongs to `x` according to the structure, must `y` also be selected? A **transitive class** is one for which the answer is yes. This is closure under *members*, not under subsets.

Transitivity is a closure condition on a class, not a field of the structure. It uses the underlying membership proof type, so it belongs to `hPropView`, where the proposition-valued structure is already fixed.

**Definition** (`Transitive`) For a proposition-valued structure `𝒮` and a class `M`, transitivity assigns, to any carrier elements `x` and `y`, a proof of `y ∈ᶜ M` from proofs of `y ∈ᵗ x` and `x ∈ᶜ M`. The quantification over `x` and `y` is implicit in the code.

```agda
  Transitive : (S → hProp ℓ) → Type ℓ
  Transitive M = ∀ {x y} → y ∈ᵗ x → x ∈ᶜ M → y ∈ᶜ M
```

</div>
</details>

The similar membership signs now play different roles. In particular, a class is a predicate `M : S → hProp ℓ`, so `x ∈ᶜ M` asks whether an element satisfies that predicate; it does not compare two carrier elements.

| notation | what it relates | what it gives |
| --- | --- | --- |
| `t ∈̇ u` | two terms | a formula, with no truth value yet |
| `x ∈ˢ y` | two carrier elements | a proposition in `hProp ℓ` |
| `x ∈ᵗ y` | the same two elements | the underlying proof type of `x ∈ˢ y` |
| `x ∈ᶜ M` | an element and a class | the underlying proof type of `M x` |
: Four membership notations and their distinct roles

## Substructures

To make the variables range over only the elements selected by `M`, we need a new carrier. It is not enough to keep the old type `S` and merely remember `M` alongside it: a variable of type `S` could still denote an unselected element. Instead, each element of the new carrier includes both an `x : S` and evidence that `x ∈ᶜ M`. The notation `𝒮 ↾ M` means the structure `𝒮` restricted to this class.

Restriction does not require transitivity or proposition-valued relations: the structure may use any truth-value type `Ω`. Only the predicate selecting carrier elements must be proposition-valued. We open the carrier-related field projections at module scope, leaving the two relations to be opened at a fixed structure where needed. Unlike the opening inside `hPropView`, this does not fix a structure: each projection takes it as an argument, as in `S 𝒮`. Here `𝒮` plays the role of a subscript on `S` in mathematical notation, specifying whose carrier we mean; in Agda it is an ordinary function argument.

```agda
open ZFStructure using ( S; isSetS )
```

**Definition** (`_↾_`) For any class `M : S → hProp ℓ`, the restricted structure has carrier `Σ[ x ∶ S ] (x ∈ᶜ M)`. This is a type of dependent pairs, not a set within the structure representing the class. The previously introduced `isSetClass` supplies its h-set proof from `isSetS` and the propositionhood of each membership type.

```agda
infixl 21 _↾_
_↾_ : ∀ {ℓ ℓΩ} {Ω : Type ℓΩ} (𝒮 : ZFStructure ℓ Ω)
    → (S 𝒮 → hProp ℓ) → ZFStructure ℓ Ω
_↾_ {ℓ} 𝒮 M = record
  { S      = Σ[ x ∶ S 𝒮 ] (x ∈ᶜ M)
  ; isSetS = isSetClass (isSetS 𝒮) (λ x → ⟨ M x ⟩isProp)
```

How should the two relations act on these pairs? For restricted elements `a` and `b`, apply the relations of `𝒮` to their first projections: `a .fst ≈ˢ b .fst` and `a .fst ∈ˢ b .fst`. We open just these two relations locally in the definition below. The proofs stored in the second components certify that the elements lie in `M`; they do not alter the truth values of equality or membership. Thus the relation fields are pulled back from `𝒮` along `fst`.

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

The relations use only the first components. Does equality of the dependent pairs themselves depend on the certificates in their second components? Here we mean Agda's path equality, not the freely chosen structure relation `≈ˢ`.

**Lemma** (`↾-reflects`) For `a` and `b` in the restricted carrier, a path `a .fst ≡ b .fst` determines a path `a ≡ b`.

**Proof** Transport one certificate along the given path between the first components. The two certificates then inhabit the same proposition and hence are equal, yielding a path between the dependent pairs. The library lemma `Σ≡Prop` carries out this construction; `⟨ M x ⟩isProp` supplies its required proof that each fibre is a proposition.

```agda
↾-reflects : ∀ {ℓ ℓΩ} {Ω : Type ℓΩ} {𝒮 : ZFStructure ℓ Ω}
             {M : S 𝒮 → hProp ℓ} {a b : S (𝒮 ↾ M)}
           → a .fst ≡ b .fst → a ≡ b
↾-reflects {M = M} = Σ≡Prop (λ x → ⟨ M x ⟩isProp)
```

The converse needs no special lemma: applying `fst` to a path `a ≡ b` gives `a .fst ≡ b .fst`.

## Recap

A structure supplies a carrier and interpretations of equality and membership. For any truth-value type, we can restrict the carrier by a proposition-valued predicate while inheriting both relations; membership proofs do not distinguish dependent pairs whose first components are equal. For proposition-valued structures, transitivity is a separate condition: members of selected objects must also be selected. The next chapter uses a chosen structure to interpret terms and formulas.