Syntax in model in syntax

This short stub is an exercise in points of view. It briefly sketches something almost tautological—and yet important, see for instance this discussion—namely that

theorem1Almost-tautology The category of types of a type theory is equivalent to its syntactic display map category.

In what follows we fix a Martin-Löf type theory $T$ with $\Pi$, $\Sigma$ with definitional eta, and unit type . $T$ is (at first) meant to be treated syntactically, i.e. from a traditional proof theorist’s point of view, in terms of its judgments, axioms and logical rules.

definition2Syntactic display map category The syntactic display map category $\Syn$ of $T$ has contexts of $T$, formed from the empty context and context extension, as objects, and substitutions between contexts as arrows. Its display maps are the context projections $\Gamma, A \xtwoheadrightarrow{p_A} \Gamma$.

Pullbacks of display maps $\Gamma, A \xtwoheadrightarrow{p_A} \Gamma$ along $f \colon \Delta \rightarrow \Gamma$ are again display maps \[ \Delta, A[f/\Gamma] \xtwoheadrightarrow{p_A[f/\Gamma]} \Delta \] where $A[t/\Gamma]$ denotes the simultaneous substitution $A[t_1/x_1, \dotsc, t_n/x_n]$ for $\Gamma = (x_1 \colon \Gamma_1, \dotsc, x_n \colon \Gamma_n)$.

definition3Category of types The category of types $\Type$ of $T$ is the category of closed types of $T$ and functions between them.

The idea is that while definition (2) might seem more “external” or “semantic” in flavor and definition (3) more “internal” or “syntactically”-flavored, they are actually the same thing.

proof (of Theorem 1). Using a suggestive overloading of notation, we have the equivalences \[ \Syn \xrightleftarrows[\centerdot,]{\tilde\Sigma} \Type \] where $\tilde\Sigma$ is defined inductively on objects by and on arrows $f \colon \Gamma \rightarrow \Delta$ by where $f = (\Gamma \vdash f_1 \colon \Delta_1, \dotsc, f_m \colon \Delta_m)$. Note that we’re implicitly left-associative for convenience.

The inverse $\centerdot, \colon \Type \rightarrow \Syn$ is given by

Now we can check that $(\tilde\Sigma \circ \centerdot,)$ and $(\centerdot, \circ \tilde\Sigma)$ are both naturally isomorphic to the identity functors. For the latter, use and observe that definitional eta is needed for this to be an isomorphism in $\Syn$.

The purpose of this discussion is not to get bogged down in metatheoretic minutiae about syntax, but rather to gain an understanding of the internal language approach, such that one may switch back and forth between the internal syntax and the external categorical/model-theoretic point of view when performing constructions in type theory.