\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*{categorical model of dependent types}

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

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

[[!include type theory - contents]]

\hypertarget{category_theory}{}\paragraph*{{Category theory}}\label{category_theory}

[[!include category theory - contents]]

\hypertarget{categorical_models_of_dependent_types}{}\section*{{Categorical models of dependent types}}\label{categorical_models_of_dependent_types}

\noindent\hyperlink{idea}{Idea}\dotfill \pageref*{idea} \linebreak
\noindent\hyperlink{definitions}{Definitions}\dotfill \pageref*{definitions} \linebreak
\noindent\hyperlink{comprehension_categories}{Comprehension categories}\dotfill \pageref*{comprehension_categories} \linebreak
\noindent\hyperlink{display_map_categories}{Display map categories}\dotfill \pageref*{display_map_categories} \linebreak
\noindent\hyperlink{categories_with_attributes}{Categories with attributes}\dotfill \pageref*{categories_with_attributes} \linebreak
\noindent\hyperlink{categories_with_families}{Categories with families}\dotfill \pageref*{categories_with_families} \linebreak
\noindent\hyperlink{natural_models}{Natural Models}\dotfill \pageref*{natural_models} \linebreak
\noindent\hyperlink{contextual_categories_or_csystems}{Contextual categories, or C-systems}\dotfill \pageref*{contextual_categories_or_csystems} \linebreak
\noindent\hyperlink{examples}{Examples}\dotfill \pageref*{examples} \linebreak
\noindent\hyperlink{syntactic_categories}{Syntactic categories}\dotfill \pageref*{syntactic_categories} \linebreak
\noindent\hyperlink{splitting_fibrations}{Splitting fibrations}\dotfill \pageref*{splitting_fibrations} \linebreak
\noindent\hyperlink{universes}{Universes}\dotfill \pageref*{universes} \linebreak
\noindent\hyperlink{simple_fibrations}{Simple fibrations}\dotfill \pageref*{simple_fibrations} \linebreak
\noindent\hyperlink{related_pages}{Related pages}\dotfill \pageref*{related_pages} \linebreak
\noindent\hyperlink{references}{References}\dotfill \pageref*{references} \linebreak


\hypertarget{idea}{}\subsection*{{Idea}}\label{idea}

In the [[relation between type theory and category theory]], [[dependent types]] are said to correspond to morphisms regarded as indexed families. That is, if a [[type]] $A$ corresponds to an [[object]] in some [[category]], then a [[dependent type]]

\begin{displaymath}
(x:A) \;\vdash\; (B(x) \;type)
\end{displaymath}
corresponds to a [[morphism]] $B\to A$ in that category. We think of this morphism as a [[bundle]] or [[fibration]], whose [[fiber]] over $x:A$ is the type $B(x)$. We can then say that [[type former|type forming operations]] such as [[dependent sum type]] and [[dependent product type]] correspond to category-theoretic operations of [[dependent sum]] and [[dependent product]].

However, this correspondence is not quite precise; in the case of dependent types there are extra [[coherence]] issues. [[substitution|Substitution]] in [[type theory]] should correspond to [[pullback]] in [[category theory]] (but see at \emph{\href{substitution#CategoricalSemantics}{substitution -- Categorical semantics}} for more); that is, given a term

\begin{displaymath}
(y:C) \;\vdash\; (f(y) : A)
\end{displaymath}
corresponding to a morphism $f:C\to A$, the substituted dependent type

\begin{displaymath}
(y:C) \;\vdash\; (B(f(y)) \;type)
\end{displaymath}
should correspond to the pullback of $B\to A$ along $f$. However, substitution in type theory is strictly [[associativity|associative]]. That is, given also $g:D\to C$, the dependent type

\begin{displaymath}
(z:D) \;\vdash\; (B(f(g(z))) \;type)
\end{displaymath}
is [[equality|syntactically the same]] regardless of whether we obtain it by substituting $y \coloneqq g(z)$ into $B(f(y))$, or $x \coloneqq f(g(z))$ into $B(x)$. In category theory, however, pullback is not generally strictly associative, so there is a mismatch. Similarly, every [[type formation rule|type-forming operation]] must also be strictly preserved by substitition/pullback.

The way this is generally dealt with is to introduce a category-theoretic structure which does have a ``substitution'' operation which is strictly associative, hence does correspond directly to type theory, and then show that any category can be ``strictified'' into such a stricter structure. Unfortunately, there are many different such structures which have been used, differing only slightly. On this page we define and compare them all.

One of these structures is called ``contextual categories'' (definition \ref{ContextualCategory} below).

 This and other kinds of categories-with-extra-structure may hence be thought of as stand-ins for the [[syntax]] of a [[type theory]]:

\begin{quote}%
Rather than constructing an interpretation of the syntax directly, we may work via the intermediary notion of contextual categories, a class of algebraic objects abstracting the key structure carried by the syntax. The plain definition of a contextual category corresponds to the structural core of the syntax; further syntactic rules (logical constructors, etc.) correspond to extra algebraic structure that contextual categories may carry. Essentially, contextual categories provide a completely equivalent alternative to the syntactic presentation of type theory.

Why is this duplication of notions desirable? The trouble with the syntax is that it is mathematically tricky to handle. Any full presentation must account for (among other things) variable binding, capture-free substitution, and the possibility of multiple derivations of a judgement; and so a direct interpretation must deal with all of these, at the same time as tackling the details of the particular model in question. By passing to contextual categories, one deals with these subtleties and bureaucracy once and for all, and obtains a clear framework for subsequently constructing models. Conversely, why not work only with contextual categories, dispensing with syntax entirely?

The trouble on this side is that working with higher-order logical structure in contextual categories quickly becomes unreadable. The reader preferring to take contextual categories as primary may regard the syntax as essentially a notation for working within them: a powerful, flexible, and intuitive notation, but one whose validity requires non-trivial work to establish. (The situation is comparable to that of string diagrams, as used in monoidal and more elaborately structured categories.)

(from \hyperlink{KapulkinLumsdaine12}{Kapulkin-Lumsdaine 12})


\end{quote}
\hypertarget{definitions}{}\subsection*{{Definitions}}\label{definitions}

In all the definitions, $C$ will be a [[category]]. Generally, we will regard the objects of $C$ as [[contexts]] in a type theory.

So far, we do not assume anything about $C$ as a category. Usually, one at least wants $C$ to have a [[terminal object]], representing the empty context, although this is not always included in the definitions. The additional structures we impose on $C$ below will imply in particular that certain [[pullbacks]] exist in $C$.

Sometimes, we want to consider $C$ as a [[strict category]], that is, we consider its objects up to [[equality]] rather than [[isomorphism]]. However, for most of the definitions below (until we get to contextual categories), it is still sensible to treat $C$ in an ordinary category-theoretic way, with the strictness living in the additional structure.

All of this could be made more precise by assembling the structures considered below into [[categories]], [[2-categories]], and/or [[strict 2-categories]].

\hypertarget{comprehension_categories}{}\subsubsection*{{Comprehension categories}}\label{comprehension_categories}

\begin{defn}
\label{ComprehensionCategory}\hypertarget{ComprehensionCategory}{}
A \textbf{comprehension category} consists of a strictly [[commuting diagram|commutative triangle]] of [[functors]]

\begin{displaymath}
\itexarray{ E && \to && C^I\\ & \searrow && \swarrow {\scriptsize cod} \\ && C }
\end{displaymath}
where $C^I$ is the [[arrow category]] of $C$ and $cod \colon C^I \to C$ denotes the codomain projection (which is a [[codomain fibration|fibration]] if $C$ has pullbacks), and such that

\begin{enumerate}%
\item $E\to C$ is a [[Grothendieck fibration]],


\item $E\to C^I$ takes [[cartesian morphisms]] in $E$ to cartesian morphisms in $C^I$ (i.e. to [[pullback]] squares in $C$).



\end{enumerate}
\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
In def \ref{ComprehensionCategory} we do not ask that $C^I \to C$ be a [[Grothendieck fibration|fibration]] (that would require $C$ to have all [[pullbacks]]), only that the \emph{particular} morphisms in the image of $E$ are cartesian.

\end{remark}
\begin{defn}
\label{FullAndSplitComprehensionCategory}\hypertarget{FullAndSplitComprehensionCategory}{}
A comprehension category (def. \ref{ComprehensionCategory}) is called

\begin{itemize}%
\item \textbf{full} if $E\to C^I$ is a [[fully faithful functor]].


\item \textbf{split} if $E\to C$ is a [[split fibration]].



\end{itemize}
In the latter case, we must consider $E$ at least to be a [[strict category]] (that is, we consider its objects up to equality rather than isomorphism) for the notion to make sense.

\end{defn}
\begin{remark}
\label{MeaningOfComprehensionCategory}\hypertarget{MeaningOfComprehensionCategory}{}
The interpretation of def. \ref{ComprehensionCategory} is as follows:

In a comprehension category, we may regard the objects of $C$ as [[contexts]], and the [[fiber]] $E^\Gamma$ of $E\to C$ over an object $\Gamma$ as the category of [[dependent types]] in context $\Gamma$. If the comprehension category is split (def. \ref{FullAndSplitComprehensionCategory}), then such dependent types have strictly [[associativity|associative]] [[substitution]].

The functor $E\to C^I$ assigns to each ``type $A$ in context $\Gamma$'' a new context which we think of as $\Gamma$ \emph{extended} by a fresh [[variable]] of type $A$, and write as $\Gamma.A$. This new context $\Gamma.A$ comes with a projection $\Gamma.A\to \Gamma$ (which forgets the fresh variable), and all substitutions in $E$ are realized as pullbacks in $C$.

\end{remark}
\hypertarget{display_map_categories}{}\subsubsection*{{Display map categories}}\label{display_map_categories}

\begin{defn}
\label{DisplayMapCategory}\hypertarget{DisplayMapCategory}{}
A \textbf{[[display map category]]} consists of a [[category]] $C$ together with a [[class]] $D$ of [[morphisms]] in $C$, called \emph{[[display maps]]}, such that all [[pullbacks]] of display maps exist and are themselves display maps.

\end{defn}
If $C$ is a display map category, then by defining $E$ to be the [[full subcategory]] of $C^I$ whose objects are display maps, we obtain a full comprehension category (def. \ref{FullAndSplitComprehensionCategory}). Thus, we have:

\begin{lemma}
\label{DMCasCmpC}\hypertarget{DMCasCmpC}{}
Display map categories (def. \ref{DisplayMapCategory}) may be identified with those comprehension categories, def. \ref{ComprehensionCategory}, for which the functor $E\to C^I$ is the inclusion of a [[full subcategory]].

\end{lemma}
\begin{remark}
\label{}\hypertarget{}{}
Working up to [[equivalence of categories]], as is usual in [[category theory]], it is natural to consider display map categories to also be equivalent to \emph{full} comprehension categories, def. \ref{FullAndSplitComprehensionCategory}, (those where $E\to C^I$ is merely fully faithful).

However, this breaks down when we are interested in \emph{split} comprehension categories, def. \ref{FullAndSplitComprehensionCategory}, for modeling substitution with strict associativity, since then $E$ at least must be regarded as a [[strict category]] and considered up to [[isomorphism]] rather than equivalence. Thus, display map categories may be said to be equivalent to non-split full comprehension categories, but ``split display map categories'' are not equivalent to split full comprehension categories. (In fact, split display map categories are not very useful; usually in order to make pullbacks strictly associative we have to introduce extra ``names'' for the same objects.)

\end{remark}
\hypertarget{categories_with_attributes}{}\subsubsection*{{Categories with attributes}}\label{categories_with_attributes}

\begin{defn}
\label{CategoryWithAttributes}\hypertarget{CategoryWithAttributes}{}
A \textbf{category with attributes} is a comprehension category, def. \ref{ComprehensionCategory}, for which $E\to C$ is a [[discrete fibration]].

\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
That is, in a category with attributes (def. \ref{CategoryWithAttributes}) we demand only that each context comes with a [[set]] of [[dependent types]] in that context, rather than a category of such. The intent is that the morphisms between two types in context $\Gamma$ should be determined by the morphisms in $C$ between the extended contexts over $\Gamma$.

Another way to convey this same intent with a comprehension category would be to ask that it be \emph{full}, def. \ref{FullAndSplitComprehensionCategory}, i.e. that the functor $E\to C^I$ be fully faithful.

\end{remark}
In fact, any category with attributes gives rise to a full comprehension category by factoring the functor $E\to C^I$ into a [[bijective on objects functor]] followed by a [[fully faithful functor]]. In this way, we obtain:

\begin{lemma}
\label{CWAasCmpC}\hypertarget{CWAasCmpC}{}
The category $\mathbf{CwA}$ of categories with attributes (def. \ref{CategoryWithAttributes}) is equivalent to the category of $\mathbf{CompCat}_{\text{full,split}}$ of full split comprehension categories (def. \ref{FullAndSplitComprehensionCategory}).

(These are, however, quite different as subcategories of $\mathbf{CompCat}$.)

\end{lemma}
\hypertarget{categories_with_families}{}\subsubsection*{{Categories with families}}\label{categories_with_families}

A category with attributes specifies for each ``context'' only a set of ``types'' in that context. A comprehension category, by contrast, specifies a whole \emph{category} of ``types'' in each context. If $A,B\in E^\Gamma$, then we may think of a morphism $f:A\to B$ in $E^\Gamma$ as a term

\begin{equation}
(\vec{x} : \Gamma), (a:A(\vec{x})) \;\vdash\; (f(\vec{x},a) : B(\vec{x}))
\label{cmpcterm}\end{equation}
in type theory.\newline A \emph{category with families} specifies instead, for each context and each type in that context, a set of ``terms belonging to that type''. These should be thought of as terms

\begin{equation}
(\vec{x} : \Gamma) \;\vdash\; (f(\vec{x}) : B(\vec{x}))
\label{cwfterm}\end{equation}
in type theory.

\begin{remark}
\label{}\hypertarget{}{}
A [[term]] of the form \eqref{cmpcterm} can equivalently be regarded as a term of the form \eqref{cwfterm} by replacing $\Gamma$ by the extended context $\Gamma.A$, and $B$ by its substitution along the projection $\Gamma.A \to \Gamma$.

\end{remark}
The additional insight in the following definition is that if we expect all of these terms to be determined by the morphisms in $C$, as in a category with attributes or a full comprehension category, then instead of specifying the functor $E\to C^I$ and then asking either that it be fully faithful or that $E$ be discrete (removing the information about extra morphisms in $E$), if we specify the terms of the form \eqref{cwfterm}, then the functor $E\to C^I$ is determined by a universal property.

Let $Fam$ denote the category of families of sets. Its objects are set-indexed families $(A_i)_{i\in I}$, and its morphisms $(A_i)_{i\in I} \to (B_j)_{j\in J}$ consist of a function $f\colon I\to J$ and functions $g_i \colon A_i \to B_{f(i)}$. We can equivalently, of course, regard this as the arrow category $Set^I$ of [[Set]], where $(B_j)_{j\in J}$ corresponds to the arrow $\coprod B \to J$.

\begin{defn}
\label{CategoryWithFamilies}\hypertarget{CategoryWithFamilies}{}
A \textbf{category with families} is a category $C$ together with

\begin{itemize}%
\item A functor $F:C^{op} \to Fam$, written $F(\Gamma) = (Tm(A))_{A\in Ty(\Gamma)}$.


\item For each $\Gamma\in C$ and $A\in Ty(\Gamma)$, a [[representing object]] for the functor

\begin{displaymath}
\begin{aligned}
  (C/\Gamma)^{op} & \to Set\\
  (\Delta \xrightarrow{f} \Gamma) & \mapsto Tm(f^*(A))
\end{aligned}
\end{displaymath}


\end{itemize}
\end{defn}
Intuitively, $F(\Gamma)$ is the set of terms in the context $\Gamma$ indexed by their type, and the representing object for the map $(C/\Gamma)^{op} \to Set$ is the context $\Gamma; A$.

We can then prove:

\begin{lemma}
\label{CwAareCwF}\hypertarget{CwAareCwF}{}
Categories with attributes, def. \ref{CategoryWithAttributes} are equivalent to categories with families, def. \ref{CategoryWithFamilies}.

\end{lemma}
\begin{proof}
Given a category with families, let $E\to C$ be the [[Grothendieck construction]] of the functor $Ty:C^{op}\to Set$, and let $E\to C^I$ take each $A\in Ty(\Gamma)$ to the above representing object. This is a category with attributes.

Conversely, given a category with attributes, let $Ty:C^{op}\to Set$ be the functor corresponding to the discrete fibration $E\to C$, and for $A\in Ty(\Gamma)$ let $Tm(A)$ be the set of [[sections]] of the morphism in $C$ that is the image of $A$ in $C^I$. These constructions are inverses up to isomorphism.

\end{proof}
\hypertarget{natural_models}{}\subsubsection*{{Natural Models}}\label{natural_models}

[[Steve Awodey]] (\hyperlink{Awodey2018}{Awodey 2018}) presented the following ``natural model'' of type theory as an alternative to categories with families.

\begin{theorem}
\label{}\hypertarget{}{}
If we modify Def. \ref{CategoryWithFamilies} by requiring only that the functors $(\Delta \xrightarrow{f} \Gamma) \mapsto Tm(f^*(A))$ be representable (rather than equipped with representing objects), then it is equivalent to giving

\begin{enumerate}%
\item a category $C$, together with
\item a morphism $Tm \to Ty$ in the category of [[presheaves]] on $C$ which is a [[representable morphism]].

\end{enumerate}
\end{theorem}
The category $C$ models the category of contexts and substitutions, and the morphism $Tm \to Ty$ models the bundle of (context-dependent) terms over (context-dependent) types. The representability models the extension of a context with a new typed variable.

The condition of being a representable morphism can be reformulated in terms of representable profunctors as follows. A natural model consists of

\begin{enumerate}%
\item a category $C$,
\item a presheaf $Ty : \hat C$ of types in context.
\item a presheaf $Tm : \widehat {\int Ty}$ of typed terms in context.
\item a functor $ext : \widehat {\int Ty} \to C$ of context extension with data that represents the profunctor ${\int Ty}(ty-,=) \odot C(-,ctx(ty(=))) : \int Ty &#8696; C$ where $ty : \int Tm \to \int Ty$ and $ctx : \int Ty \to C$ are the projections of the [[Grothendieck construction]].

\end{enumerate}
Writing the profunctor as P, it is equivalent to the following definition:

\begin{displaymath}
P(\Delta, (\Gamma, A)) = (\gamma : \Delta \to \Gamma) \times (a : Tm(\Delta, A[\gamma]))
\end{displaymath}
then the universal property of the context extension is that there is a natural isomorphism $\Delta \to ext(\Gamma, A) \cong P(\Delta,(\Gamma,A))$

\hypertarget{contextual_categories_or_csystems}{}\subsubsection*{{Contextual categories, or C-systems}}\label{contextual_categories_or_csystems}

Recall that

\begin{defn}
\label{NotationForExtendedContexts}\hypertarget{NotationForExtendedContexts}{}
If $C$ is a [[comprehension category]] (def. \ref{ComprehensionCategory}), $\Gamma\in C$ is a ``context'' and $A\in E^\Gamma$ is a ``type'' in context $\Gamma$, then we denote by $\Gamma.A$ the ``extended context'' in $C$ (remark \ref{MeaningOfComprehensionCategory}).

\end{defn}
\begin{defn}
\label{ContextualCategory}\hypertarget{ContextualCategory}{}
A \textbf{contextual category} (\hyperlink{Cartmell86}{Cartmell 86}, \hyperlink{Streicher91}{Streicher 91}) or \textbf{C-system} (\hyperlink{Voevodsky15a}{Voevodsky 15}) is a category with attributes $C$ (def. \ref{CategoryWithAttributes}) together with a \emph{length function} $\ell : ob(C) \to \mathbb{N}$ such that

\begin{enumerate}%
\item There is a unique object of length $0$, which is a [[terminal object]].
\item For any $\Gamma\in C$ and $A\in E^\Gamma$, we have $\ell(\Gamma.A) = \ell(\Gamma)+1$.
\item For any $\Delta\in C$ with $\ell(\Delta)\gt 0$, there exists a unique $\Gamma\in C$ and $A\in E^\Gamma$ such that $\Delta = \Gamma.A$ (with notation as in def. \ref{NotationForExtendedContexts}).

\end{enumerate}
\end{defn}
\begin{remark}
\label{}\hypertarget{}{}
Since def. \ref{ContextualCategory} refers to [[equality]] of objects, a contextual category $C$ must be a [[strict category]].

\end{remark}
\begin{remark}
\label{}\hypertarget{}{}
The idea which distinguishes a contextual category is that ``every context must be built out of types'' in a unique way.

\end{remark}
This makes for the closest match with type theory; in fact we have:

\begin{theorem}
\label{CxtCareTT}\hypertarget{CxtCareTT}{}
The category of contextual categories, def. \ref{ContextualCategory}, and (strictly) structure-preserving functors is [[equivalence of categories|equivalent]] to the [[category of dependent type theories and interpretations]].

\end{theorem}
\begin{remark}
\label{}\hypertarget{}{}
Since contextual categories are [[strict categories]], the category of such is really a [[1-category]], or perhaps a [[strict 2-category]].

\end{remark}
\begin{example}
\label{ContextualFromAttributes}\hypertarget{ContextualFromAttributes}{}
Given any category with attributes $C$, def. \ref{CategoryWithAttributes}, possessing a [[terminal object]], there is a canonical way to build a contextual category $cxt(C)$, def. \ref{ContextualCategory}, from it.

\begin{enumerate}%
\item Choose a [[terminal object]] $1\in C$ (the resulting contextual category does not depend on this choice, up to isomorphism).


\item The [[objects]] of $cxt(C)$ are the finite [[lists]]

\begin{displaymath}
(A_0,A_1,\dots,A_n)
\end{displaymath}
such that $A_0 \in E^1$ and $A_{k+1} \in E^{1.A_0.A_1.\cdots .A_k}$ for all $k$.


\item The [[morphisms]] $(A_0,\dots,A_n) \to (B_0,\dots,B_m)$ in $cxt(C)$ are the morphisms $1.A_0.A_1.\cdots.A_n \to 1.B_0.B_1.\cdots.B_m$ in $C$.



\end{enumerate}
All the rest of the structure on $cxt(C)$ is induced in an evident way from $C$.

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

Comprehension categories and display map categories are easy to come by ``in nature'', but it is more difficult to find examples of the ``split'' versions of the above structure (which are what is needed for modeling type theory). Here we summarize some basic known constructions.

However, first we should mention the examples that come from type theory itself.

\hypertarget{syntactic_categories}{}\subsubsection*{{Syntactic categories}}\label{syntactic_categories}

\begin{example}
\label{}\hypertarget{}{}
The [[syntactic category]] of any [[dependent type theory]] has all of the above structures. Its objects are [[contexts]] in the theory, and the types in context $\Gamma$ form the set or category $E^\Gamma$. The strict associativity of substitution in type theory makes this fibration automatically split.

\end{example}
\hypertarget{splitting_fibrations}{}\subsubsection*{{Splitting fibrations}}\label{splitting_fibrations}

There are standard constructions which can replace any [[Grothendieck fibration]] by an equivalent [[split fibration]]. Therefore,

\begin{example}
\label{FromComprehensionToContextual}\hypertarget{FromComprehensionToContextual}{}
Given any comprehension category, def. \ref{ComprehensionCategory},

\begin{enumerate}%
\item we may replace it by a split comprehension category, def. \ref{FullAndSplitComprehensionCategory},


\item then consider the underlying category with attributes, def. \ref{CategoryWithAttributes},


\item and finally pass to a contextual category by the construction in example \ref{ContextualFromAttributes}.



\end{enumerate}
\end{example}
Of course, comprehension categories are easy to come by; perhaps they arise most commonly as [[display map categories]]. For instance, if $C$ has all [[pullbacks]], then we can take all maps to be [[display maps]]. If $C$ is a [[category of fibrant objects]], we can take the [[fibrations]] to be the display maps.

So, for the record, we have in particular:

\begin{example}
\label{TypeTheoryModelFromLocallyCartesianClosedCategory}\hypertarget{TypeTheoryModelFromLocallyCartesianClosedCategory}{}
For $C$ a [[locally cartesian closed category]] $C$, it becomes a model for [[dependent type theory]] by regarding its [[codomain fibration]] $C^I \to C$ as a comprehension category, def. \ref{ComprehensionCategory}, and then strictifying that as in example \ref{FromComprehensionToContextual}.

\end{example}
\begin{remark}
\label{}\hypertarget{}{}
It turns out that for modeling additional [[type-forming operations]], however, not all splitting constructions are created equal.

Given $E\to C$, one classical construction (due to [[John Power]]) defines $E'\to C$, where an object of $E'$ over $\Gamma\in C$ consists of a morphism $f:\Gamma \to \Delta$ in $C$ along with an object $A$ of $E$ over $\Delta$. Type-theoretically, we can regard $(f,A)$ as a type $A$ with a ``delayed substitution'' $f$. This produces a split fibration (the chosen cartesian arrows are given by composition of morphisms in $C$), but it seems impossible to define dependent sums and products on it in a strict way.

A better choice is a construction due to [[Benabou]], which defines the objects of $E'$ over $\Gamma\in C$ to be functors $C/\Gamma \to E$ over $C$ which map every morphism of $C/\Gamma$ to a cartesian arrow. Type-theoretically, we can think of such an object as a type together with \emph{specified} compatible substitutions along any possible morphism. That type-formers may be extended in this case was proven by [[Martin Hofmann]] for [[dependent sums]] and [[dependent products]] and [[extensional type theory|extensional]] [[identity types]], and by [[Michael Warren]] in the case of [[intensional type theory|intensional]] [[identity types]] (but not for the [[term elimination|eliminator]]).

\end{remark}
\hypertarget{universes}{}\subsubsection*{{Universes}}\label{universes}

Suppose given a particular morphism $p:\widetilde{U} \to U$ in $C$. We can then define a category with attributes, def. \ref{CategoryWithAttributes}, as follows: the discrete fibration $E\to C$ corresponds to the representable presheaf $C(-,U)$, and the functor $E\to C^I$ is defined by pullback of $p$. We are thus treating $U$ as a ``[[universe]]'' of types. We may then of course pass to a contextual category, via example \ref{FromComprehensionToContextual}.

Type-forming operations may be extended strictly in this case by performing them once in the ``universal'' case, then acting by composition. This construction is due to [[Voevodsky]]. It also meshes quite well with type theories that contain internal universes -- a [[type of types]]-- , and in particular for modeling the [[univalence axiom]].

Particular important universes include:

\begin{itemize}%
\item Any [[Grothendieck universe]] in [[Set]], or more generally a [[universe in a topos]]. The resulting display maps are those with ``$U$-small fibers''.


\item In the category [[Gpd]], the groupoid of small groupoids. The resulting display maps are the [[split opfibrations]] with small fibers. Similarly, we can consider the groupoid of small sets, whose display maps are the [[discrete opfibrations]] with small fibers.


\item In the category [[sSet]] of [[simplicial sets]], there is a [[universal Kan fibration]] $p:\widetilde{U} \to U$ which classifies all [[Kan fibrations]] with small fibers.



\end{itemize}
\hypertarget{simple_fibrations}{}\subsubsection*{{Simple fibrations}}\label{simple_fibrations}

Let $C$ be any category with finite products, and define $E\to C$ to be the [[discrete fibration]] corresponding to the presheaf $C^{op}\to Set$ which is constant at $ob(C)$. Thus, the objects of $E$ are pairs $(\Gamma,A)$ of objects of $C$, with the only morphisms being of the form $(\Gamma,A) \to (\Delta,A)$ induced by a morphism $\Gamma\to\Delta$ in $C$.

Define the functor $E\to C^I$ to take $(\Gamma,A)$ to the projection $\Gamma\times A \to \Gamma$. It is straightforward to check that this defines a category with attributes. The corresponding (split) full comprehension category is called the \emph{simple fibration} of $C$.

The dependent type theory which results from this structure ``has no nontrivial dependency''. That is, whenever we have a dependent type $\Gamma \vdash (A \;type)$, it is already the case that $A$ is a type in the empty context (that is, we have $\vdash (A\; type)$), and so it cannot depend nontrivially on $\Gamma$. In effect, it is not really a dependent type theory, but a \emph{simple} (non-dependent) type theory --- hence the name ``simple fibration''.

\hypertarget{related_pages}{}\subsection*{{Related pages}}\label{related_pages}

\begin{itemize}%
\item [[categorical semantics]]


\item [[relation between type theory and category theory]]


\item [[Awodey's conjecture]]



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

Another overview can be found in the \href{https://ncatlab.org/homotopytypetheory/show/semantics}{HoTT wiki}.

A general overview may be found in

\begin{itemize}%
\item [[Martin Hofmann]], \emph{Syntax and semantics of dependent types}, Semantics and logics of computation (Cambridge, 1995), Publ. Newton Inst., vol. 14, Cambridge Univ. Press, Cambridge, 1997, pp. 79--130

\end{itemize}
Comprehension categories are defined in

\begin{itemize}%
\item [[Bart Jacobs]], \emph{Comprehension categories and the semantics of type dependency}, Theoret. Comput. Sci. 107 (1993), no. 2, 169--207

\end{itemize}
A correspondence with orthogonal factorization systems is discussed in

\begin{itemize}%
\item Clemens Berger, Ralph M. Kaufmann, \emph{Comprehensive factorisation systems} (\href{https://arxiv.org/abs/1710.09438}{pdf})

\end{itemize}
Display maps are discussed in

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

\end{itemize}
Categories with attributes are discussed in

\begin{itemize}%
\item John Cartmell, \emph{Generalised algebraic theories and contextual categories}, Ph.D. thesis, Oxford, 1978 (\href{https://github.com/peterlefanulumsdaine/cartmell-thesis}{GitHub \LaTeX\xspace ing project}, organised by [[Peter LeFanu Lumsdaine]]. Currently only sections 1.0-1.4 are done)


\item [[Eugenio Moggi]], \emph{A category-theoretic account of program modules}, Math. Structures Comput. Sci. 1 (1991), no. 1, 103--139


\item Andrew M. Pitts, \emph{Categorical logic}, Handbook of logic in computer science, Vol. 5, Handb. Log. Comput. Sci., vol. 5, Oxford Univ. Press, New York, 2000, pp. 39--128



\end{itemize}
Categories with families are defined in

\begin{itemize}%
\item [[Peter Dybjer]], \emph{Internal type theory}, Types for proofs and programs (Torino, 1995), Lecture Notes in Comput. Sci., vol. 1158, Springer, Berlin, 1996, pp. 120--134, \href{http://www.cse.chalmers.se/~peterd/papers/InternalTT.pdf}{PDF}

\end{itemize}
and shown to be equivalent to categories with attributes in

\begin{itemize}%
\item [[Martin Hofmann]], \emph{Syntax and semantics of dependent types}, \href{http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.8985}{citeseer}.

\end{itemize}
The formulation in terms of representable natural transformations is in

\begin{itemize}%
\item [[Steve Awodey]]. (2018). \emph{Natural models of homotopy type theory}, Mathematical Structures in Computer Science, 28(2), 241-286. \href{https://arxiv.org/pdf/1406.3219.pdf}{PDF}

\end{itemize}
A proof of initiality for dependent type theory is claimed in

\begin{itemize}%
\item Simon Castellan, \emph{Dependent type theory as the initial category with families}, 2014 (\href{http://iso.mor.phis.me/archives/2011-2012/stage-2012-goteburg/report.pdf}{pdf})

\end{itemize}
This was formalized inside type theory with set quotients of [[higher inductive types]] in:

\begin{itemize}%
\item [[Thorsten Altenkirch]], Ambrus Kaposi, \emph{Type Theory in Type Theory using Quotient Inductive Types}, (2015) (\href{http://www.cs.nott.ac.uk/~txa/publ/tt-in-tt.pdf}{pdf}), (\href{https://bitbucket.org/akaposi/tt-in-tt}{formalisation in Agda}).

\end{itemize}
Contextual categories were defined in

\begin{itemize}%
\item John Cartmell, \emph{Generalised algebraic theories and contextual categories}, Annals of Pure and Applied Logic Volume 32, 1986, Pages 209-243 (\href{http://dx.doi.org/10.1016/0168-0072%2886%2990053-9}{doi:10.1016/0168-0072(86)90053-9})


\item [[Thomas Streicher]], \emph{Semantics of type theory}, Progress in Theoretical Computer Science, Birkh\"a{}user Boston Inc., Boston, MA, 1991, Correctness, completeness and independence results.



\end{itemize}
Review includes

\begin{itemize}%
\item [[Chris Kapulkin]], [[Peter LeFanu Lumsdaine]], section 1.2 and appendix B of \emph{The Simplicial Model of Univalent Foundations (after Voevodsky)} (\href{https://arxiv.org/abs/1211.2851}{arXiv:1211.2851})

\end{itemize}
Contextual categories as models for [[homotopy type theory]] are discussed in

\begin{itemize}%
\item [[Chris Kapulkin]], [[Peter LeFanu Lumsdaine]], \emph{The homotopy theory of type theories} (\href{https://arxiv.org/abs/1610.00037}{arXiv:1610.00037})


\item [[André Joyal]], \emph{Notes on Clans and Tribes} (\href{https://arxiv.org/abs/1710.10238}{arXiv:1710.10238})


\item See also [[clan]].



\end{itemize}
Further discussion of contextual categories is in

\begin{itemize}%
\item [[Vladimir Voevodsky]], \emph{A C-system defined by a universe category}, Theory Appl. Categ. 30 (2015), No. 37, 1181--1215, arXiv:1409.7925 (\href{https://arxiv.org/abs/1409.7925}{arXiv:1409.7925})


\item [[Vladimir Voevodsky]], \emph{Martin-L\"o{}f identity types in the C-systems defined by a universe category} (\href{https://arxiv.org/abs/1505.06446}{arXiv:1505.06446})


\item [[Vladimir Voevodsky]], \emph{Products of families of types in the C-systems defined by a universe category} (\href{https://arxiv.org/abs/1503.07072}{arXiv:1503.07072})


\item [[Vladimir Voevodsky]], \emph{Subsystems and regular quotients of C-systems} (\href{https://arxiv.org/abs/1406.7413}{arXiv:1406.7413})



\end{itemize}
Strictification is discussed in

\begin{itemize}%
\item [[Martin Hofmann]], \emph{On the interpretation of type theory in locally cartesian closed categories}


\item [[Pierre-Louis Curien]], [[Richard Garner]], [[Martin Hofmann]], \emph{Revisiting the categorical interpretation of dependent type theory} ([[CurienGarnerHofmann.pdf:file]])


\item [[Peter LeFanu Lumsdaine]], [[Michael Warren]], \emph{An overlooked coherence construction for dependent type theory}, CT2013


\item [[Vladimir Voevodsky]], \href{http://www.math.ias.edu/~vladimir/Site3/Univalent_Foundations_files/expressions_current.pdf}{Notes on type systems}


\item [[Steve Awodey]]. (2018). \emph{Natural models of homotopy type theory}, Mathematical Structures in Computer Science, 28(2), 241-286. \href{https://arxiv.org/pdf/1406.3219.pdf}{PDF}



\end{itemize}
A comparison of various models, internally in type theory, is in

\begin{itemize}%
\item [[Benedikt Ahrens]], [[Peter LeFanu Lumsdaine]], [[Vladimir Voevodsky]], \emph{Categorical structures for type theory in univalent foundations}, \href{https://arxiv.org/abs/1705.04310}{arxiv}

\end{itemize}
Recent work on abstract definitions of (models of) type theory include:

\begin{itemize}%
\item Valery Isaev, \emph{Algebraic Presentations of Dependent Type Theories} \href{https://arxiv.org/abs/1602.08504}{arXiv}


\item Taichi Uemura, \emph{A General Framework for the Semantics of Type Theory} \href{https://arxiv.org/abs/1904.04097}{arXiv}



\end{itemize}
[[!redirects categorical model of dependent types]] [[!redirects categorical models of dependent types]] [[!redirects category-theoretic model of dependent types]] [[!redirects category-theoretic models of dependent types]] [[!redirects split model of type theory]] [[!redirects split models of type theory]] [[!redirects categorical semantics of dependent types]] [[!redirects category-theoretic semantics of dependent types]]

[[!redirects comprehension category]] [[!redirects comprehension categories]] [[!redirects display map category]] [[!redirects display map categories]] [[!redirects category with attributes]] [[!redirects categories with attributes]] [[!redirects category with families]] [[!redirects categories with families]] [[!redirects contextual category]] [[!redirects contextual categories]] [[!redirects C-system]] [[!redirects C-systems]]



\end{document}