Sheaf Model

Definition

A sheaf model of type theory is a semantic interpretation of types and terms using sheaves over a topological space or site. In this model, types are interpreted as sheaves (or presheaves) and terms correspond to global sections of these sheaves.

More precisely, given a category $\mathcal{C}$ with a Grothendieck topology, a sheaf model interprets:

• Types $A$ as sheaves $[A]$ on $\mathcal{C}$
• Contexts $\Gamma$ as sheaves $[\Gamma ]$ on $\mathcal{C}$
• Terms $\Gamma ⊢t:A$ as natural transformations $[\Gamma ]\to [A]$

Properties

Local Character: The interpretation satisfies the sheaf condition, meaning that elements are determined by their local behavior and can be “glued” from compatible local data. Functoriality: The interpretation is functorial with respect to substitution, reflecting the compositional structure of type theory. Soundness: All typing rules and definitional equalities of the type theory are preserved in the sheaf model.

Construction

For dependent type theory, sheaf models are typically constructed using:

1. A base category $\mathcal{C}$ with finite limits
2. A Grothendieck topology on $\mathcal{C}$
3. The topos $\mathbf{Sh}(\mathcal{C})$ of sheaves on $\mathcal{C}$
4. A universe object in $\mathbf{Sh}(\mathcal{C})$ to interpret type universes The dependent product $\Pi x:A.B(x)$ is interpreted using the internal hom object, while dependent sums $\Sigma x:A.B(x)$ correspond to images of certain morphisms.

Applications

Sheaf models provide:

• Consistency proofs for type theories with strong axioms
• Models for Homotopy Type Theory via simplicial sheaves
• Interpretations of constructive logic and mathematics
• Connections between type theory and algebraic geometry

Examples

Beth Models (1956)

Beth introduced semantic trees to interpret intuitionistic logic. In this model, truth is established over time across a branching tree structure. A proposition is true at a node if it is eventually verified on every path passing through that node (a concept anticipating the covering notion in Grothendieck topologies).

Formally, this corresponds to a sheaf condition on a topological space constructed from the tree, emphasizing that truth is a local property that can be glued together from future states.

Kripke Semantics (1965)

Kripke simplified and generalized Beth’s work using partially ordered sets of “worlds” or “states of knowledge.” A Kripke model for intuitionistic logic consists of a poset $(W,\le )$ and a valuation relation that persists upwards.

Categorically, a Kripke model is a presheaf $P:W^{op}\to \mathbf{Set}$ (or valued in truth values $\Omega$). The monotonicity of truth corresponds to the functoriality of the presheaf restriction maps. Unlike Beth models, Kripke models generally do not require a covering condition (unless forcing a specific topology), making them purely presheaf-theoretic.

Other models

• Effective topos: Provides a model of Type Theory with choice principles
• Simplicial sheaves: Model homotopy type theory and univalent foundations
• Étale sheaves: Connect type theory with algebraic geometry

See also

• Presheaf Model of Type Theory
• Topos
• Homotopy Type Theory
• Contextual Category
• Semi-Simplicial Complex