Artin Gluing and Freyd Covers

Origin. The gluing construction is Artin's, from SGA4 (1972), where it assembles a topos from an open and its closed complement. Peter Freyd, "Aspects of topoi" (1972), used it to prove the disjunction and existence properties for intuitionistic logic categorically. Lambek and Scott's Introduction to Higher Order Categorical Logic (1986) is where the logical technique was systematized; Taylor's Practical Foundations (1999) and Streicher's later work extend it to type theory.

Models. The disjunction property — if ⊢ φ ∨ ψ then ⊢ φ or ⊢ ψ — is proved syntactically by normalization, and the proof is a combinatorial induction that has to be redone for every system. Freyd's method proves it once, structurally: glue the term model to Set along the global-sections functor, show the glued category still models the theory, and read the property off the gluing. The induction disappears into a pullback.

Formalism.

The Freyd cover (glueing along global sections): Let C be the term model of a theory, Γ = Hom(1, −) : C → Set the global-sections functor. The Freyd cover C̃ is the comma category (Set ↓ Γ): objects are triples (S, A, f) with S a set, A ∈ C, f : S → Γ(A) morphisms are the evident commuting squares.

Artin gluing, generally: For a left-exact functor F : E → S, the glued category S ↓ F. If E and S are toposes and F is left exact, S ↓ F is a topos. The two projections give an open and a closed inclusion — the topos is glued from the pieces.

The disjunction property, categorically: 1 is indecomposable in C̃: 1 → A + B factors through A or through B. Transport that along the projection C̃ → C and it says: ⊢ φ ∨ ψ implies ⊢ φ or ⊢ ψ. The property is a fact about the terminal object of the glued category, not about proofs.

The existence property: 1 is projective in C̃ with respect to the covers that interpret ∃. So ⊢ ∃x φ(x) implies ⊢ φ(t) for some closed term t. Same construction, different property of 1.

Why it generalizes: The construction needs only that Γ be left exact. It applies uniformly to IPC, to Martin-Löf type theory, to the internal logic of any topos with enough structure. The syntactic proofs do not transfer; this one does.

Symbols.

Metatheory. Freyd's proof is the standard demonstration of what categorical logic buys: a property that syntactic methods prove by induction on derivations, one system at a time, becomes a structural fact about the terminal object of a glued category, and the same construction then applies to any theory whose term model is a category of the right kind. That is the third of the subject's three themes — term models characterized by a universal property, with metatheorems as corollaries — cashed. Gluing also has a topological reading: Artin's construction assembles a topos from an open subtopos and its closed complement, so the logical technique and the geometric one are the same, which is the connection Grothendieck's machinery was doing before anyone applied it to logic.

Applies to. The disjunction and existence properties, for intuitionistic logic and for type theories. Canonicity and normalization proofs by gluing — the modern form, where the glued category is the logical relation. Realizability and parametricity, which are gluing constructions. Any metatheorem provable from the term model's universal property rather than from its derivations.

Limitations. The construction needs the term model to be a category with enough structure, so it proves properties of theories that already have a categorical semantics — and supplying that semantics is often as much work as the syntactic proof would have been. Gluing gives the disjunction property and gives no bound: the syntactic proof yields a normalization algorithm, and the categorical proof yields an existence claim. For classical logic it says nothing, since 1 is not indecomposable there, which is the correct answer and not a useful one.

© 2026 Lingenic LLC