\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*{Initiality Project - References}

\begin{description}

\item[ [[Steve Awodey]], \emph{Natural models of homotopy type theory}] Math. Structures Comput. Sci. 28 (2018), no. 2, 241--286.

\href{https://arxiv.org/abs/1406.3219}{arXiv:1406.3219}, \href{https://doi.org/10.1017/S0960129516000268}{doi:10.1017/S0960129516000268}, \href{https://mathscinet.ams.org/mathscinet-getitem?mr=3742564}{MR}, \href{/nlab/show/Initiality+Project+-+BibTeX+database#awodey_2018_natural-models-of-homotopy-type-theory}{BibTeX}

 
\end{description}
\begin{description}

\item[ [[Krzysztof Kapulkin]] and [[Peter LeFanu Lumsdaine]], \emph{The simplicial model of univalent foundations (after Voevodsky)}] 2012, Revised 2018 as v5

\href{https://arxiv.org/abs/1211.2851}{arXiv:1211.2851}, \href{/nlab/show/Initiality+Project+-+BibTeX+database#kapulkin_2012_the-simplicial-model-of-univalent-foundations}{BibTeX}

Conjecture 1.2.9 in the article says,

\begin{quote}%
Let $\mathbf{T}$ be the type theory given by the structural rules of Section A.1, plus any combination of the logical rules of Sections A.2, A.3. Then $\mathcal{C}(\mathbf{T})$ is initial among contextual categories with the correspondingly-named extra structure.


\end{quote}
The next paragraph of the article says,

\begin{quote}%
In other words, if $\mathcal{C}$ is a contextual category with structure corresponding to the logical rules of a type theory $\mathbf{T}$, then there should be a unique homomorphism $\mathcal{C}(\mathbf{T}) \to \mathcal{C}$ interpreting the syntax of $\mathbf{T}$ in $\mathcal{C}$. As discussed at the beginning of this section, the Correctness Theorem of Str91, Ch. III, p. 181 gives an analogous fact for a rather smaller type theory, while the status of the present conjecture is debated, accepted by some but not all in the field as a straightforward extension of that theorem.


\end{quote}
 
\end{description}
\begin{description}

\item[ [[Thomas Streicher]], \emph{Semantics of type theory}, Correctness, completeness and independence results] With a foreword by Martin Wirsing, Progress in Theoretical Computer Science, Birkhäuser Boston, Inc., Boston, MA, 1991, xii+298 pp., ISBN: 0-8176-3594-7

\href{https://doi.org/10.1007/978-1-4612-0433-6}{doi:10.1007/978-1-4612-0433-6}, \href{https://mathscinet.ams.org/mathscinet-getitem?mr=1134134}{MR}, \href{/nlab/show/Initiality+Project+-+BibTeX+database#streicher_1991_semantics-of-type-theory}{BibTeX}

This book was suggested by Mike Shulman, in an \href{https://nforum.ncatlab.org/discussion/8904/a-communal-proof-of-an-initiality-theorem/?Focus=71137#Comment_71137}{nForum message}, as a primary reference for the [[Initiality Project]].

 
\end{description}
\begin{description}

\item[ [[Vladimir Voevodsky]], \emph{HoTT is not an interpretation of MLTT into abstract homotopy theory}] Article at the {\colorbox[rgb]{1.00,0.93,1.00}{\tt homotopytypetheory\char46org}} blog, January 11, 2015

\href{https://homotopytypetheory.org/2015/01/11/hott-is-not-an-interpretation-of-mltt-into-abstract-homotopy-theory/}{URL}, \href{/nlab/show/Initiality+Project+-+BibTeX+database#voevodsky_2015_hott-is-not_an-interpretation-of-mltt-into-abstract-homotopy-theory}{BibTeX}

There is a discussion of the initiality conjecture in the last four paragraphs of the article.

 
\end{description}
\begin{description}

\item[ [[Vladimir Voevodsky]], \emph{From syntax to semantics of dependent type theories --- formalized}] Slides of a lecture at RDP 2015, Warsaw, June 30, 2015

\href{https://www.math.ias.edu/vladimir/sites/math.ias.edu.vladimir/files/2015_06_30_RDP.pdf}{URL}, \href{/nlab/show/Initiality+Project+-+BibTeX+database#voevodsky_2015_from-syntax-to-semantics-of-dependent-type-theories}{BibTeX}

There is a statement of the initiality conjecture on slide 18. Slide 19 has some remarks on the difficulty of the conjecture, and slide 20 has some remarks on the importance of the conjecture.

 
\end{description}
\begin{description}

\item[ [[Vladimir Voevodsky]], \emph{Mathematical theory of type theories and the initiality conjecture}] Research proposal to the Templeton Foundation, 2016

\href{https://www.math.ias.edu/Voevodsky/voevodsky-publications_abstracts.html#TempletonProposal}{URL}, \href{/nlab/show/Initiality+Project+-+BibTeX+database#voevodsky_2016_mathematical-theory-of-type-theories}{BibTeX}

 
\end{description}
\begin{description}

\item[ [[Vladimir Voevodsky]], \emph{The meta-theory of dependent type theories}] Video, Members Seminar, Institute for Advanced Study, Princeton, NJ, USA, February 27, 2017

\href{https://video.ias.edu/membsem/2017/0227-VladimirVoevodsky}{URL}, \href{/nlab/show/Initiality+Project+-+BibTeX+database#voevodsky_2017_the-meta-theory-of-dependent-type-theories}{BibTeX}

 
\end{description}
\begin{description}

\item[ [[Vladimir Voevodsky]], \emph{Models, interpretations and the initiality conjectures}] Lecture at the special session on category theory and type theory in honor of Per Martin-Löf on his 75th birthday, August 17--19, 2017, during the Logic Colloquium 2017, August 14--20, 2017, Stockholm

\href{https://www.math.ias.edu/Voevodsky/voevodsky-publications_abstracts.html#logcoll-1}{URL}, \href{/nlab/show/Initiality+Project+-+BibTeX+database#voevodsky_2017_models-interpretations-and-the-initiality-conjectures}{BibTeX}

The annotation at the URL of the document says, ``This is a clear and enlightening sketch of Voevodsky's entire program!''.

 
\end{description}
\hypertarget{see_also}{}\subsection*{{See also}}\label{see_also}

\begin{itemize}%
\item [[Initiality Project]]
\item [[Initiality Project - BibTeX database]]

\end{itemize}
category: Initiality Project



\end{document}