cart-models.tex

\documentclass[reqno]{amsart}

\usepackage{amssymb}
\usepackage{hyperref}
\usepackage{mathtools}
\usepackage[all]{xy}
\usepackage{ifthen}
\usepackage{xargs}
\usepackage{bussproofs}
\usepackage{verbatim}
\usepackage{turnstile}

\hypersetup{colorlinks=true,linkcolor=blue}

\renewcommand{\turnstile}[6][s]
    {\ifthenelse{\equal{#1}{d}}
        {\sbox{\first}{$\displaystyle{#4}$}
        \sbox{\second}{$\displaystyle{#5}$}}{}
    \ifthenelse{\equal{#1}{t}}
        {\sbox{\first}{$\textstyle{#4}$}
        \sbox{\second}{$\textstyle{#5}$}}{}
    \ifthenelse{\equal{#1}{s}}
        {\sbox{\first}{$\scriptstyle{#4}$}
        \sbox{\second}{$\scriptstyle{#5}$}}{}
    \ifthenelse{\equal{#1}{ss}}
        {\sbox{\first}{$\scriptscriptstyle{#4}$}
        \sbox{\second}{$\scriptscriptstyle{#5}$}}{}
    \setlength{\dashthickness}{0.111ex}
    \setlength{\ddashthickness}{0.35ex}
    \setlength{\leasturnstilewidth}{2em}
    \setlength{\extrawidth}{0.2em}
    \ifthenelse{%
      \equal{#3}{n}}{\setlength{\tinyverdistance}{0ex}}{}
    \ifthenelse{%
      \equal{#3}{s}}{\setlength{\tinyverdistance}{0.5\dashthickness}}{}
    \ifthenelse{%
      \equal{#3}{d}}{\setlength{\tinyverdistance}{0.5\ddashthickness}
        \addtolength{\tinyverdistance}{\dashthickness}}{}
    \ifthenelse{%
      \equal{#3}{t}}{\setlength{\tinyverdistance}{1.5\dashthickness}
        \addtolength{\tinyverdistance}{\ddashthickness}}{}
        \setlength{\verdistance}{0.4ex}
        \settoheight{\lengthvar}{\usebox{\first}}
        \setlength{\raisedown}{-\lengthvar}
        \addtolength{\raisedown}{-\tinyverdistance}
        \addtolength{\raisedown}{-\verdistance}
        \settodepth{\raiseup}{\usebox{\second}}
        \addtolength{\raiseup}{\tinyverdistance}
        \addtolength{\raiseup}{\verdistance}
        \setlength{\lift}{0.8ex}
        \settowidth{\firstwidth}{\usebox{\first}}
        \settowidth{\secondwidth}{\usebox{\second}}
        \ifthenelse{\lengthtest{\firstwidth = 0ex}
            \and
            \lengthtest{\secondwidth = 0ex}}
                {\setlength{\turnstilewidth}{\leasturnstilewidth}}
                {\setlength{\turnstilewidth}{2\extrawidth}
        \ifthenelse{\lengthtest{\firstwidth < \secondwidth}}
            {\addtolength{\turnstilewidth}{\secondwidth}}
            {\addtolength{\turnstilewidth}{\firstwidth}}}
        \ifthenelse{\lengthtest{\turnstilewidth < \leasturnstilewidth}}{\setlength{\turnstilewidth}{\leasturnstilewidth}}{}
    \setlength{\turnstileheight}{1.5ex}
    \sbox{\turnstilebox}
    {\raisebox{\lift}{\ensuremath{
        \makever{#2}{\dashthickness}{\turnstileheight}{\ddashthickness}
        \makehor{#3}{\dashthickness}{\turnstilewidth}{\ddashthickness}
        \hspace{-\turnstilewidth}
        \raisebox{\raisedown}
        {\makebox[\turnstilewidth]{\usebox{\first}}}
            \hspace{-\turnstilewidth}
            \raisebox{\raiseup}
            {\makebox[\turnstilewidth]{\usebox{\second}}}
        \makever{#6}{\dashthickness}{\turnstileheight}{\ddashthickness}}}}
        \mathrel{\usebox{\turnstilebox}}}

\newcommand{\newref}[4][]{
\ifthenelse{\equal{#1}{}}{\newtheorem{h#2}[hthm]{#4}}{\newtheorem{h#2}{#4}[#1]}
\expandafter\newcommand\csname r#2\endcsname[1]{#3~\ref{#2:##1}}
\expandafter\newcommand\csname R#2\endcsname[1]{#4~\ref{#2:##1}}
\expandafter\newcommand\csname n#2\endcsname[1]{\ref{#2:##1}}
\newenvironmentx{#2}[2][1=,2=]{
\ifthenelse{\equal{##2}{}}{\begin{h#2}}{\begin{h#2}[##2]}
\ifthenelse{\equal{##1}{}}{}{\label{#2:##1}}
}{\end{h#2}}
}

\newref[section]{thm}{Theorem}{Theorem}
\newref{lem}{Lemma}{Lemma}
\newref{prop}{Proposition}{Proposition}
\newref{cor}{Corollary}{Corollary}
\newref{cond}{Condition}{Condition}
\newref{conj}{Conjecture}{Conjecture}

\theoremstyle{definition}
\newref{defn}{Definition}{Definition}
\newref{example}{Example}{Example}

\theoremstyle{remark}
\newref{rem}{Remark}{Remark}

\newcommand{\red}{\Rightarrow}
\newcommand{\deq}{\equiv}
\newcommand{\repl}{:=}
\newcommand{\idtype}{\rightsquigarrow}
\newcommand{\Id}{\mathrm{Id}}

\newcommand{\cat}[1]{\mathbf{#1}}
\newcommand{\C}{\cat{C}}
\newcommand{\D}{\cat{D}}
\newcommand{\Cat}{\cat{Cat}}
\newcommand{\Mod}[1]{#1\text{-}\cat{Mod}}
\newcommand{\Th}{\cat{Th}}
\newcommand{\emptyCtx}{\mathbf{1}}
\newcommand{\Set}{\cat{Set}}
\newcommand{\sSet}{\cat{sSet}}
\newcommand{\qcat}{\cat{qcat}}
\newcommand{\K}{$\mathcal{K}$}
\newcommand{\join}{\star}
\newcommand{\Hom}{\mathrm{Hom}}

\newcommand{\cmap}[1]{\mathrm{c}_{#1}}
\newcommand{\nf}{\mathrm{nf}}
\newcommand{\M}{H}

\newcommand{\we}{\mathcal{W}}
\newcommand{\I}{\mathrm{I}}
\newcommand{\J}{\mathrm{J}}
\newcommand{\class}[2]{#1\text{-}\mathrm{#2}}
\newcommand{\Icell}[1][\I]{\class{#1}{cell}}
\newcommand{\Icof}[1][\I]{\class{#1}{cof}}
\newcommand{\Iinj}[1][\I]{\class{#1}{inj}}
\newcommand{\Jinj}[1][]{\Iinj[\J#1]}
\newcommand{\Jcell}[1][]{\Icell[\J#1]}
\newcommand{\Jcof}[1][]{\Icof[\J#1]}

\numberwithin{figure}{section}

\newcommand{\pb}[1][dr]{\save*!/#1-1.2pc/#1:(-1,1)@^{|-}\restore}
\newcommand{\po}[1][dr]{\save*!/#1+1.2pc/#1:(1,-1)@^{|-}\restore}

\begin{document}

\title[Equivalence between quasicategories and models of type theory]{Equivalence between finitely complete quasicategories and models of simplicial homotopy type theory}

\author{Valery Isaev}

\begin{abstract}
Abstract.
\end{abstract}

\maketitle

\section{Introduction}

\section{Functors between $\sSet$ and $\Mod{T}$}
\label{sec:nerve}

In this section we define a Quillen adjunction between $\sSet$ and $\Mod{T}$ for every appropriate algebraic dependent type theory $T$.
Recall that $sq_l$ is the theory with the following axioms:
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash i : I$}
\AxiomC{$\Gamma \vdash j : I$}
\BinaryInfC{$\Gamma \vdash sq_l(i,j) : I$}
\DisplayProof
\end{center}
\begin{align*}
sq_l(left,j) & = left \\
sq_l(right,j) & = j \\
sq_l(i,left) & = left \\
sq_l(i,right) & = i
\end{align*}
To define functors between $\sSet$ and $\Mod{T}$, we also need to assume that $sq_l$ is associative.
Let $sq^a_l$ be the theory which has the same axioms as $sq_l$ together with the following axiom:
\[ sq_l(sq_l(i,j),k) = sq_l(i,sq_l(j,k)) \]

Let $T$ be any theory under $sq^a_l$.
For every finite nonempty linearly ordered set $J$, we define a model $\mathfrak{C}(\Delta^J)$ of $T$.
It is generated by the generators and relations described below.
Generators of $\mathfrak{C}(\Delta^J)$ are $O_j : (ty,0)$ for every $j \in J$, and $\M_{J'} : (tm,|J'|-1)$ for every subset $J'$ of $J$ such that $|J'| \geq 2$.
For every $j \in J$, $\mathfrak{C}(\Delta^J)$ has relation $\vdash O_j\ type$.
For every $J' = \{ j_1 < \ldots < j_n \} \subseteq J$ such that $n \geq 2$, it has the following relation:
\[ x : O_{j_1}, x_{j_2} : I, \ldots x_{j_{n-1}} : I \vdash \M_{J'} : O_{j_n} \]
For every $j \notin J'$ such that $j_1 < j < j_n$, it has the following relations:
\begin{align}
x : O_{j_1}, x_{j_2} : I, \ldots x_{j_{n-1}} : I & \vdash \M_{J' \cup \{j\}}[x_j \repl left] \deq \M_{\{ j, \ldots j_n \}}[x \repl \M_{\{ j_1, \ldots j \}}] \label{rel:left} \\
x : O_{j_1}, x_{j_2} : I, \ldots x_{j_{n-1}} : I & \vdash \M_{J' \cup \{j\}}[x_j \repl right] \deq \M_{J'} \label{rel:right}
\end{align}

The idea of this definition is similar to \cite[Definition~1.1.5.1]{lurie-topos}.
For every vertex $j$ of $\Delta^J$, we have a type $O_j$,
and for every $(n+1)$-dimensional face $J'$ of $\Delta^J$, we have an $n$-dimensional cube $\M_{J'}$.
Relations describe faces of these cubes.

Let $sq_l(x_1, \ldots x_n) = sq_l(x_1, \ldots sq_l(x_{n-1},x_n) \ldots )$.
In particular, $sq_l(x) = x$ and $sq_l() = right$.
Now, we can extend $\mathfrak{C}$ to a functor $\Delta \to \Mod{T}$.
Let $f : J \to K$ be a monotone map between linearly ordered sets.
Then we define $\mathfrak{C}(f)$ as follows:
\begin{align*}
\mathfrak{C}(f)(O_j) & = O_{f(j)} \\
\mathfrak{C}(f)(\M_{J'}) & =
\begin{cases}
    x                                                                  & \text{if } |f(J')| = 1 \\
    \M_{f(J')}[\ \ldots\ x_{k_i} \repl sq_l(x_{f^{-1}(k_i)})\ \ldots\ ] & \text{if } |f(J')| > 1 \\
\end{cases}
\end{align*}
where $k_i$ runs from $k_2$ to $k_{m-1}$, $\{ k_1 < \ldots < k_m \} = f(J')$,
and $x_{f^{-1}(k_i)} = x_{j_1}, \ldots x_{j_n}$, $\{ j_1 < \ldots < j_n \} = f^{-1}(k_i)$.

Let us check that $\mathfrak{C}(f)$ preserves relations.
Let $J' = \{ j_1 < \ldots < j_i < j < j_{i+1} < \ldots < j_n \}$ be a subset of $J$, and let $f'$ be the restriction of $f$ to $J'$.
If $|f(J')| = 1$, then $\mathfrak{C}(f)(\M_{J' \cup \{j\}}[x_j \repl left]) = \mathfrak{C}(f)(\M_{\{ j, \ldots j_n \}}[x \repl \M_{\{ j_1, \ldots j \}}]) = \mathfrak{C}(f)(\M_{J' \cup \{j\}}[x_j \repl right]) = \mathfrak{C}(f)(\M_{J'}) = x$.
Thus we may assume that $|f(J')| > 1$. 

Let $\rho(x_{f(j_i)}) = sq_l(x_{f'^{-1}(f(j_1))})$ for every $1 \leq i \leq n$ such that $f(j_i) \neq f(j)$.
Let us consider the first relation.
If $f(j) = f(j_1)$, then
\begin{align*}
\mathfrak{C}(f)(\M_{J' \cup \{j\}}[x_j \repl left]) & = \\
\M_{f(J')}[\rho] & = \\
\M_{\{ f(j), \ldots f(j_n) \}}[\rho][x \repl x] & = \\
\mathfrak{C}(f)(\M_{\{ j, \ldots j_n \}}[x \repl \M_{\{ j_1, \ldots j \}}]) & .
\end{align*}
If $f(j) = f(j_n)$, then
\begin{align*}
\mathfrak{C}(f)(\M_{J' \cup \{j\}}[x_j \repl left]) & = \\
\M_{f(J')}[\rho] & = \\
x[x \repl \M_{\{f(j_1), \ldots f(j)\}}[\rho]] & = \\
\mathfrak{C}(f)(\M_{\{ j, \ldots j_n \}}[x \repl \M_{\{ j_1, \ldots j \}}]) & .
\end{align*}
If $f(j_1) < f(j) < f(j_n)$, then
\begin{align*}
\mathfrak{C}(f)(\M_{J' \cup \{j\}}[x_j \repl left]) & = \\
\M_{f(J') \cup \{f(j)\}}[\rho, x_{f(j)} \repl sq_l(x_{f'^{-1}(f(j))}, x_j)][x_j \repl left] & = \\
\M_{f(J') \cup \{f(j)\}}[\rho, x_{f(j)} \repl left] & = \\
\M_{\{f(j), \ldots f(j_n)\}}[x \repl \M_{\{f(j_1), \ldots f(j)\}}][\rho] & = \\
\mathfrak{C}(f)(\M_{\{ j, \ldots j_n \}}[x \repl \M_{\{ j_1, \ldots j \}}]) & .
\end{align*}

Let us consider the second relation.
If either $f(j) = f(j_1)$ or $f(j) = f(j_n)$, then $\mathfrak{C}(f)(\M_{J' \cup \{j\}}[x_j \repl right]) = \M_{f(J')}[\rho] = \mathfrak{C}(f)(\M_{J'})$.
If $f(j_1) < f(j) < f(j_n)$, then
\begin{align*}
\mathfrak{C}(f)(\M_{J' \cup \{j\}}[x_j \repl right]) & = \\
\M_{f(J') \cup \{f(j)\}}[\rho, x_{f(j)} \repl sq_l(x_{f'^{-1}(f(j))}, x_j)][x_j \repl right] & = \\
\M_{f(J') \cup \{f(j)\}}[\rho, x_{f(j)} \repl sq_l(x_{f'^{-1}(f(j))})] & = \\
\mathfrak{C}(f)(\M_{J'}) & ,
\end{align*}
If $f(j_i) < f(j) < f(j_{i+1})$, then the last equality holds by \eqref{rel:right},
otherwise it holds immediately by definition of $\mathfrak{C}(f)(\M_{J'})$.

Let $[n]$ be the set of natural numbers $\{ 0, \ldots n \}$ with the obvious linear order.
Then $\Delta$ is the full subcategory of linearly ordered sets on objects of the form $[n]$.
It is easy to see that $\mathfrak{C}$ preserves identity morphisms,
and the fact that it preserves compositions follows from associativity of $sq_l$.
Thus we have a functor $\mathfrak{C} : \Delta \to \Mod{T}$.
This functor (uniquely) extends to a colimit-preserving functor $\mathfrak{C} : \sSet \to \Mod{T}$,
which has a right adjoint $N : \Mod{T} \to \sSet$ defined by equation $N(X) = \Hom(\mathfrak{C}(-),X)$.

We can explicitly describe $\mathfrak{C} : \sSet \to \Mod{T}$.
Model $\mathfrak{C}(X)$ is generated by symbols $O_a : (ty,0)$ for every $a \in X_0$, and $\M_a : (tm,n)$ for every $a \in X_n$, $n \geq 1$.
For every $a \in X_0$, $\mathfrak{C}(X)$ has relations $\vdash O_a\ type$ and $\M_{s_0(a)} = (x : O_a \vdash x : O_a)$.
For every $a \in X_n$, $n \geq 1$, it has the following relation:
\[ x : O_{a|\Delta^{\{0\}}}, x_1 : I, \ldots x_{n-1} : I \vdash \M_a : O_{a|\Delta^{\{n\}}} \]
For every $1 \leq j \leq n-1$, it has the following relations:
\begin{align*}
\M_a[x_j \repl left] & = \M_{a|\Delta^{\{ j, \ldots n \}}}[x \repl \M_{a|\Delta^{\{ 0, \ldots j \}}}] \\
\M_a[x_j \repl right] & = \M_{a|\Delta^{\{0, \ldots j-1, j+1, \ldots n\}}}
\end{align*}
For every $0 \leq j \leq n$, it has the following relation:
\[ \M_{s_j(a)} =
\begin{cases}
    \M_a[x_1 \repl x_2, \ldots x_{n-1} \repl x_n]                                      & \text{if } j = 0 \\
    \M_a[x_j \repl sq_l(x_j,x_{j+1}), x_{j+1} \repl x_{j+2}, \ldots x_{n-1} \repl x_n] & \text{if } 1 \leq j \leq n-1 \\
    \M_a                                                                               & \text{if } j = n \\
\end{cases}
\]
For every morphism $f : X \to Y$ of simplicial sets, let $\mathfrak{C}(f)(O_a) = O_{f(a)}$ and $\mathfrak{C}(f)(\M_a) = \M_{f(a)}$.
It is easy to see that this definition preserves relations, identity morphisms and compositions.

\begin{prop}
Functors $\mathfrak{C} \dashv N$ determine a Quillen adjunction between $\sSet$ with the Joyal model structure and $\Mod{T}$ with the model structure defined in \cite{alg-models}.
\end{prop}
\begin{proof}
Note that $\mathfrak{C}(\partial \Delta^n)$ is isomorphic (over $\mathfrak{C}(\Delta^n)$) to the theory
generated by the same generators and relations as $\mathfrak{C}(\Delta^n)$ except for $\M_{[n]}$.
Similarly, if $i \in [n]$, then $\mathfrak{C}(\Lambda^n_i)$ is generated by the same generators
and relations as $\mathfrak{C}(\partial \Delta^n)$ except for $\M_{\{ 0, \ldots i-1, i+1, \ldots n \}}$.

Let us prove that $\mathfrak{C}$ preserves cofibration.
To do this, it is enough to show that $\mathfrak{C}(\partial \Delta^n) \to \mathfrak{C}(\Delta^n)$ is a cofibration for every $n$.
If $n = 0$, then this map equals to $i_{(ty,0)}$.
Suppose that $n > 0$.
First, let us define objects $\square^k$ and $\partial \square^k$.
Let $\square^k = F(\{ x : A, x_1 : I, \ldots x_k : I \vdash b : B \})$,
and let $\partial \square^k$ be generated by the generators and relations described below.
Generators of $\partial \square^k$ are $A,B : (ty,0)$ and $b_{[i=c]} : (tm,k)$ for every $1 \leq i \leq k$, $c \in \{left,right\}$.
For every $1 \leq i \leq k$ and $c \in \{left,right\}$, it has the following relation:
\[ x : A, x_1 : I, \ldots x_{i-1} : I, x_{i+1} : I, \ldots x_k : I \vdash b_{[i=c]} : B \]
For every $1 \leq i_1 < i_2 \leq k$ and $c,c' \in \{left,right\}$, it has the following relation:
\[ b_{[i_2=c']}[x_{i_1} \repl c] = b_{[i_1=c]}[x_{i_2} \repl c'] \]

Map $i^k : \partial \square^k \to \square^k$ is defined in the obvious way: $i^k(b_{[i=c]}) = b[x_i \repl c]$.
Let $v : \square^{n-1} \to \mathfrak{C}(\Delta^n)$ be defined as follows: $v(A) = O_0$, $v(B) = O_n$, $v(b) = \M_{[n]}$.
Map $v \circ i^k$ factors through $\mathfrak{C}(\partial \Delta^n) \to \mathfrak{C}(\Delta^n)$, and the following square is cocartesian:
\[ \xymatrix{ \partial \square^{n-1} \ar[r] \ar[d]_{i^k} & \mathfrak{C}(\partial \Delta^n) \ar[d] \\
              \square^{n-1} \ar[r]_v & \mathfrak{C}(\Delta^n)
            } \]
Thus we just need to show that $i^k$ is a cofibration.
But it is a pushout of $i_{(tm,1)} : F(\{ x : A \vdash B\ type \}) \to F(\{ x : A \vdash b : B \})$.
Indeed, let $v' : F(\{ x : A \vdash b : B \}) \to \square^k$ be defined as follows: $v'(b) = path(x_1.\,\ldots path(x_n.\,b) \ldots)$ and $v'(B)$ equals to
\begin{align*}
Path(x_1.\, \ldots Path(x_{n-2}.\, & Path(x_{n-1}.\,     Path(x_n.\,B, b[x_n \repl left], b[x_n \repl right]), \\
                                   & \qquad \qquad \quad path(x_n.\,b[x_{n-1} \repl left]), \\
                                   & \qquad \qquad \quad path(x_n.\,b[x_{n-1} \repl right])), \\
                                   & path(x_{n-1}.\,     path(x_n.\,b[x_{n-2} \repl left])), \\
                                   & path(x_{n-1}.\,     path(x_n.\,b[x_{n-2} \repl right]))) \ldots )
\end{align*}
Then $v' \circ i_{(tm,1)}$ factors through $i^k$, and the following square is cocartesian:
\[ \xymatrix{ F(\{ x : A \vdash B\ type \}) \ar[r] \ar[d]_{i_{(tm,1)}} & \partial \square^k \ar[d]^{i^k} \\
              F(\{ x : A \vdash b : B \}) \ar[r]_-{v'} & \square^k
            } \]

Now, let us prove that for every $X \in \Mod{T}$, $N(X)$ is fibrant.
Since fibrant objects in $\sSet$ are precisely quasicategories,
it is enough to show that $\mathfrak{C}(\Lambda^n_i) \to \mathfrak{C}(\Delta^n)$ is a trivial cofibration for every inner horn $\Lambda^n_i \to \Delta^n$.
First, for every $1 \leq i \leq k$, let $\sqcap^k_i$ be the object defined by the same generators and relations as $\partial \square^k$ except for $b_{[i=right]}$.
Then we have the following cocartesian square:
\[ \xymatrix{ \sqcap^{n-1}_i \ar[r] \ar[d] & \mathfrak{C}(\Lambda^n_i) \ar[d] \\
              \partial \square^{n-1} \ar[r] & \mathfrak{C}(\partial \Delta^n)
            } \]

Since $\sqcap^k_i \to \square^k$ is a cofibration, we just need to show that it is a weak equivalence.
Note that $\sqcap^k_i \to \square^k$ is isomorphic to $\sqcap^k_k \to \square^k$ for every $1 \leq i \leq k$.
Indeed, we can define isomorphism $g : \square^k \to \square^k$ as $g(b) = b[x_i \repl x_k, x_k \repl x_i]$
and isomorphism $f : \sqcap^k_i \to \sqcap^k_k$ as $f(b_{[i=left]}) = b_{[k=left]}[x_i \repl x_k]$, $f(b_{[k=c]}) = b_{[i=c]}[x_k \repl x_i]$,
and $f(b_{[j=c]}) = b_{[j=c]}[x_i \repl x_k, x_k \repl x_i]$ for every $j \neq i,k$.
Then $f$ and $g$ commute with $\sqcap^k_i \to \square^k$ and $\sqcap^k_k \to \square^k$.
Thus we just need to prove that $\sqcap^k_k \to \square^k$ is a weak equivalence.

Note that $\square^{k+1}$ is a (relative) cylinder object for $F(\{ A : (ty,0), B : (ty,0) \}) \to \square^k$.
Indeed, $\square^k \amalg_{F(\{ A : (ty,0), B : (ty,0) \})} \square^k \to \square^{k+1}$ is a cofibration,
and $\square^k \to \square^{k+1}$ is a weak equivalence since it is a pushout of
a generating trivial cofibration $F(\{ \Gamma \vdash b : B \}) \to F(\{ \Gamma, y : I \vdash h : B \})$.

Every object has RLP with respect to $\sqcap^k_k \to \square^k$ (see \cite[Section~2.4]{alg-models}).
In particular, $\sqcap^k_k \to \square^k$ has a retract $\square^k \to \sqcap^k_k$.
The composite map $\square^k \to \sqcap^k_k \to \square^k$ is homotopic to $id$.
To show this, we just need to construct an appropriate map $\square^{k+1} \to \square^k$,
which is easy to do using filler operations from \cite[Section~2.4]{alg-models}.
Thus $\sqcap^k_k \to \square^k$ is a homotopy equivalence.

Finally, let us prove that if $f : X \to Y$ is a fibration in $\Mod{T}$, then $N(f)$ is a fibration in $\sSet$.
Since $N(Y)$ is fibrant, by \cite[Corollary~2.4.6.5]{lurie-topos}, we just need to prove the following conditions:
\begin{enumerate}
\item $N(f)$ is an inner fibration.
\item For every object $A$ of $N(X)$ and every equivalence $p : N(f)(A) \to B$ in $N(Y)$, there exists an equivalence $p' : A \to B'$ in $N(X)$ such that $N(f)(p') = p$.
\end{enumerate}
The first condition follows from the fact that maps $\mathfrak{C}(\Lambda^n_i) \to \mathfrak{C}(\Delta^n)$ are trivial cofibrations.
The second condition can be reformulated as follows: for every closed type $A$ of $X$ and every equivalence $p : f(A) \to B$ in $Y$,
there exists an equivalence $p' : A \to B'$ in $X$ such that $f(p') = p$.
But this follows from the fact that $f$ has RLP with respect to $\J_{\I_{ty}}$.
\end{proof}

\section{Slice quasicategories}

Let $T$ be a stable theory with $\Sigma$-types with eta rules.
Then for every model $M$ of $T$ and every $A \in M_{(ty,0)}$, we can define another model $M/A$ of $T$.
Let $(M/A)_{(p,n)} = \{ x \in M_{(p,n+1)}\ |\ ft^n(x) = A \}$.
Since $T$ is stable, the structure of a model of $T$ on $M$ induces this structure on $M/A$.
In this section we construct a categorical equivalence $p : N(M/A) \to N(M)/A$ between the nerve of $M/A$ and the slice quasicategory of $N(M)$ over $A$.
We also prove that $N(M)$ has finite limits.
We begin with terminal objects.
A type $C \in M_{(ty,n)}$ is a \emph{proposition} if there is a term $\Gamma, x : C, y : C \vdash p : x \idtype y$.
It is \emph{contractible} if it is a proposition and there is a term $\Gamma \vdash c : C$.

\begin{prop}[contr-terminal]
Let $M$ be a model of a dependent type theory.
Then $C \in M_{(ty,0)}$ is a contractible type of $M$ if and only if $C$ is a terminal object of $N(M)$.
Moreover, if $C$ is contractible, then, for every type $A$, the weakening of $C$ is a terminal object of $N(M/A)$.
\end{prop}
\begin{proof}
An object $C$ of $N(M)$ is terminal if and only if every map $f : \partial \Delta^n \to N(M)$ such that $f|_{\Delta^{\{n\}}} = C$ extends to a map $\Delta^n \to N(M)$.
This is true if and only if every map $f : \partial \square^n \to M$ such that $f(B) = C$ extends to a map $\square^n \to M$.
Thus, if $C$ is a terminal object of $N(M)$, then we have a term $x : I \vdash b : C$ and hence a term $\vdash c : C$.
Moreover, we have a term $x : C \vdash p : x \idtype c$, which implies that $C$ is contractible.

Conversely, assume that $C \in M_{(ty,n)}$ is a proposition.
Then a standard argument implies that the type $\Gamma, x : C, y : C \vdash x \idtype y$ is also a proposition.
Since $Path(x.\,A,a_1,a_2)$ is equivalent to a type of the form $a_1' \idtype a_2$,
this implies types of the form $Path(x_n.\, \ldots Path(x_1.\,C,c_1,c_1'), \ldots, c_n, c_n')$ are inhabited.
An element of such a type determines an extension of a map $\partial \square^n \to M$ determined by terms $c_1,c_1', \ldots c_n,c_n'$.
Thus, every such map has an extension to a map $\square^n \to M$.

Finally, if $C$ is contractible, then its weakening is contractible type.
Hence, it is a terminal object of $N(M/A)$.
\end{proof}

Let $C$ be a quasicategory, and let $A \in C_{[0]}$ be an object of $C$.
Then $C/A$ is the quasicategory defined as follows: $(C/A)_{[n]} = \{ x \in C_{[n+1]}\ |\ x|_{\Delta^{\{n+1\}}} = A \}$.
For every monotone map $f : [k] \to [n]$, let $(C/A)_f(x) = C_{f'}(x)$, where $f' : [k+1] \to [n+1]$ is the map such that $f'(k) = n$ and $f'(i) = f(i)$ for every $0 \leq i \leq k$.
For a proof that this simplicial set is a quasicategory, see for instance \cite[Proposition~1.2.9.3]{lurie-topos}.

Elements of $N(M)_{[n]}$ can be represented by pairs $(O,H)$, where $O$ is a function that maps elements of $[n]$ to $N(M)_{(ty,0)}$
and $H$ is a function that maps a subset $J = \{ j_1 < \ldots < j_k \}$ of $[n]$ such that $k \geq 2$ to a term of the form $x : O_{j_1}, x_{j_2} : I, \ldots x_{j_{k-1}} : I \vdash H_J : O_{j_k}$.
These functions must satisfy relations described in the previous section.
Let $(O,H)$ be an element of $N(M/A)_{[n]}$.
Then $O_i \in M_{(ty,1)}$ is such that $z : A \vdash O_i\ type$ and $H_J$ can be identified with an element of $M_{(tm,k)}$ such that $z : A, x : O_{j_1}, x_{j_2} : I, \ldots x_{j_{k-1}} : I \vdash H_J : O_{j_k}$.
To define an element $p(O,H) \in (N(M)/A)_{[n]}$, we need to specify functions $O'$ and $H'$ as described above.
Let $O'_{n+1}$ be equal to $A$, and let $O'_i$ be equal to $\Sigma(z : A)\,O_i$.
If $J = \{ j_1 < \ldots < j_k \}$ and $j_k \leq n$, then we define $H'_J$ as follows:
\[ x : \Sigma (z : A)\,O_{j_1}, x_{j_2} : I, \ldots x_{j_{k-1}} : I \vdash (\pi_1(x), H_J[z \repl \pi_1(x), x \repl \pi_2(x)]) : \Sigma (z : A)\,O_{j_k} \]
If $J = \{ j_1 < \ldots < j_k \}$ and $j_k = n+1$, then we define $H'_J$ as follows:
\[ x : \Sigma (z : A)\,O_{j_1}, x_{j_2} : I, \ldots x_{j_{k-1}} : I \vdash \pi_1(x) : A \]
It is easy to see that $p$ respects face maps and, since the theory has eta rules for $\Sigma$-types, $p$ respects degeneracy maps too.
Thus, we defined a map $p : N(M/A) \to N(M)/A$.

\begin{prop}[slice-stability]
Let $M$ be a model of a stable theory.
Then, for every $A \in M_{(ty,0)}$, the map $p : N(M/A) \to N(M)/A$ is a categorical equivalence.
\end{prop}
\begin{proof}
Since $N(M/A)$ and $N(M)/A$ are quasicategories, \cite[Proposition~3.5]{f-model-structures} implies that to prove that $p$ is a categorical equivalence,
we just need to show that for every $n \in \mathbb{N}$ and every commutative square of the form
\[ \xymatrix{ \partial \Delta^n \ar[r]^-f \ar[d] & N(M/A) \ar[d]^p \\
              \Delta^n \ar[r]_-g                 & N(M)/A,
            } \]
there is a map $g' : \Delta^n \to N(M/A)$ such that the top triangle commutes and the bottom triangle commutes up to relative homotopy.
Maps $g,g' : \Delta^0 \to X$ are (relatively) homotopic if the objects of $X$ represented by these maps are equivalent.
If $n > 0$, then maps $g,g' : \Delta^n \to X$ are relatively homotopic if there is a map $h : \Delta^{n+1} \to X$
such that $\delta_0(h) = g$, $\delta_0(h) = f$, and $\delta_i(h) = \sigma_0(\delta_{i-1}(f))$ for every $2 \leq i \leq n+1$.

Let us prove that for every object $s$ of $N(M)/A$, there is an object $s'$ of $N(M/A)$ such that $p(s')$ is equivalent to $s$.
An object of $N(M)/A$ is a 1-simplex $s$ of $N(M)$ such that $s|_{\Delta^{\{1\}}} = A$.
Thus, it is just a term of the form $y : C \vdash a : A$.
Let $B$ be the object of $N(M/A)$ defined as $x : A \vdash \Sigma (y : C)\,(a \idtype x)$.
It is an easy exercise to prove that $\Sigma (x : A)\,\Sigma (y : C)\,(a \idtype x)$ and $C$ are homotopy equivalent over $A$.
It follows that $p(B)$ is equivalent to $a$.

Let $f : \partial \Delta^n \to N(M/A)$ and $g = (O,H) : \Delta^n \to N(M)/A$ be maps such that $n > 0$ and the square above commutes.
Then $x : \Sigma (z : A)\,O_0, x_1 : I, \ldots x_n : I \vdash H_{[n+1]} : A$ and
$x : \Sigma (z : A)\,O_0, x_1 : I, \ldots x_{n-1} : I \vdash H_{[n]} : \Sigma (z : A)\,O_n$.
To extend $f$ to a map $\Delta^n \to N(M/A)$, we need to define a term $z : A, x : O_0, x_1 : I, \ldots x_{n-1} : I \vdash h' : O_n$
in such a way that relations \eqref{rel:left} and \eqref{rel:right} hold.
Let $h' = coe_0(x_n.\,O_n[z \repl H_{[n+1]}], \pi_2(H_{[n]}))[x \repl (z,x)]$.
Note that $H_{[n+1]}[x_j \repl c] = \pi_1(x)$ for every $1 \leq j \leq n$ and every $c \in \{ left, right \}$.
By $\sigma$-rule, $h'[x_j \repl c] = \pi_2((H_{[n]}[x \repl (z,x), x_j \repl c]))$.
Thus, the relations for $h'$ hold since they hold for $H_{[n]}$.

Let $g' : \Delta^n \to N(M/A)$ be the map corresponding to $h'$.
We need to prove that $p \circ g'$ is relatively homotopic to $g$.
That is, we need to find a map $T : \Delta^{n+2} \to N(M)$ such that $\delta_0(T) = g$, $\delta_1(T) = p \circ g'$,
and $\delta_i(T) = \sigma_0(\delta_{i-1}(g))$ for every $2 \leq i \leq n+1$.
Since all of the faces except the last one are fixed, we just need to specify a term $x : \Sigma (z : A)\,O_0, x_1 : I, \ldots x_n : I \vdash T_{[n+1]} : \Sigma (z : A)\,O_{n+1}$
corresponding to the last face and a term $x : \Sigma (z : A)\,O_0, x_1 : I, \ldots x_{n+1} : I \vdash T_{[n+2]} : A$ corresponding to the interior of the simplex $T$.

We define $T_{[n+1]}$ as $(H_{[n+1]}, coe_1(x_n.O_n[z \repl \pi_1(H_{[n]})], \pi_2(H_{[n]}), x_n))\rho$, where $\rho = [x_1 \repl x_2, \ldots x_{n-1} \repl x_n, x_n \repl x_1]$.
Let $T_{[n+2]} = H_{[n+1]}[x_1 \repl x_2, \ldots x_{n-1} \repl x_n, x_n \repl sq_r(x_1, x_{n+1})]$,
where $sq_r$ is a function such that $sq_r(i,right) = right$, $sq_r(right,j) = right$, $sq_r(i,left) = i$, and $sq_r(left,j) = j$.
It is easy to see that relations \eqref{rel:left} and \eqref{rel:right} hold.
Thus, $T$ determines a homotopy between $g$ and $p \circ g'$.
\end{proof}

The previous proposition shows that stable theories are stable under slicing.
That is if we can prove that, for every model $M$ of a stable theory, the quasicategory $N(M)$ has some property,
then this property holds for every slice quasicategory $N(M)/A$.
For example, if we can prove that $N(M)$ has all finite products, then it also has all finite limits.

Let $C$ be a quasicategory, and let $A$ and $B$ be objects of $C$.
Then we define $C/A,B$ as the slice category $C/p$, where $p : \partial \Delta^1 \to C$ is the map determined by $A$ and $B$.
The set $(C/A,B)_{[n]}$ consists of pairs of simplices $x,y \in C_{[n+1]}$ such that
$x|_{\Delta^{\{n+1\}}} = A$, $y|_{\Delta^{\{n+1\}}} = B$, and $x|_{\Delta^{\{0, \ldots n\}}} = y|_{\Delta^{\{0, \ldots n\}}}$.
Then a product of $A$ and $B$ is a terminal object of $C/A,B$.

\begin{prop}
For every model $M$ of a stable theory with $\Sigma$-types with eta rules, the quasicategory $N(M)$ is finitely complete.
\end{prop}
\begin{proof}
By \rprop{slice-stability}, we just need to prove that $N(M)$ has all finite products.
By \rprop{contr-terminal}, $N(M)$ has a terminal object since the interval is contractible.
To prove that $N(M)$ has binary products, note that $N(M)/A,B$ is isomorphic to $N(M)/(A \times B)$ and the latter has a terminal object.
\end{proof}

The results of \cite{szumilo} and \cite{kapulkin-szumilo} imply that the simplicial localization of $M$ as a category with weak equivalences is finitely complete.
If $M$ is a model of a theory with $\Pi$-types, then it was shown in \cite{kapulkin} that it is also locally Cartesian closed.
We believe that $N(M)$ is equivalent to the simplicial localization of $M$, but we do not have a proof, so these results cannot be applied in our case.

\section{Marked models}

Let $\C$ be a category, let $\mathcal{K}$ be a small category, and let $\mathcal{F} : \mathcal{K} \to \C$ be a functor.
A \emph{\K-marked object} of $\C$ is a pair $(X,\mathcal{E})$, where $X$ is an object of $\C$ and $\mathcal{E} : \mathcal{K}^{op} \to \Set$ is a subfunctor of $\Hom(\mathcal{F}(-),X)$.
Morphisms $f : \mathcal{F}(K) \to X$ that belong to $\mathcal{E}$ will be called \emph{marked}.
A morphism of marked objects is a morphism of the underlying objects that preserves marked morphisms.
The category of marked objects will be denoted by $\C^m$.
The forgetful functor $U : \C^m \to \C$ has a left adjoint $(-)^\flat : \C \to \C^m$ and a right adjoint $(-)^\sharp : \C \to \C^m$.

Let $\mathcal{K} = \{ \Delta^0, \Delta^1 \times \Delta^1 \}$.
Note that $\mathcal{K} = \{ \Delta^0 \join L\ |\ L \in \mathcal{L} \}$, where $\mathcal{L} = \{ \varnothing, \Lambda^2_2 \}$.
The Joyal model structure induces a model structure on the category of \K-marked simplicial sets.
It was shown in \cite{marked-obj} that there is a model structure on the category of marked simplicial sets with the following properties:
\begin{itemize}
\item A map of marked simplicial sets is a cofibration if and only if its underlying map is a monomorphism
\item A makred simplicial set $X$ is fibrant if and only if its underlying simplicial set is a finitely complete quasicategory,
a map $\Delta^0 \to X$ is marked if and only if it corresponds to a terminal object of $X$, and
a map $\Delta^1 \times \Delta^1 \to X$ is marked if and only if it corresponds to a Cartesian square.
\item A map of fibrant marked simplicial sets is a weak equivalence if and only if its underlying map is a homotopy equivalence of quasicategories.
\end{itemize}

In this section we define a model category $\Mod{T}^m$ of marked models of a theory $T$ with $\Sigma$-types.
We construct a Quillen adjunction $\mathfrak{C}^m \dashv N^m$ between $\sSet^m$ and $\Mod{T}^m$,
so that the following square of left Quillen functors commutes up to a natural isomorphism:
\[ \xymatrix{ \sSet \ar[d]_{(-)^\flat} \ar[r]^{\mathfrak{C}} & \Mod{T} \ar[d]^{(-)^\flat} \\
              \sSet^m \ar[r]_{\mathfrak{C}^m}                & \Mod{T}^m
            } \]

We prove that $(-)^\flat : \Mod{T} \to \Mod{T}^m$ is a Quillen equivalence.
Moreover, if $T = T_\Sigma$, then $\mathfrak{C}^m : \sSet^m \to \Mod{T}^m$ is also a Quillen equivalence.
Thus, the model categories of models of $T_\Sigma$ and finitely complete quasicategories are Quillen equivalent.

Let $\Mod{T}^m$ be the category of $\mathfrak{C}(\mathcal{K})$-marked models of $T$.
To define a model structure on this category, we need to define a functor $R : \Mod{T}^m \to \Mod{T}$.

Let $\C$ and $\D$ be categories, and let $F \dashv G$ be an adjunction between $\C$ and $\D$.
If $\mathcal{K}$ is a set of objects of $\C$, then there is an adjunction $F^m \dashv G^m$ between
the categories $\C^m$ of \K-marked objects and $\D^m$ of $F(\mathcal{K})$-marked objects.
We define $G^m(X)$ as $G(X)$ in which a map $K \to G(X)$ is marked if and only if the adjoint map $F(K) \to X$ is marked in $X$.
Let $F^m(X,\mathcal{E}) = (F(X),F(\mathcal{E}))$.
Then it is easy to see that $F^m$ is left adjoint to $G^m$ and that the following diagram commutes up to natural isomorphisms:
\[ \xymatrix{ \C \ar[r]^{(-)^\flat} \ar[d]^F & \C^m \ar[d]^{F^m} \ar[r]^U & \C \ar[d]^F \\
              \D \ar[r]_{(-)^\flat}          & \D^m \ar[r]_U              & \D
            } \]

\begin{lem}
Let $\C$ and $\D$ be model categories, and let $F \dashv G$ be a Quillen adjunction.
Then, for every functor $\mathcal{F} : \mathcal{K} \to \C$ and every set of marked objects $\mathcal{J}$ of $\C^m$,
the adjunction $F^m \dashv G^m$ is a Quillen adjunction between $\C^m_\mathcal{J}$ and $\D^m_{F^m(\mathcal{J})}$.
\end{lem}
\begin{proof}
TODO
\end{proof}

Let us define a set $\mathcal{J}$ of $\mathfrak{C}(\mathcal{K})$-marked models of a dependent type theory $T$.
This set consists of the following objects:
\begin{enumerate}
\item The initial model in which the only marked type is the interval type.
\item The model generated by types $A,B,C : (ty,0)$ and terms $x : A \vdash f : C$ and $y : B \vdash g : C$.
The only marked square is the pullback square of $f$ and $g$:
\[ \xymatrix{ \Sigma (x : A)\,(y : B)\,(f \idtype g) \ar[r]^-{\pi_2} \ar[d]_{\pi_1} \ar[dr]_{f \circ \pi_1} & B \ar[d]^g \\
              A \ar[r]_f                                                                                    & C
            } \]
The bottom triangle commutes strictly and the homotopy corresponding to the top triangle is determined by the third projection.
\end{enumerate}
We define $\Mod{T}^m$ as the category of $\mathfrak{C}(\mathcal{K})$-marked objects localized at $\mathcal{J}$.

\begin{thm}
The adjunction $\mathfrak{C}^m \dashv N^m$ is a Quillen equivalence between $\sSet^m$ and $\Mod{T}^m$.
\end{thm}
\begin{proof}
TODO
\end{proof}

\bibliographystyle{amsplain}
\bibliography{ref}

\end{document}