|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-proposition, mere proposition|
|cut elimination for implication||counit for hom-tensor adjunction||beta reduction|
|introduction rule for implication||unit for hom-tensor adjunction||eta conversion|
|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)|
|linear logic||(symmetric, closed) monoidal category||linear type theory/quantum computation|
|proof net||string diagram||quantum circuit|
|(absence of) contraction rule||(absence of) diagonal||no-cloning theorem|
structures in a cohesive (∞,1)-topos
As remarked at type theory, it is useful to distinguish between the internal type theory of a category and the internal logic which sits on top of that type theory. The type theory is about constructing objects, while the logic is about constructing subobjects. For instance, limits and colimits, exponentials, and object classifiers belong to the type theory, while images, dual images?, intersections, unions, and subobject classifiers belong to the logic. Thus, the semantics of (extensional) type theory naturally lies in a category with appropriate structure, while the semantics of logic over that type theory naturally lies in some indexed poset over that category. However, we commonly take this indexed poset to consist of the subobjects in the category in question, in which case additional “logical” structure on the category is required, for instance that it be a Heyting category.
In an elementary 1-topos, all of the “logical” structure is not usually included in the definition, because it comes for free once you have power objects. But object classifiers may not be as powerful as power objects in this respect, so for purposes of studying the internal logic (and not just the internal type theory) of an -topos, it’s good to keep in mind both the type-theoretic structure and the logical structure, and in particular both the object classifier and the subobject classifier.
Amazingly, a variant of type theory that seems appropriate for interpretation in an -category already exists, namely intensional type theory with identity types.
The usual sort of type theory that one interprets in a 1-category is extensional type theory. To explain what this means, consider how the categorical structure of finite limits is represented in the type theory. On the one hand, we have product types , which of course represent categorical products; thus to obtain finite limits it suffices to have equalizers. We can obtain these from identity types, which supply for each type and each pair of terms , a dependent type , whose intended interpretation is that it is inhabited precisely when . In terms of 1-categorical semantics, it is natural to require that any two elements of be equal, i.e. that be essentially a truth value/subsingleton. Then if we have two terms and representing morphisms , their equalizer is represented by the type .
However, for semantics in an -category, it makes sense to use the same identity types, but now interpreted as a path space. Now it will no longer be true that is a subsingleton, since two points can be connected by more than one path, so we must drop that axiom. This intensional type theory has been widely studied by type-theorists, although from a different point of view: assuming the propositions as types approach, should be the type of proofs or reasons why , which can also of course have many different elements.
Thus we suspect that intensional type theory may be a natural sort of type theory to have semantics in an -category. According to the general framework of syntax/semantics, we would hope that
Some work in both of these directions has been done. On the one hand, it is known that in any intensional type theory with identity types, for any type the globular set (or more accurately globular context) given by
has the structure of a Batanin ω-groupoid. This can be found in:
Moreover, the syntactic category of such a theory carries a natural weak factorization system, the identity type weak factorization system?. However, there seems as yet to be no published work constructing a full syntactic -category.
On the other hand, it is known that in any nice enough model category (and in fact, in any category with a nice enough weak factorization system), one can model intensional type theory. This is studied in
Although intensional type theory has semantics in -categories, one can naturally expect that these models will all satisfy additional axioms. This is especially true if we want to add additional structure to our -categories.
Exponential (and dependent product) types can probably be modeled by (locally) cartesian closed -categories. However, although exponentials in an -category are not strictly extensional the way they are in a 1-category, they are still extensional “up to coherent higher homotopies,” which (unlike the case for identity types) is seemingly not guaranteed by the type-theoretic structure. Thus, there may be an -extensionality axiom to be added.
Disjoint sum types may be expected to correspond to coproducts in an -category.
The usual notions of quotient type make little sense without extensional identity types. In the 1-categorical world, quotient types correspond to exact categories, while the appropriate notion of “exactness” for an -category deals with groupoid objects in an (∞,1)-category. It remains to be seen how to phrase a corresponding axiom in the type theory.
The object classifier in an -topos does in fact correspond to a well-known concept in type theory, namely that of a universe such as the type . However, as a universe, the object classifier in an -topos has the special property that the paths between two types and as elements of (that is, the path space ) is equivalent to the space of equivalences between and as types (an appropriate subspace of the exponential ). A type-theoretic axiom asserting this equivalence was introduced by Voevodsky under the name of the equivalence axiom.
Now when we go to add logic to the type theory of an -category, it seems natural by analogy that it will deal with subobjects, i.e. with monomorphisms in an (∞,1)-category. That is, a proposition with a variable will be interpreted by a monomorphism . Just as in the internal logic of a 1-category and of a 2-category, in order to interpret the logical connectives and quantifiers we will then need suitable structure on the posets of subobjects in our -category. It is naturally to be expected that any -topos will have this necessary structure.
Again, the requisite type theory more or less exists, namely intensional type theory together with a sort of propositions that can depend on types. In fact, this type theory is very closely related to the calculus of constructions used in the proof assistant Coq, making Coq a very convenient place to play around with the type theory that ought to be valid in an -topos. In particular, Voevodsky has written out a Coq script up to the statement of his equivalence axiom, to be found on his website.
In describing the internal type theory and logic of an -category we encounter the problem that many structures in an -category require a (countably) infinite amount of data to describe. For instance, when looking for a way to state the “exactness” property one has to say what is meant by a groupoid object, but since this really means a “coherent” or ”” groupoid object, it involves an infinite amount of data. By contrast, the most common type theories are purely finitary systems.
There is the one amazing fact that the entire complicated infinitary structure of a Batanin -groupoid can be recovered from the simple finitary rules of identity types. It is not clear, however, whether we can expect this happy occurrence to continue. We might have to bite the bullet and work with an infinitary type theory, i.e. one allowing derivation rules taking as input an infinite list of hypotheses. In fact, this is almost certainly what we will need if we want a good notion of a geometric theory in the -case, since that involves infinitary logic even in the 1-categorical case.
However, such a type theory would obviously no longer have “computational content” and couldn’t be modeled in a proof assistant such as Coq, and also wouldn’t provide a fully “elementary,” i.e. finitary first-order, theory such as ETCS provides in the 1-categorical case. It might be helpful to note that infinitary structures can at least sometimes be finitarily described using inductive types and/or coinductive types, but it is not clear yet whether this is useful in the -categorical context.
Here we look at the -categorical analog of that discussion, step-by-step, now everything internal to ∞Grpd.
This generates under colimits: every small -groupoid is a colimit over a small diagram consisting only of copies of the terminal -groupoid.
The subobject classifier of is