\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*{generalized algebraic theory}

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

As described in Cartmell's \href{http://dx.doi.org/10.1016/0168-0072%2886%2990053-9}{Generalised Algebraic Theories and Contextual Categories}, a generalized algebraic theory (GAT) consists of:

\begin{enumerate}%
\item An \href{algebraic+theory}{algebraic theory} of sorts, which may itself be multi-sorted.


\item A collection of operations, each having zero or more arguments and one result. Each $n$-ary operation is also given with $(n+1)$-many \href{http://en.wikipedia.org/w/index.php?title=Universal_algebra&oldid=413212476#Derived_Operations}{derived operations} of the algebraic theory of sorts, all of the same arity, specifying the sort of each argument and the sort of the result.


\item Equations between pairs of derived operations\footnote{An $n$-ary derived operation of a GAT is defined in the same manner as a derived operation of a many-sorted algebra, except that it must also be given with $(n+1)$-many derived operations of the algebraic theory of sorts. Just as in many-sorted algebras, composition of operations is permitted only when the sorts match; in the GAT case those sorts must match for any choice of sort-algebra-derived-operation arguments.}  with the same arity and whose result sorts are provably equal in the algebraic theory of sorts (see example below).



\end{enumerate}
To avoid confusion, this article will refer to the sorts of the algebraic theory of sorts as ``supersorts'' (this convention is not used in Cartmell's paper).

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

The theory of categories is a GAT:

\begin{enumerate}%
\item Its algebraic theory of sorts is two-supersorted, with supersorts ``Ob'' and ``Mor'', and one binary operation ``Hom(-,+)'' with arguments of supersort ``Ob'' and result of supersort ``Mor''.


\item Its operations include:



\end{enumerate}
\begin{itemize}%
\item The unary operation $id(-)$ with argument sort given by the derived operation $x\mapsto x$ and result sort given by the derived operation $x\mapsto Hom(x,x)$.


\item The binary operation $comp(-,+)$ with first argument sort given by $x,y,z\mapsto Hom(x,y)$ and second argument sort given by $x,y,z\mapsto Hom(y,z)$ and result sort given by $x,y,z\mapsto Hom(x,z)$



\end{itemize}
\begin{enumerate}%
\item Its equations are

\end{enumerate}
\begin{itemize}%
\item $comp(id(a),f)=f$ where argument $a$ has sort $x,y\mapsto x$ and argument $f$ has sort $x,y\mapsto Hom(x,y)$


\item $comp(f,id(a))=f$ where argument $a$ has sort $x,y\mapsto y$ and argument $f$ has sort $x,y\mapsto Hom(x,y)$


\item $comp(f,comp(g,h))=comp(comp(f,g),h)$ where argument $f$ has sort $w,x,y,z\mapsto Hom(w,x)$, argument $g$ has sort $w,x,y,z\mapsto Hom(x,y)$ and argument $h$ has sort $w,x,y,z\mapsto Hom(y,z)$.



\end{itemize}
Note that this GAT has no equations imposed on the sort algebra.

One may also elect to include the following operations:

\begin{itemize}%
\item The unary operation $dom(-)$ with argument sort given by the derived operation $x,y\mapsto Hom(x,y)$ and result sort given by the derived operation $x,y\mapsto x$


\item The unary operation $cod(-)$ with argument sort given by the derived operation $x,y\mapsto Hom(x,y)$ and result sort given by the derived operation $x,y\mapsto y$



\end{itemize}
One can also directly axiomatize the theory of [[monoidal categories]] by adding:

\begin{enumerate}%
\item A 0-ary operation (constant) $I$ of supersort ``Ob'' to the algebraic theory of sorts.


\item A binary operation $-\otimes -$ whose arguments and result are of supersort ``Ob'' to the algebraic theory of sorts.


\item A fifth operation to the GAT having argument sort $x_1,y_1,x_2,y_2\mapsto Hom(x_1,y_1)$ and $x_1,y_1,x_2,y_2\mapsto
Hom(x_2,y_2)$ and result sort $x_1,y_1,x_2,y_2\mapsto Hom(x_1\otimes
x_2,y_1\otimes y_2)$


\item Operations for the left unitor (argument sort $x\mapsto x$, result sort $x\mapsto I\otimes x$) and its inverse.


\item Operations for the GAT for the right unitor (argument sort $x\mapsto x$, result sort $x\mapsto x\otimes I$) and its inverse.


\item Operations for the GAT for the associator (argument sort $x,y,z\mapsto x\otimes(y\otimes z)$, result sort $x,y,z\mapsto (x\otimes y)\otimes z$) and its inverse.


\item Quite a large number of additional equations corresponding to the pentagon and triangle diagrams, functoriality of the new fifth GAT operation, and inverse+naturality squares for remaining operations.



\end{enumerate}
This GAT also has no equations on the sort algebra.

I suspsect that you can do strict monoidal categories too (though I haven't worked it out completely) -- but that definitely requires sort equations. -- [[Adam]]

I think you can do [[multicategories]] too, but that requires infinitely many operations (in both the algebraic theory of sorts and the GAT itself) and infinitely many equations in the GAT. Even for finitary multicategories. -- [[Adam]]

Finally, one can axiomatize the theory of categories with [[finite limits]] as a GAT. This GAT, however, requires equations on the algebra of sorts.

\hypertarget{relationship_to_manysorted_algebraic_theories}{}\subsubsection*{{Relationship to Many-Sorted Algebraic Theories}}\label{relationship_to_manysorted_algebraic_theories}

A \href{http://ncatlab.org/nlab/show/algebraic+theory#multisorted_algebraic_theories_20}{many-sorted algebraic theory} is a GAT whose algebraic theory of sorts has no equations and no operations of arity greater than zero (i.e., has only constants).

\hypertarget{relationship_to_essentially_algebraic_theories}{}\subsubsection*{{Relationship to Essentially Algebraic Theories}}\label{relationship_to_essentially_algebraic_theories}

Cartmell's paper explains how, for every GAT there is an EAT with the same models and for every EAT there is a GAT with the same models. In this sense they are more or less equivalent in descriptive power.

Cartmell (sec 6)compares essentially algebraic theories to [[Cartesian logic]].

However (not in Cartmell's paper), there is no notion in the world of EAT's equivalent to a ``GAT without sort equations''. This is relevant because it yields an interpretation result. Just as the theory of finite-limit categories is an EAT, and one can interpret any EAT in a finite-limit category, so too is the theory of monoidal categories a GAT without sort equations, and one can interpret any\footnote{The GAT of monoidal categories (without dom+cod) has a nice property: the argument and result sorts of $comp$ are all the same, and we can get away with using the unit object $I$ of the interpreting category for all sorts of supersort $Ob$. I need to explain how to interpret GATs which lack this property -- those which have more than one supersort with nontrivial sorts. Here's a sketch: just as in the ``nice'' case the interpreting monoidal category $V$ will have an object for each sort of the GAT. Now construct a monoidal category $K$ with an object for each supersort and a morphism for each of the operations in the algebraic theory of sorts. If $V'$ is the subcategory of $V$ which does the interpretation, there ought to be a \href{Grothendieck+fibration}{Grothendieck-Street Fibration} of $V'$ over $K$ with the fibration functor sending each sort ($V$-object) to its supersort ($K$-object).}  GAT without sort equations in a monoidal category.

\hypertarget{relationship_to_enriched_categories}{}\subsubsection*{{Relationship to Enriched Categories}}\label{relationship_to_enriched_categories}

When one interprets the EAT of categories in a [[finite-limit category]] $V$, the result is a $V$-[[internal category]]. When one interprets the GAT of categories in a monoidal category $V$, the result is an $V$-[[enriched category]].

The theory of internal categories is an essentially algebraic theory (specifically, the theory for which a model is a category with a designated category internal to it). Likewise, the theory of enriched categories is a GAT without sort equations (specifically, the theory for which a model is a category with a category enriched in it).

\hypertarget{relationship_to_type_theory}{}\subsubsection*{{Relationship to Type Theory}}\label{relationship_to_type_theory}

Type theories with type operators and polymorphism but without dependent types (such as System \href{http://en.wikipedia.org/wiki/System_F#System_F.CF.89}{$F_\omega$} and the \href{http://haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#universal-quantification}{unbounded-rank polymorphic version} of the [[Haskell]] type system) can represent any GAT without sort equations, encoding the sorts of the GAT as types and the operations of the algebraic theory of sorts as type operations. Type theories without dependent types generally enjoy better \href{http://en.wikipedia.org/wiki/Type_inference#Hindley.E2.80.93Milner_type_inference_algorithm}{type inference} properties than those with dependent types, making them practical as programming languages.

\hypertarget{speculative}{}\subsubsection*{{Speculative}}\label{speculative}

Might there be such a thing as an $n$-GAT, where a $0$-GAT is an algebraic theory and an $(n+1)$-GAT is defined as above except that the sort algebra is an $n$-GAT rather than an algebra? -- [[Adam]]

I feel like there must be some sort of way to eliminate the notion of ``arity'' and put in its place an arbitrary (G)AT, recovering the original notion using the single-sorted Peano algebra (one constant ``0'', one unary operation ``S'', and no equations) or binary tree algebra (one constant ``0'', one binary operation ``B'', and no equations). But I can't quite put my finger on how to do it. -- [[Adam]]



\end{document}