Structures

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.

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.

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

  infix  _≈ˢ_ _∈ˢ_

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.

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.

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

open ZFStructure 𝒮 public

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

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

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.

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.

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.

infixl  _↾_
_↾_ : ∀ {ℓ ℓΩ} {Ω : 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.

  ; _≈ˢ_   = λ 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.

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