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. The gluing theorem, from SGA4, states that for any left exact functor F : E → S between toposes the comma category S ↓ F is again a topos, and that E and S embed in it as a closed and an open subtopos respectively — the two together are complementary, and every topos with a chosen subterminal decomposes this way. Freyd (1972) drew the logical consequence: gluing the syntactic topos of intuitionistic higher-order logic along its global-sections functor produces a topos whose terminal object is indecomposable and projective, and those two facts are exactly the disjunction and existence properties. The construction is uniform, so the same argument yields DP and EP for intuitionistic predicate logic, for higher-order Heyting arithmetic, and for Martin-Löf type theory, where the syntactic proofs are separate inductions. The Freyd cover is the same construction later named the scone, and Mitchell and Scedrov (1992) identified it as the categorical form of a logical relation, which is why gluing also yields normalization and canonicity: Altenkirch, Hofmann and Streicher (1995) reconstructed normalization by evaluation as a gluing argument, and Sterling and Angiuli (2021) proved normalization for cubical type theory by Artin gluing.

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. Left exactness of the glued functor is not negotiable: glue along a functor that fails to preserve finite limits and the comma category need not be a topos, so the theorem gives no technique for functors that merely preserve products. 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 argument yields a normalization algorithm with a measure, the categorical one yields an existence claim, and extracting a program from it requires the gluing to be carried out constructively in the metatheory. The properties proved concern closed terms over the empty context only; nothing follows about derivability under hypotheses, where DP fails outright. Closure rules that are not about the terminal object — Church's rule, Markov's rule, independence of premise — do not come from gluing over Set and need realizability instead. And the method says nothing classically: adding excluded middle, or any axiom making the syntactic topos Boolean, leaves 1 decomposable, so the property itself fails rather than the proof.

© 2026 Lingenic LLC