\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{syntactic category}

\hypertarget{context}{}\subsubsection*{{Context}}\label{context}

\hypertarget{topos_theory}{}\paragraph*{{Topos Theory}}\label{topos_theory}

[[!include topos theory - contents]]

\hypertarget{type_theory}{}\paragraph*{{Type theory}}\label{type_theory}

[[!include type theory - contents]]

\emph{Note: This page is about [[categories]] (in the sense of [[category theory]]) built out of [[syntax]], i.e. ``term models''. The phrase ``syntactic category'' is also sometimes used to mean a grouping of syntactic objects, so that e.g. [[terms]] belong to one syntactic category and [[formulas]] to another. For this usage, see also [[categorial grammar]].}

\hypertarget{contents}{}\section*{{Contents}}\label{contents}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definition}{Definition}\dotfill \pageref*{definition} \linebreak
\noindent\hyperlink{properties}{Properties}\dotfill \pageref*{properties} \linebreak
\noindent\hyperlink{structure}{Structure}\dotfill \pageref*{structure} \linebreak
\noindent\hyperlink{UniversalProperty}{Universal property}\dotfill \pageref*{UniversalProperty} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{SubstitutionAndIntroductionOfTerm}{Substitution and introduction of a single term}\dotfill \pageref*{SubstitutionAndIntroductionOfTerm} \linebreak
\noindent\hyperlink{group}{The theory of a group}\dotfill \pageref*{group} \linebreak
\noindent\hyperlink{variations}{Variations}\dotfill \pageref*{variations} \linebreak
\noindent\hyperlink{cartesian_multicategories}{Cartesian multicategories}\dotfill \pageref*{cartesian_multicategories} \linebreak
\noindent\hyperlink{the_syntactic_site}{The syntactic site}\dotfill \pageref*{the_syntactic_site} \linebreak
\noindent\hyperlink{related_concepts}{Related concepts}\dotfill \pageref*{related_concepts} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{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]]

\begin{displaymath}
Theories \;\rightleftarrows\; Categories
\end{displaymath}
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 closed category|cartesian closure]], etc.).

The \textbf{syntactic category} construction is the functor from theories to categories, denoted $Syn$ or $Con$. Given a theory, it generates the [[walking structure|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 \textbf{category of contexts}.

The functor in the other direction associates to any category its [[internal logic]].

\hypertarget{definition}{}\subsection*{{Definition}}\label{definition}

Given a [[type theory]] $T$, its \textbf{syntactic category} or \textbf{category of contexts} $Con(T)$ is defined as follows.

\begin{itemize}%
\item Its [[objects]] are the [[contexts]] in the type theory;


\item Its [[morphisms]] between contexts are \textbf{[[substitutions]]}, or \textbf{interpretations} of [[variables]].



\end{itemize}
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]] $T$ of the form

\begin{displaymath}
\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})
\end{displaymath}
and

\begin{displaymath}
\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})
  \,.
\end{displaymath}
(Here we allow the possibility that each type in these contexts [[dependent type|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)$ consists of a sequence of terms such as the following:

\begin{displaymath}
\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}
\end{displaymath}
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

\hypertarget{properties}{}\subsection*{{Properties}}\label{properties}

\hypertarget{structure}{}\subsubsection*{{Structure}}\label{structure}

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

\begin{itemize}%
\item If $T$ has [[function types]], then $Con(T)$ is [[cartesian closed category]].
\item If $T$ has [[sum types]], then $Con(T)$ has binary [[coproducts]].
\item If $T$ is a [[dependent type theory]] with [[dependent product types]], then $Con(T)$ is a [[locally cartesian closed category]].
\item If $T$ is a [[regular theory]], then $Con(T)$ is a [[regular category]].
\item If $T$ is a [[coherent theory]], then $Con(T)$ is a [[coherent category]].
\item If $T$ is a [[geometric theory]], then $Con(T)$ is a [[geometric category]].
\item If $T$ is a finitary [[first-order theory]], then $Con(T)$ is a [[Heyting category]].

\end{itemize}
And so on. (If $T$ lacks [[eta-conversion]], then this categorical structure may only be ``weak''.) One thing worth noting is that

\begin{itemize}%
\item $Con(T)$ always has finite [[products]].

\end{itemize}
This is due to the objects of $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)$ 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.

\hypertarget{UniversalProperty}{}\subsubsection*{{Universal property}}\label{UniversalProperty}

The syntactic category $Con(T)$ has the [[universal property]] that for $C$ any suitable category, [[functors]]

\begin{displaymath}
Con(T) \to C
\end{displaymath}
that preserve the relevant structure correspond to [[categorical semantics|interpretations]] of $T$ in $C$.

The construction

\begin{displaymath}
Con\colon TypeTheories \to Categories
\end{displaymath}
is the [[left adjoint]] in an [[adjunction]] that [[relation between type theory and category theory|relates type theories and categories]], whose [[right adjoint]] $Lan : Categories \to TypeTheories$ extracts the [[internal logic]] of a category.

Accordingly, the [[counit of an adjunction|adjunction counit]] evaluated on any category $C$

\begin{displaymath}
Con(Lan(C)) \to C
\end{displaymath}
says that there a canonical interpretation of the internal logic of a category $C$ in $C$ itself, while the [[unit of an adjunction|unit]] evaluated at a theory $T$:

\begin{displaymath}
T \to Lan(Con(T))
\end{displaymath}
says that there is a canonical interpretation of $T$ in the internal logic of its syntactic category.

\hypertarget{examples}{}\subsection*{{Examples}}\label{examples}

\hypertarget{SubstitutionAndIntroductionOfTerm}{}\subsubsection*{{Substitution and introduction of a single term}}\label{SubstitutionAndIntroductionOfTerm}

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

Given a [[term]] $t : X$ there is a canonical morphism of contexts

\begin{displaymath}
\Gamma \stackrel{[t/x]}{\to} [\Gamma, x : X]
\end{displaymath}
which picks that term in $X$. The [[base change]] functor along this morphism

\begin{displaymath}
[t/x]^* : Con(T)_{/[\Gamma, x : X]} \to Con(T)_{/\Gamma}
\end{displaymath}
is the operation of \emph{[[substitution]] of [[variables]]: it sends a [[dependent type]] $\Gamma, x : X \vdash P(x)$ to $\Gamma \vdash P(t)$.}

There is also the canonical morphism of contexts

\begin{displaymath}
\hat x : [\Gamma, x : X] \to \Gamma
\end{displaymath}
which simply forgets the type $X$. The [[base change]] along this morphism is the context extension functor

\begin{displaymath}
\hat x^* : Con(T)_{/\Gamma} \to Con(T)_{/[\Gamma , x : X]}
  \,.
\end{displaymath}
Its [[right adjoint]] is the [[dependent product]] functor $\prod_{x : X}$ giving the [[universal quantifier]] $\forall_{x : X}$, and its [[left adjoint]] is the [[dependent sum]] functor $\sum_{x : X}$ giving the [[existential quantifier]] $\exists_{x :X}$.

\hypertarget{group}{}\subsubsection*{{The theory of a group}}\label{group}

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

\begin{displaymath}
\Gamma \;=\; a\colon G,\; b\colon G
\end{displaymath}
\begin{displaymath}
\Delta \;=\; a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2
\end{displaymath}
\begin{displaymath}
E \;=\; a\colon G,\; b\colon G,\; a b = b a
\end{displaymath}
\begin{displaymath}
Z \;=\; x\colon G,\; y\colon G
\end{displaymath}
One interpretation of $\Gamma$ in $\Delta$ (that is, a morphism from $\Delta$ to $\Gamma$) is given by the substitution

\begin{displaymath}
a \coloneqq a,\; b \coloneqq b .
\end{displaymath}
The fact that $(a b)^2 = a^2 b^2$ in $\Delta$ is ignored. In type-theoretic language, this would consist of the two terms

\begin{displaymath}
\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}
\end{displaymath}
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

\begin{displaymath}
a \coloneqq b,\; b \coloneqq a .
\end{displaymath}
There is no reason to keep variable names the same. (At this point, compare $\Gamma$ and $Z$; when the definition is complete, it ought to follow that these are isomorphic.)

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

\begin{displaymath}
a \coloneqq a^2,\; b \coloneqq a^3 .
\end{displaymath}
Not only does this ignore that $(a b)^2 = a^2 b^2$; it also ignores the very existence of $b$ in $\Delta$. (It also uses the existence of $a$ more than once. Ignoring and reusing information like this is not always allowed in substructural logics such as [[linear logic]].)

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

\begin{displaymath}
a\colon G,\; b\colon G,\; (a b)^2 = a^2 b^2 \;\vdash\; a b = b a.
\end{displaymath}
That is, we get a morphism from $\Delta$ to $E$ by performing the substitution

\begin{displaymath}
a \coloneqq a,\; b \coloneqq b
\end{displaymath}
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 $E$ 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

\begin{displaymath}
a \coloneqq a,\; b \coloneqq a
\end{displaymath}
and then inserting a proof that

\begin{displaymath}
\Gamma \;\vdash\; (a a)^2 = a^2 a^2 .
\end{displaymath}
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)$ can be seen explicitly as well. First, given a context $\Gamma$, there is an obvious \textbf{[[identity morphism|identity]]} morphism where every variable is substituted for itself and every statement assumed is proved immediately from itself.

Given morphisms $\Gamma \overset{f}\to \Delta \overset{g}\to E$, form the \textbf{[[composite]]} as follows: First, for each variable $X$ required by $\Gamma$, $f$ tells us how to substitute a term $T$ built out of the variables in $\Delta$, while $g$ tells us how to substitute a term from $E$ for each of these variables. So in the end, $X$ is expressed as a term $T[g]$ involving variables available in $E$. Also, by combining the proofs provided by $f$ and $g$, 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 \textbf{[[equality|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 $X$ 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.

\begin{example}
\label{}\hypertarget{}{}
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 of categories|equivalence]]) in terms familiar to an algebraist. In particular, compare it to the [[Grp|category of groups]].

\end{example}
\begin{proof}
In \href{http://www.rot13.com/}{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.

\end{proof}
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]].

\hypertarget{variations}{}\subsection*{{Variations}}\label{variations}

\hypertarget{cartesian_multicategories}{}\subsubsection*{{Cartesian multicategories}}\label{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 logic|linear]] type theory, a plain (symmetric) [[multicategory]]). This avoids the need to take the objects to be contexts rather than single types.

\hypertarget{the_syntactic_site}{}\subsubsection*{{The syntactic site}}\label{the_syntactic_site}

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

\hypertarget{related_concepts}{}\subsection*{{Related concepts}}\label{related_concepts}

\begin{itemize}%
\item More or less the same concept is that of \emph{[[term model]]}.


\item [[free topos]]



\end{itemize}
\hypertarget{references}{}\subsection*{{References}}\label{references}

Sections D4.1 and D4.4 of

\begin{itemize}%
\item [[Peter Johnstone]], \emph{[[Sketches of an elephant]]},

\end{itemize}
A description of the construction of the category of contexts is in

\begin{itemize}%
\item Andrew Pitts, \emph{Categorical logic}, In Handbook of Logic in Computer Science, volume 5, pages 39--128. Oxford University Press (2001)

\end{itemize}
Another description, via [[sketches]], is in chapter VIII of

\begin{itemize}%
\item [[Paul Taylor]], \emph{[[Practical Foundations of Mathematics]]},

\end{itemize}
A review of this is around \href{http://www.paultaylor.eu/ASD/foufct/cattype.html}{section 2.8} of

\begin{itemize}%
\item [[Paul Taylor]], \emph{Foundations for computable topology} (\href{http://www.paultaylor.eu/ASD/foufct/abstract.html}{webpage})

\end{itemize}
[[!redirects syntactic category]] [[!redirects syntactic categories]] [[!redirects syntactic site]] [[!redirects syntactic sites]] [[!redirects category of contexts]] [[!redirects categories of contexts]]



\end{document}