|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|
|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|
where on the left we have a category or 2-category of theories of some sort (i.e. in some doctrine), and on the right we have a category or 2-category of categories with some structure (e.g. finite limits, cartesian closure, etc.).
The syntactic category construction is the functor from theories to categories, denoted or . Given a theory, it generates the walking model of that theory, i.e. a structured category of the appropriate sort which is generated by a model of that theory. Since the objects of the syntactic category are frequently taken to be the contexts in the theory, the syntactic category is also called the category of contexts.
The functor in the other direction associates to any category its internal logic.
Given a type theory , its syntactic category or category of contexts is defined as follows.
A morphism from the context to the context consists of a way of fulfilling the assumptions required by by appropriately interpreting those provided by , generally by substituting terms available in for variables needed in and proving whatever is necessary from the assumptions at hand.
More precisely, let and be contexts of some type theory of the form
(Here we allow the possibility that each type in these contexts depends on the variables occurring earlier in the context, but for simplicity we can ignore that. )
Then a morphism in the category of contexts consists of a sequence of terms such as the following:
In other words, to give such a morphism we must give, for each type (or assumption) required by , a way to construct an element of that type (or a proof of that assumption) out of the data and assumptions contained in .
This might fit better after the motivating examples below; but maybe those examples don't make sense to a newcomer. This is incomplete, however, since it doesn't address contexts that include propositional hypotheses. —Toby
Depending on the type-forming operations available in , the category will have categorical structure. Roughly:
And so on. (If lacks eta-conversion, then this categorical structure may only be “weak”.) One thing worth noting is that
This is due to the objects of being contexts rather than types. A way to avoid this is to work instead with a syntactic cartesian multicategory.
In fact, is not just a structured category, it is a split model of type theory in any of the senses described there. In constructing formally an internal logic that involves dependent types, this is important to keep track of.
that preserve the relevant structure correspond to interpretations of in .
Accordingly, the adjunction counit evaluated on any category
says that there a canonical interpretation of the internal logic of a category in itself, while the unit evaluated at a theory :
says that there is a canonical interpretation of in the internal logic of its syntactic category.
Given a context and a type , there is a new context .
Given a term there is a canonical morphism of contexts
which picks that term in . The base change functor along this morphism
There is also the canonical morphism of contexts
which simply forgets the type . The base change along this morphism is the context extension functor
For example, consider these contexts in the theory of a group :
One interpretation of in (that is, a morphism from to ) is given by the substitution
The fact that in is ignored. In type-theoretic language, this would consist of the two terms
Note that in this way of presenting things, the names of the variables in do not appear; only the order in which the types appear in matters.
A less obvious interpretation of in is the substitution
There is no reason to keep variable names the same. (At this point, compare and ; when the definition is complete, it ought to follow that these are isomorphic.)
Another, perhaps even less obvious, morphism is
Not only does this ignore that ; it also ignores the very existence of in . (It also uses the existence of more than once. Ignoring and reusing information like this is not always allowed in substructural logics such as linear logic.)
We can interpret in without renaming variables because the theory of a group allows us to derive the judgment
That is, we get a morphism from to by performing the substitution
and then inserting a proof of the above judgment. As it happens, the argument in such a proof is reversible, so you should expect that and are also isomorphic.
Are there any morphisms from to ? The obvious substitution does not define a morphism, since the required fact cannot be proved. However, you get one using the substitution
and then inserting a proof that
All the same, we would not want to say that and are isomorphic contexts; although there are morphisms in each direction, composing them should never produce identity morphisms on both sides.
The category structure of can be seen explicitly as well. First, given a context , there is an obvious identity morphism where every variable is substituted for itself and every statement assumed is proved immediately from itself.
Given morphisms , form the composite as follows: First, for each variable required by , tells us how to substitute a term built out of the variables in , while tells us how to substitute a term from for each of these variables. So in the end, is expressed as a term involving variables available in . Also, by combining the proofs provided by and , we get the proofs required for their composite.
To really complete the definition of a category, I should also describe when two morphisms are equal. There are actually many options here; the most strict is to say that they are equal only if the substitutions and proofs used are syntactically identical, and the most weak is to say that any parallel morphisms are equal. Neither of these is very useful; for purposes of this example, let us require only that the expressions substituted for each variable in can be proved equal in the context .
Now you should be able to prove that composition satisfies the axioms of a category.
Notice that the exact definition of equality of morphisms can depend heavily on the theory in question and your own purposes. For example, this definition makes sense only because we have a notion of proving equality of elements of a group. Also, you can sometimes place interesting conditions on whether two proofs count as equivalent, rather than requiring either syntactic identity or (as we do here) accepting proof irrelevance.
Now that the category of contexts (in one sense) of the theory of a group has been completely defined, describe that category (up to equivalence) in terms familiar to an algebraist. In particular, compare it to the category of groups.
In rot13 (so that you have a chance to think about it yourself without accidentally seeing the answer): gur bccbfvgr bs gur pngrtbel bs svavgryl cerfragrq tebhcf.
The result of this exercise is true in more generality: it works for any finite-limit theory; see in particular Lawvere theory. Presumably there are also infinitary generalizations. There’s some general discussion in the Elephant.
Instead of a syntactic category, for a non-dependent type theory one can construct instead a syntactic cartesian multicategory (or, in the case of a linear type theory, a plain (symmetric) multicategory). This avoids the need to take the objects to be contexts rather than single types.
For some doctrines, the syntactic category of any theory is naturally equipped with the structure of a site. For instance, if is a regular, coherent, or geometric theory, then is a regular, coherent, or geometric category, which comes with a naturally defined topology. When equipped with this topology, the syntactic category is called the syntactic site.
In each of these cases, the category of sheaves on the syntactic site is the classifying topos of the theory. In other words, it has the universal property that for any Grothendieck topos , geometric morphisms are equivalent to models of the theory in .
Sections D4.1 and D4.4 of
A description of the construction of the category of contexts is in
Another description, via sketches, is in chapter VIII of
A review of this is around section 2.8 of