nLab
syntactic category

Context

Topos Theory

topos theory

Background

Toposes

Internal Logic

Topos morphisms

Extra stuff, structure, properties

Cohomology and homotopy

In higher category theory

Theorems

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

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecompositionsubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator 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

homotopy levels

semantics

Contents

Idea

As described at relation between type theory and category theory, for many kinds of logic and type theory there is an adjunction or equivalence

TheoriesCategories Theories \;\rightleftarrows\; Categories

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 SynSyn or ConCon. 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.

Definition

Given a type theory TT, its syntactic category or category of contexts Con(T)Con(T) is defined as follows.

A morphism from the context Γ\Gamma to the context Δ\Delta consists of a way of fulfilling the assumptions required by Δ\Delta by appropriately interpreting those provided by Γ\Gamma, generally by substituting terms available in Γ\Gamma for variables needed in Δ\Delta and proving whatever is necessary from the assumptions at hand.

More precisely, let Γ\Gamma and Δ\Delta be contexts of some type theory TT of the form

Γ=x 0:A 0,x 1:A 1(x 0),x 2:A 2(x 0,x 1),x n:A n(x 0,,x n1)\Gamma \;=\; x_0:A_0,\; x_1:A_1(x_0),\; x_2:A_2(x_0,x_1),\;\dots x_n:A_n(x_0,\dots,x_{n-1})

and

Δ=y 0:B 0,y 1:B 1(y 0),y 2:B 2(y 0,y 1),y m:B m(y 0,,y m1).\Delta \;=\; y_0:B_0,\; y_1:B_1(y_0),\; y_2:B_2(y_0,y_1),\;\dots y_m:B_m(y_0,\dots,y_{m-1}) \,.

(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 ΓΔ\Gamma \to \Delta in the category of contexts Con(T)Con(T) consists of a sequence of terms such as the following:

Γ t 0:B 0 Γ t 1:B 1(t 0) Γ t m:B m(t 0,t 1,,t m1) \begin{aligned} \Gamma &\vdash t_0 :B_0\\ \Gamma &\vdash t_1 : B_1(t_0)\\ \vdots\\ \Gamma &\vdash t_m : B_m(t_0,t_1,\dots, t_{m-1}) \end{aligned}

In other words, to give such a morphism we must give, for each type (or assumption) required by Δ\Delta, a way to construct an element of that type (or a proof of that assumption) out of the data and assumptions contained in Γ\Gamma.

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

Properties

Structure

Depending on the type-forming operations available in TT, the category Con(T)Con(T) will have categorical structure. Roughly:

And so on. (If TT lacks eta-conversion, then this categorical structure may only be “weak”.) One thing worth noting is that

  • Con(T)Con(T) always has finite products.

This is due to the objects of Con(T)Con(T) being contexts rather than types. A way to avoid this is to work instead with a syntactic cartesian multicategory.

In fact, Con(T)Con(T) 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.

Universal property

The syntactic category Con(T)Con(T) has the universal property that for CC any suitable category, functors

Con(T)C Con(T) \to C

that preserve the relevant structure correspond to interpretations of TT in CC.

The construction

Con:TypeTheoriesCategories Con\colon TypeTheories \to Categories

is the left adjoint in an adjunction that relates type theories and categories, whose right adjoint Lan:CategoriesTypeTheoriesLan : Categories \to TypeTheories extracts the internal logic of a category.

Accordingly, the adjunction counit evaluated on any category CC

Con(Lan(C))C Con(Lan(C)) \to C

says that there a canonical interpretation of the internal logic of a category CC in CC itself, while the unit evaluated at a theory TT:

TLan(Con(T)) T \to Lan(Con(T))

says that there is a canonical interpretation of TT in the internal logic of its syntactic category.

Examples

Substitution and introduction of a single term

Given a context Γ\Gamma and a type XX, there is a new context [Γ,x:X][\Gamma, x : X].

Given a term t:Xt : X there is a canonical morphism of contexts

Γ[t/x][Γ,x:X] \Gamma \stackrel{[t/x]}{\to} [\Gamma, x : X]

which picks that term in XX. The base change functor along this morphism

[t/x] *:Con(T) /[Γ,x:X]Con(T) /Γ [t/x]^* : Con(T)_{/[\Gamma, x : X]} \to Con(T)_{/\Gamma}

is the operation of substitution of variables: it sends a dependent type Γ,x:XP(x)\Gamma, x : X \vdash P(x) to ΓP(t)\Gamma \vdash P(t).

There is also the canonical morphism of contexts

x^:[Γ,x:X]Γ \hat x : [\Gamma, x : X] \to \Gamma

which simply forgets the type XX. The base change along this morphism is the context extension functor

x^ *:Con(T) /ΓCon(T) /[Γ,x:X]. \hat x^* : Con(T)_{/\Gamma} \to Con(T)_{/[\Gamma , x : X]} \,.

Its right adjoint is the dependent product functor x:X\prod_{x : X} giving the universal quantifier x:X\forall_{x : X}, and its left adjoint is the dependent sum functor x:X\sum_{x : X} giving the existential quantifier x:X\exists_{x :X}.

The theory of a group

For example, consider these contexts in the theory of a group GG:

Γ=a:G,b:G \Gamma \;=\; a\colon G,\; b\colon G
Δ=a:G,b:G,(ab) 2=a 2b 2 \Delta \;=\; a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2
E=a:G,b:G,ab=ba E \;=\; a\colon G,\; b\colon G,\; a b = b a
Z=x:G,y:G Z \;=\; x\colon G,\; y\colon G

One interpretation of Γ\Gamma in Δ\Delta (that is, a morphism from Δ\Delta to Γ\Gamma) is given by the substitution

aa,bb. a \coloneqq a,\; b \coloneqq b .

The fact that (ab) 2=a 2b 2(a b)^2 = a^2 b^2 in Δ\Delta is ignored. In type-theoretic language, this would consist of the two terms

a:G,b:G,(ab) 2=a 2b 2 a:G a:G,b:G,(ab) 2=a 2b 2 b:G\begin{aligned} a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2 &\vdash a:G\\ a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2 &\vdash b:G \end{aligned}

Note that in this way of presenting things, the names of the variables in Γ\Gamma do not appear; only the order in which the types appear in Γ\Gamma matters.

A less obvious interpretation of Γ\Gamma in Δ\Delta is the substitution

ab,ba. a \coloneqq b,\; b \coloneqq a .

There is no reason to keep variable names the same. (At this point, compare Γ\Gamma and ZZ; when the definition is complete, it ought to follow that these are isomorphic.)

Another, perhaps even less obvious, morphism ΔΓ\Delta \to \Gamma is

aa 2,ba 3. a \coloneqq a^2,\; b \coloneqq a^3 .

Not only does this ignore that (ab) 2=a 2b 2(a b)^2 = a^2 b^2; it also ignores the very existence of bb in Δ\Delta. (It also uses the existence of aa more than once. Ignoring and reusing information like this is not always allowed in substructural logics such as linear logic.)

We can interpret EE in Δ\Delta without renaming variables because the theory of a group allows us to derive the judgment

a:G,b:G,(ab) 2=a 2b 2ab=ba. a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2 \;\vdash\; a b = b a.

That is, we get a morphism from Δ\Delta to EE by performing the substitution

aa,bb a \coloneqq a,\; b \coloneqq b

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 Δ\Delta and EE are also isomorphic.

Are there any morphisms from Γ\Gamma to Δ\Delta? The obvious substitution does not define a morphism, since the required fact cannot be proved. However, you get one using the substitution

aa,ba a \coloneqq a,\; b \coloneqq a

and then inserting a proof that

Γ(aa) 2=a 2a 2. \Gamma \;\vdash\; (a a)^2 = a^2 a^2 .

All the same, we would not want to say that Γ\Gamma and Δ\Delta are isomorphic contexts; although there are morphisms in each direction, composing them should never produce identity morphisms on both sides.

The category structure of Con(T)Con(T) can be seen explicitly as well. First, given a context Γ\Gamma, there is an obvious identity morphism where every variable is substituted for itself and every statement assumed is proved immediately from itself.

Given morphisms ΓfΔgE\Gamma \overset{f}\to \Delta \overset{g}\to E, form the composite as follows: First, for each variable XX required by Γ\Gamma, ff tells us how to substitute a term TT built out of the variables in Δ\Delta, while gg tells us how to substitute a term from EE for each of these variables. So in the end, XX is expressed as a term T[g]T[g] involving variables available in EE. Also, by combining the proofs provided by ff and gg, we get the proofs required for their composite.

To really complete the definition of a category, I should also describe when two morphisms ΓΔ\Gamma \to \Delta 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 XX in Γ\Gamma can be proved equal in the context Δ\Delta.

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.

Exercise

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.

Answer

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.

Variations

Cartesian multicategories

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.

The syntactic site

For some doctrines, the syntactic category of any theory is naturally equipped with the structure of a site. For instance, if TT is a regular, coherent, or geometric theory, then Con(T)Con(T) 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 \mathcal{E}, geometric morphisms Sh(Con(T))\mathcal{E} \to Sh(Con(T)) are equivalent to models of the theory TT in \mathcal{E}.

References

Sections D4.1 and D4.4 of

A description of the construction of the category of contexts is in

  • Andrew Pitts, Categorical logic, In Handbook of Logic in Computer Science, volume 5, pages 39–128. Oxford University Press (2001)

Another description, via sketches, is in chapter VIII of

A review of this is around section 2.8 of

Revised on September 23, 2012 14:42:37 by Urs Schreiber (89.204.137.161)