nLab stack semantics

Stack semantics


Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory

logicset theory (internal logic of)category theorytype theory
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Stack semantics


The stack semantics is an extension of the internal logic of a category (or higher category) CC which allows us to talk about, and quantify over, objects of CC. (Such quantification is sometimes called “unbounded” quantification.)

In the ordinary internal language, an internal “element” of an object AA is interpreted into a generalized element XAX\to A for some object XCX\in C, which consists intuitively of one “actual” element of AA for every element of XX. Similarly, in the stack semantics, an internal “object” is interpreted as a “generalized object” defined at some stage XX, which we define to mean an object of the slice category C/XC/X. This makes sense because an object of C/XC/X consists intuitively of one “actual” object of CC for each “element” of XX (namely, the fiber over that element).

The stack semantics is so-called because in most categories CC where we consider it (such as toposes or pretoposes), the self-indexing is a stack for some naturally defined Grothendieck topology on CC, and the stack semantics can be regarded as the ordinary internal logic of a higher topos of stacks on CC (see below). Analogously, the ordinary internal logic is often called sheaf semantics, because in a subcanonical topology all representable functors are sheaves, and because it can often be regarded as part of the internal logic of the topos of sheaves on CC.


Direct description

As internal logic

While on the one hand, the stack semantics generalizes the internal logic of a category, it can also be regarded as a special case thereof.

The basic idea of this is that if we have a chosen morphism U˜U\widetilde{U}\to U in CC, then generalized elements of UU at stage XX can be regarded as “names” for generalized objects of CC at stage XX. Namely, the generalized element u:XUu\colon X\to U names the pullback of U˜U\widetilde{U}\to U along uu.

There are two issues with this idea, which can prevent it from faithfully representing the idea of the stack semantics sketched above.

The first issue is that a given “generalized object” over XX may have multiple names, whereas the stack semantics ought to speak directly about objects rather than about names for them. Moreover, since C/XC/X is actually a category (or a higher category, if CC is such), generalized objects should be considered “the same” only if they are isomorphic or equivalent, whereas morphisms XUX\to U may admit a stricter notion of sameness. In particular, when CC is a 1-category (the classical case), the morphisms XUX\to U form a set, whereas C/XC/X should be regarded as a category, or at worst as a groupoid (its core).

More generally, if CC is an n-category for some finite nn, then C(X,U)C(X,U) is only an (n1)(n-1)-category, whereas C/XC/X is also an nn-category or at worst an n-groupoid. Thus, there is no hope of solving this problem inside of CC unless CC is at least an (∞,1)-category. In that case, the notion of object classifier in an (∞,1)-category does solve this problem: the \infty-groupoid C(X,U)C(X,U) is equivalent to the core of (a suitable subcategory of) C/XC/X. (The presence of noninvertible morphisms in C/XC/X is not nearly so big a problem; at least when CC is an (n,1)(n,1)-category, these can be described already in the ordinary internal logic if CC is locally cartesian closed category.)

If CC is only an (n,1)(n,1)-category for some finite nn, however, then in order to obtain its stack semantics as an internal logic, we must pass to some higher category containing it which is at least an (n+1,1)(n+1,1)-category. The obvious choice is a category of presheaves or sheaves/stacks on CC valued in nn-categories or nn-groupoids (or mm-groupoids for some mnm\ge n).

The second issue is that not every “generalized object” over XX may have a name. This is almost impossible to get around while remaining within CC, due to issues with paradoxes. Even object classifiers in an (∞,1)-category only classify the core of some subcategory of C/XC/X.

One way to deal with this is to suppose some (possibly transfinite) sequence of object classifiers, each contained in the next, such that every generalized object is eventually classified by some one of them. In the internal logic, this corresponds roughly to the idea of universe polymorphism in type theory.

Another way is, of course, to move outside of CC. In particular, if we work in a category of presheaves/sheaves/stacks on CC at one category-level up, then the self-indexing of CC (or its core) will be an object UU which classifies exactly the desired category C/XC/X of generalized objects for each XCX\in C. (The exhaustive sequence of universes can also be regarded as moving outside of CC, perhaps to a category of ind-objects in CC.) The fragment of the internal logic of this category of stacks which deals only with objects of CC itself can then be identified with the direct Kripke–Joyal style stack-semantics described above.

Of course, one can also embrace this second limitation and just live with a “partial” stack semantics that only allows us to talk about a particular subclass of generalized objects. The Mitchell–Bénabou language of a topos can be regarded as a partial stack semantics in this sense, in which the only generalized objects we can classify over are the subterminal objects (i.e. the subobjects AXA \hookrightarrow X). The object UU in this case is, of course, the subobject classifier.

One can also embrace the first limitation and not worry about having multiple names for the same object. This leads to notions such as a universe in a topos and the field of algebraic set theory.

Relationship to locally internal categories

The stack semantics for a topos \mathcal{E} can be used to talk about locally internal categories of \mathcal{E} (in the sense of (Penon 1974)) as if they’re ordinary locally small categories over Set\mathrm{Set}.


  • A geometric morphism f:f: \mathcal{F} \to \mathcal{E} looks like the canonical morphism Set\mathcal{F} \to \mathrm{Set} when using the stack semantics of \mathcal{E}.

  • The internal statement “\mathcal{F} is a compact topos” is equivalent to ff being a proper morphism.

  • The internal statement “\mathcal{F} is an indiscrete topos” (i.e. “the canonical morphism Sub (1)Sub Set(1)\mathrm{Sub}_{\mathcal{F}}(1) \to \mathrm{Sub}_{\mathrm{Set}}(1) is a bijection”, where Sub\mathrm{Sub} refers to the corresponding posets of subobjects) is true iff ff is hyperconnected.

  • Because the proof that indiscrete toposes are compact is constructive, it immediately follows that hyperconnected morphisms are proper.


  • Locally internal categories, Appendix in: Peter Johnstone, Topos theory, London Math. Soc. Monographs 10, Acad. Press 1977, xxiii+367 pp.

Last revised on January 26, 2021 at 17:30:26. See the history of this page for a list of all contributions to it.