|logic||category theory||type theory|
|true||terminal object/(-2)-truncated object||h-level 0-type/unit type|
|false||initial object||empty type|
|proposition||(-1)-truncated object||h-level 1-type/h-prop|
|classical type theory?||internal logic||classical type theory?, logic programming?|
|cut elimination?||counit||beta reduction|
|disjunction||coproduct ((-1)-truncation of)||sum type (bracket type of)|
|implication||internal hom||function type|
|negation||internal hom into initial object||function type into empty type|
|universal quantification||dependent product||dependent product type|
|existential quantification||dependent sum ((-1)-truncation of)||dependent sum type (bracket type of)|
|equivalence||path space object||identity type|
|equivalence class||quotient||quotient type|
|induction||colimit||inductive type, W-type, M-type|
|higher induction||higher colimit||higher inductive type|
|completely presented set||discrete object/0-truncated object||h-level 2-type/preset/h-set|
|set||internal 0-groupoid||Bishop set/setoid|
|universe||object classifier||type of types|
|modality||closure operator monad||modal type theory, monad (in computer science)|
The stack semantics is an extension of the internal logic of a category (or higher category) which allows us to talk about, and quantify over, objects of . (Such quantification is sometimes called “unbounded” quantification.)
In the ordinary internal language, an internal “element” of an object is interpreted into a generalized element for some object , which consists intuitively of one “actual” element of for every element of . Similarly, in the stack semantics, an internal “object” is interpreted as a “generalized object” defined at some stage , which we define to mean an object of the slice category . This makes sense because an object of consists intuitively of one “actual” object of for each “element” of (namely, the fiber over that element).
The stack semantics is so-called because in most categories where we consider it (such as toposes or pretoposes), the self-indexing is a stack for some naturally defined Grothendieck topology on , and the stack semantics can be regarded as the ordinary internal logic of a higher topos of stacks on (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 .
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 in , then generalized elements of at stage can be regarded as “names” for generalized objects of at stage . Namely, the generalized element names the pullback of along .
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 may have multiple names, whereas the stack semantics ought to speak directly about objects rather than about names for them. Moreover, since is actually a category (or a higher category, if is such), generalized objects should be considered “the same” only if they are isomorphic or equivalent, whereas morphisms may admit a stricter notion of sameness. In particular, when is a 1-category (the classical case), the morphisms form a set, whereas should be regarded as a category, or at worst as a groupoid (its core).
More generally, if is an n-category for some finite , then is only an -category, whereas is also an -category or at worst an n-groupoid. Thus, there is no hope of solving this problem inside of unless is at least an (∞,1)-category. In that case, the notion of object classifier in an (∞,1)-category does solve this problem: the -groupoid is equivalent to the core of (a suitable subcategory of) . (The presence of noninvertible morphisms in is not nearly so big a problem; at least when is an -category, these can be described already in the ordinary internal logic if is locally cartesian closed category.)
If is only an -category for some finite , 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 -category. The obvious choice is a category of presheaves or sheaves/stacks on valued in -categories or -groupoids (or -groupoids for some ).
The second issue is that not every “generalized object” over may have a name. This is almost impossible to get around while remaining within , due to issues with paradoxes. Even object classifiers in an (∞,1)-category only classify the core of some subcategory of .
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 . In particular, if we work in a category of presheaves/sheaves/stacks on at one category-level up, then the self-indexing of (or its core) will be an object which classifies exactly the desired category of generalized objects for each . (The exhaustive sequence of universes can also be regarded as moving outside of , perhaps to a category of ind-objects in .) The fragment of the internal logic of this category of stacks which deals only with objects of 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 ). The object in this case is, of course, the subobject classifier.
A geometric morphism looks like the canonical morphism when using the stack semantics of .
The internal statement ” is a compact topos” is equivalent to being a proper morphism.
Because the proof that indiscrete toposes are compact is constructive, it immediately follows that hyperconnected morphisms are proper.
J. Penon, Categories localement internes, C. R. Acad. Sci. Paris 278 (1974) A1577-1580