enriched-cwa.tex

\documentclass[reqno]{amsart}

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

\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{\axlabel}[1]{(#1) \phantomsection \label{ax:#1}}
\newcommand{\axtag}[1]{\label{ax:#1} \tag{#1}}
\newcommand{\axref}[1]{(\hyperref[ax:#1]{#1})}

\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}

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

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

\newcommand{\fs}[1]{\mathrm{#1}}
\newcommand{\Hom}{\fs{Hom}}
\newcommand{\Ho}{\fs{Ho}}
\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\C}{\cat{C}}
\newcommand{\D}{\cat{D}}
\newcommand{\K}{\cat{K}}
\newcommand{\op}{\fs{op}}
\newcommand{\id}{\fs{id}}
\newcommand{\Id}{\fs{Id}}
\newcommand{\Set}{\fs{Set}}
\newcommand{\sSet}{\fs{sSet}}
\newcommand{\sCat}{\fs{sCat}}
\newcommand{\sfCat}{\fs{sfCat}}
\newcommand{\colim}{\fs{colim}}
\newcommand{\bcat}[1]{\mathbf{#1}}
\newcommand{\Mod}[1]{#1\text{-}\bcat{Mod}}

\newcommand{\I}{\fs{I}}
\newcommand{\J}{\fs{J}}
\newcommand{\we}{\mathcal{W}}
\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{\Jcell}[1][]{\Icell[\J#1]}
\newcommand{\Jcof}[1][]{\Icof[\J#1]}
\newcommand{\Jinj}[1][]{\Iinj[\J#1]}

\numberwithin{figure}{section}

\newcommand{\ct}{%
  \mathchoice{\mathbin{\raisebox{0.25ex}{$\displaystyle\centerdot$}}}%
             {\mathbin{\raisebox{0.25ex}{$\centerdot$}}}%
             {\mathbin{\raisebox{0.25ex}{$\scriptstyle\,\centerdot\,$}}}%
             {\mathbin{\raisebox{0.25ex}{$\scriptscriptstyle\,\centerdot\,$}}}
}

\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{Title}

\author{Valery Isaev}

\begin{abstract}
Abstract
\end{abstract}

\maketitle

\section{Introduction}

\section{Simplicial categories with fibrations}

In this section, we will define a model structure on the category of simplicial categories with fibrations and prove that it is Quillen equivalent to the model category of simplicial categories.

Let us establish some notation and terminology.
We will denote by $\sSet$ and $\sCat$ the categories of simplicial sets and simplicial categories, respectively.
We will denote by $N : \sCat \to \sSet$ the simplicial nerve functor.
A simplicial category is \emph{fibrant} if its simplicial $\Hom$-sets are Kan complexes.
A map of a simplicial category is an \emph{equivalence} if it becomes an isomorphism in the homotopy category.

We will say that a map $g : Y \to Z$ in a simplicial category $\C$ is a \emph{basic fibration} if, for every object $X$, the map of simplicial sets $g \circ - : \Hom(X,Y) \to \Hom(X,Z)$ is a Kan fibration.
For every object $Z$ of $\C$, we define a simplicial category $\C/Z$ as follows.
Its objects are basic fibrations $f : X \to Z$ and the simplicial set $\Hom_{\C/Z}(X,Y)$ of morphisms between $f : X \to Z$ and $g : Y \to Z$ is the following pullback:
\[ \xymatrix{ \Hom_{\C/Z}(X,Y) \ar[r] \ar[d] & \Hom_\C(X,Y) \ar[d]^{g \circ -} \\
              1 \ar[r]_-f                    & \Hom_\C(X,Z)
            } \]
The composition and identity maps are defined in the obvious way.
Since $g \circ -$ is a Kan fibration, $\Hom_{\C/Z}(X,Y)$ is a Kan complex, so $\C/Z$ is a fibrant simplicial category.
If $\C$ has enough basic fibrations, then $N(\C/Z)$ is equivalent to $N(\C)/Z$:

\begin{prop}[over-cat]
Let $\C$ be a fibrant simplicial category.
Suppose that every map of $\C$ factors into an equivalence followed by a basic fibration.
Then $N(\C/Z)$ is equivalent to $N(\C)/Z$ for every object $Z$ of $\C$.
\end{prop}
\begin{proof}
The proof of \cite[Lemma~6.1.3.13]{lurie-topos} applies in this setting.
\end{proof}

A \emph{simplicial category with fibrations} is a simplicial category which is equipped with a distinguished class of maps, called fibrations.
A morphism of simplicial categories with fibraions is a morphism of simplicial categories preserving fibrations.
The category of small simplicial categories with fibrations is finitely locally presentable since it is the category of models of a finitary essentially algebraic theory.
We will denote this category by $\sfCat$.

We will construct a semi-model structure on the category of small simplicial categories with fibrations.
We will use the notation from \cite{hovey}.
We will work only with combinatorial (left) semi-model categories.
Thus, the following proposition will be useful:

\begin{prop}[semi-model-cat]
Let $\C$ be a category and let $\we$ be a class of morphisms of $\C$.
Then there is a combinatorial semi-model structure on $\C$ with $\we$ as a class of weak equivalences if and only if there are sets $\I$ and $\J$ of morphisms of $\C$ such that the following conditions hold:
\begin{enumerate}
\item $\we$ satisfies 2-out-of-3 and is closed under retracts.
\item $\Iinj \subseteq \we$.
\item $\J \subseteq \Icof$ and every map in $\Jcell$ with a domain which is an $\Icell$ complex belongs to $\we$.
\item $\Jinj \cap \we \subseteq \Iinj$.
\end{enumerate}
The class of cofibrations in this model category is $\Icof$ and the class of fibrations is $\Jinj$.
\end{prop}

This proposition implies that semi-model structures can be transferred:
\begin{prop}[semimodel-transfer]
Let $F : \C \to \D$ be functor between locally presentable categories with a right adjoint $U : \D \to \C$.
Suppose that there is a semi-model structure on $\C$ with $\we$ as the class of weak equivalences, $\I$ as a set of generating cofibrations, and $\J$ as a set of generating trivial cofibrations.
Then there is a semi-model structure on $\D$ with $U^{-1}(\we)$ as the class of weak equivalences, $F(\I)$ as a set of generating cofibrations, and $F(\J)$ as a set of generating trivial cofibrations
if and only if, for every map $f$ in $\Icell[F(\J)]$ with a domain which is an $\Icell[F(\I)]$ complex, the map $U(f)$ is a weak equivalence.
\end{prop}

Recall that the category of small simplicial categories is a combinatorial model category \cite[Proposition~A.3.2.4]{lurie-topos}.
The forgetful functor $U : \sfCat \to \sCat$ has both left and right adjoints.
Moreover, $U \circ (-)^\flat$ is isomorphic to $\Id$, where $(-)^\flat$ is the left adjoint of $U$.
It follows that the model structure on $\sCat$ can be transferred to $\sfCat$.
Moreover, $(-)^\flat \dashv U$ is a Quillen equivalence between $\sCat$ and $\sfCat$.

Let $\C$ be a combinatorial semi-model category with $\I$ and $\J$ as sets of generating cofibrations and generating trivial cofibrations, respectively.
Let $S$ be a set of maps of $\C$ such that maps in $\Icell[(\J \cup S)]$ with domains in $\Icell[(\I \cup S)]$ are weak equivalences.
Then \rprop{semi-model-cat} implies that $\I \cup S$ and $\J \cup S$ are sets of generating cofibrations and generating trivial cofibrations, respectively, for a semi-model structure on $\C$ with the same class of weak equivalences.
Moreover, the identity functor is a Quillen equivalence between the original model structure and the new one.

Let $[0]$ be the terminal simplicial category and let $[1]$ be the walking arrow considered as simplicial category with discrete simplicial $\Hom$-sets.
Let $[1]_f$ be the simplicial category with fibrations which has two objects and one non-identity map which is a fibration.
Consider the simplicial category with fibrations $[1] \amalg_{[0]} [1]_f$, where $[0] \to [1]_f$ and $[0] \to [1]_e$ choose the codomain and the domain of the walking arrow, respectively.
Let $\varphi : [1] \to [1] \amalg_{[0]} [1]_f$ be the unique morphism which chooses the composite of $[1]$ and $[1]_f$.
We can represent this morphism as the following diagram:
\[ \xymatrix{                               & \circ \ar@{-->>}[dr] & \\
              \bullet \ar@{-->}[ur] \ar[rr] &                      & \bullet
            } \]
This diagram represents the codomain of $\varphi$ codomain.
The subdiagram consisting of solid arrows and $\bullet$ represents the domain of $\varphi$.
The map $\varphi$ is the obvious inclusion.

Let $[1]_e$ be any simplicial category weakly equivalent to $[0]$ such that there exists a cofibration $[1] \to [1]_e$.
Let $\tau$ be the composite $[1] \to [1]_e \to [1]_e \amalg_{[0]} [1]_f$.
This morphism can be represented as the following diagram:
\[ \xymatrix{                                        & \circ \ar@{-->>}[dr] & \\
              \bullet \ar@{-->}[ur]^{\simeq} \ar[rr] &                      & \bullet
            } \]
If $Z$ is a simplicial category with fibrations such that the underlying simplicial category is fibrant,
then $Z$ has the right lifting property with respect to $\tau$ if and only if every map factors into an equivalence followed by a fibration.

Finally, let $\gamma : [0] \to [1]_f$ be the morphism that maps the unique object of $[0]$ to the codomain of $[1]_f$.
This morphism can be represented as follows:
\[ \xymatrix{ \circ \ar@{-->>}[r] & \bullet } \]

If $V$ is a simplicial set and $U$ is a simplicial subset of $V$, then we will denote by $[2]_{U,V}$ the simplicial category with fibrations that has three objects $0$, $1$, and $2$ such that
\[ \Hom_{[2]_{U,V}}(x,y) =
  \begin{cases}
    \varnothing & \quad \text{if } x > y \\
    \Delta^0    & \quad \text{if } x = y \\
    U           & \quad \text{if } x = 0, y = 1 \\
    \Delta^0    & \quad \text{if } x = 1, y = 2 \\
    V           & \quad \text{if } x = 0, y = 2
  \end{cases}
\]
The composition is defined in the obvious way.
The only fibration in $[2]_{U,V}$ is the unique map between $1$ and $2$.
Then we have the obvious maps $\lambda^n_k : [2]_{\Lambda^n_k,\Delta^n} \to [2]_{\Delta^n,\Delta^n}$.
A simplicial category with fibrations $Z$ has the right lifting property with respect to the maps $\lambda^n_k$ if and only if every fibration in $Z$ is a basic fibration.

\begin{lem}
Let $S_0 = \{ \lambda^n_k \mid k \leq n, n \in \mathbb{N} \}$.
Then sets $\{ \varphi \} \cup \I^\flat \cup S_0$, $\{ \tau \} \cup \I^\flat \cup S_0$, and $\{ \gamma \} \cup \I^\flat \cup S_0$ generate the same class of cofibrations.
We will denote this class by $\mathcal{C}$.
\end{lem}
\begin{proof}
The map $\tau$ is a composite of $\varphi$ and a cofibration from $\Icof^\flat$.
The map $\gamma$ is a retract of the cofibration $[0] \to [1] \xrightarrow{\varphi} [1]_e \amalg_{[0]} [1]_f$.
Thus, we just need to show that $\varphi$ belongs to $\Icof[(\{ \gamma \} \cup \I^\flat \cup S_0)]$.
Consider the morphism $i : [1] \to [2]_{\Lambda^1_1,\Delta^1}$ which maps the non-identity arrow of $[1]$ to the map between $0$ and $2$ which is not the composite of the maps $0 \to 1 \to 2$.
This morphism is a composite of maps from $\{ \gamma \} \cup \I^\flat$.
The map $\varphi$ is a retract of $[1] \xrightarrow{i} [2]_{\Lambda^1_1,\Delta^1} \xrightarrow{\lambda^1_1} [2]_{\Delta^1,\Delta^1}$.
\end{proof}

\begin{prop}
There is a semi-model structure on the category of small simplicial categories with fibrations satisfying the following properties.
Weak equivalences are precisely the maps that are weak equivalences of the underlying simplicial categories.
The class of cofibrations is $\mathcal{C}$.
A simplicial category with fibrations $Z$ is fibrant if and only if the following conditions hold:
\begin{enumerate}
\item \label{it:fib-a} The underlying simplicial category of $Z$ is fibrant.
\item \label{it:fib-b} Every map in $Z$ factors into an equivalence followed by a fibration.
\item \label{it:fib-c} Every fibration in $Z$ is a basic fibration.
\end{enumerate}
Every fibration $p : \Hom(x,y)$ in a cofibrant simplicial category with fibrations is an epimorphism (that is, the map $- \circ p : \Hom(y,b) \to \Hom(x,b)$ is a monomorphism of simplicial sets for every object $b$).
The forgetful functor $U : \sfCat \to \sCat$ is the right part of a Quillen equivalence.
\end{prop}
\begin{proof}
Let $S = \{ \tau \} \cup S_0$.
A simplicial category with fibrations satisfies conditions \eqref{it:fib-a}-\eqref{it:fib-c} if and only if it has the right lifting property with respect to $\J^\flat \cup S$.
Thus, we just need to show that maps in $\Icell[(\J^\flat \cup S)]$ with domains in $\Icell[(\I^\flat \cup S)]$ are weak equivalences (of simplicial categories).
Since weak equivalences are closed under transfinite composition, it is enough to prove that pushouts of maps in $S$ with domains in $\Icell[(\I^\flat \cup S)]$ are weak equivalences.

Let $h : \Hom_Z(a,c)$ be a map in a simplicial category with fibrations.
Let $\tau' : Z \to Z'$ be the pushout of $\tau$ along the map $[1] \to Z$ corresponding to $h$.
We need to show that $\tau'$ is a weak equivalence.
The only object of $Z'$ that does not belong to $Z$ is $b$ and it is equivalent to $a$.
Thus, we just need to show that, for every pair of objects $x$ and $y$ of $Z$, the map $\Hom_Z(x,y) \to \Hom_{Z'}(\tau'(x),\tau'(y))$ is a weak equivalence of simplicial sets.
The map $\tau$ can be factored into maps $[1] \xrightarrow{\varphi} [1] \amalg_{[0]} [1]_f \xrightarrow{e} [1]_e \amalg_{[0]} [1]_f$.
Let $\varphi'$ and $e'$ be pushouts of $\varphi$ and $e$, respectively.
The map $\Hom_Z(x,y) \to \Hom(\varphi'(x),\varphi'(y))$ is an isomorphism.
The proof that the map $\Hom(\varphi'(x),\varphi'(y)) \to \Hom(e'(x),e'(y))$ is a weak equivalence is the same as in \cite[Proposition~A.3.2.4]{lurie-topos}.

Now, let us prove that every fibration $p : \Hom(x,y)$ in a cofibrant simplicial category with fibrations is an epimorphism.
It is enough to prove this for $\Icell[(\I^\flat \cup S)]$ complexes since every cofibrant simplicial category with fibrations is a retract of such a complex.
Let $Z$ be an $\Icell[(\I^\flat \cup S)]$ complex.
Then $Z = \colim_{\alpha < \lambda} Z_\alpha$, where $Z_\alpha \to Z_{\alpha + 1}$ is a pushout of a map in $\I^\flat \cup S$, $Z_0 = 0$, and $Z_\kappa = \colim_{\alpha < \kappa} Z_\alpha$.
We will prove by induction on $\lambda$ that, for every fibration $p : \Hom_Z(x,y)$ and every object $b$, the map $- \circ p : \Hom_Z(y,b) \to \Hom_Z(x,b)$ is a monomorphism.
This is obvious for $\lambda = 0$.
For limit ordinals, this follows from induction hypothesis.
If $\lambda = \alpha+1$, then $Z_\alpha \to Z_{\alpha+1}$ is a pushout of one of the generating cofibrations.
If it is a cofibration of the form $f^\flat$, then we can use the description of simplicial $\Hom$-sets of $Z_{\alpha+1}$ given in \cite[Proposition~A.3.2.4]{lurie-topos} to conclude that $- \circ p$ is a monomorphism.
If it is $\tau$, then the description of simplicial $\Hom$-sets given above implies that $- \circ p$ is an isomorphism.
If it is $\lambda^n_k$, then simplicial $\Hom$-sets can be explicitly described in a similar way.
This description also implies $- \circ p$ is a monomorphism.

Finally, let $Z$ be a $\Icell[(\I^\flat \cup S)]$ complex and let $\lambda' : Z \to Z'$ be a pushout of a map $\lambda^n_k : [2]_{\Lambda^n_k,\Delta^n} \to [2]_{\Delta^n,\Delta^n}$.
Let $z$ be the image of $0$ and let $p : \Hom(x,y)$ be the image of the unique fibration in $[2]_{\Lambda^n_k,\Delta^n}$.
For every object $c$, we define a map of simplicial sets $f(c)$ as the pushout-product of $\Lambda^n_k \to \Delta^n$ and $- \circ p : \Hom_Z(y,c) \to \Hom(x,c)$.
Since $p$ is a fibration in a cofibrant simplicial category with fibrations, $- \circ p$ is a cofibration and $f(c)$ is a trivial cofibration.

Let $a$ and $b$ be a pair of objects of $Z$.
We define a sequence of trivial cofibrations of simplicial sets $f_i : N_i \to M_i$ as follows:
$f_0 = \id_{\Hom_Z(a,z)} \times f(b)$ and $f_{i+1}$ is the pushout-product of $f_i$ and $f(z)$.
We can also define maps $g_i : N_i \to \Hom_Z(a,b)$ such that $\tau'_{a,b} : \Hom_Z(a,b) \to \Hom_{Z'}(\tau'(a),\tau'(b))$ is the pushout of $\coprod_{i \in \mathbb{N}} f_i$ along $[g_i]_{i \in \mathbb{N}}$.
Since $f_i$ are trivial cofibrations, $\tau'_{a,b}$ is also a trivial cofibration.
Since $\tau' : Z \to Z'$ is surjective on objects, this implies that it is a weak equivalence of simplicial categories.
\end{proof}

\section{Categories of marked objects}

Categories of marked objects were defined in \cite{marked-obj}.
Here, we recall their definition and basic properties.

\begin{defn}[marked-obj]
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$.
\end{defn}

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$.
For every $X \in \C$, $X^\flat$ is the marked object in which no morphisms are marked (that is, $X^\flat = (X,\varnothing)$),
and $X^\sharp$ is the marked object in which all morphisms are marked (that is, $X^\sharp = (X,\coprod_{K \in \mathcal{K}} \Hom(K,X))$).
Objects of the form $X^\flat$ and of the form $X^\sharp$ will be called \emph{flat} and \emph{sharp} respectively.

\begin{thm}[mark-main]
Let $\C$ be a combinatorial model category and let $\mathcal{F} : \mathcal{K} \to \C$ be a functor such that, for every $K \in \mathcal{K}$, the object $\mathcal{F}(K)$ is cofibrant.
Then $\C^m$ is a combinatorial model category in which a map is a cofibration if and only if the underlying map is a cofibration in $\C$.
Both adjoint pairs $(-)^\flat \dashv U$ and $U \dashv (-)^\sharp$ are Quillen pairs.
If $\C$ is left proper, then so is $\C^m$.
A marked object $X$ is fibrant in $\C^m$ if and only if the following conditions hold:
\begin{itemize}
\item The underlying object $U(X)$ is fibrant in $\C$
\item Marked maps in $X$ are stable under homotopy (that is, if two maps $K \to U(X)$ are homotopic and one of them is marked, then so is the other).
\end{itemize}
A map $f$ is a weak equivalence in $\C^m$ if and only if its underlying map is a weak equivalence in $\C$ and $R^m(f)$ reflects marked maps, where $R^m : \C^m \to \C^m$ is a fibrant replacement functor

A fibrant replacement functor $R^m$ can be defined as $X \mapsto (R(X),\mathcal{E})$,
where $R$ is a fibrant replacement functor for $\C$ and a map $K \to R(X)$ is marked in $R^m(X)$ if and only if
it is homotopic to a map that factors as a marked map $K \to X$ followed by the map $X \to R(X)$.
\end{thm}

\begin{remark}
This theorem also holds for semi-model categories with one additional assumption that the domains of generating cofibrations are cofibrant.
This assumption is required for Jeff Smith's theorem for semi-model categories \cite[Theorem~3.1]{semi-smith}.
\end{remark}

The model category of marked objects has an explicit description of mapping spaces:

\begin{lem}[marked-hom]
Let $X$ and $Y$ be a pair of marked objects and let $\mathrm{Map}(U(X),U(Y))$ be the mapping space in $\C$.
Then $\mathrm{Map}(X,Y)$ is a Kan subcomplex of $\mathrm{Map}(U(X),U(Y))$ consisting of those connected components in which one of the vertices correspond to a marked map $X \to Y$.
\end{lem}
\begin{proof}
By \cite[Lemma~3.4]{marked-obj}.
\end{proof}

We want to use the category of marked objects to described (non-full) $\infty$-subcategories of the $\infty$-category $\Ho_\infty(\C)$ corresponding to $\C$,
that is we want to find a model structure on $\C^m$ such that $\Ho_\infty(U) : \Ho_\infty(\C^m) \to \Ho_\infty(\C)$ is a monomorphism of $\infty$-categories.
A functor $U : \D \to \C$ between $\infty$-categories is a monomorphism if and only if the following conditions hold:
\begin{enumerate}
\item \label{it:mono-hom} For every pair of objects $x$ and $y$ of $\D$, the map $\Hom(x,y) \to \Hom(U(x),U(y))$ is a monomorphism of spaces.
\item \label{it:mono-eq} For every pair of objects $x$ and $y$ of $\D$ and every equivalence $e$ between $U(x)$ and $U(y)$, there is an equivalence $e'$ between $x$ and $y$ such that $U(e')$ is homotopic to $e$.
\end{enumerate}

The first condition holds by \rlem{marked-hom}, but the second one does not usually hold for all marked objects.
We can consider some full $\infty$-subcategory of $\Ho_\infty(\C^m)$ for which it holds.
One way to describe such $\infty$-categories is to take left Bousfield localizations of $\C^m$.
The following proposition gives a sufficient condition for such a localization to be an $\infty$-subcategory of $\Ho_\infty(\C)$:

\begin{prop}[marked-mono]
Let $\C^m_L$ be a left Bousfield localization of $\C^m$ such that, for every pair of fibrant objects $X$ and $Y$ of $\C^m_L$, every weak equivalence $f : U(X) \to U(Y)$ preserves and reflects marked maps.
Then $\Ho_\infty(U) : \Ho_\infty(\C^m_L) \to \Ho_\infty(\C)$ is a monomorphism of $\infty$-categories.
\end{prop}
\begin{proof}
Condition~\eqref{it:mono-hom} is true by \rlem{marked-hom}.
Let us prove that condition~\eqref{it:mono-eq} also holds for $\Ho_\infty(U)$.
Let $X$ and $Y$ be a pair of fibrant objects of $\C^m_L$.
Then every equivalence in $\Ho_\infty(\C)$ between $U(X)$ and $U(Y)$ can be presented as a span $p : Z \to U(X)$, $q : Z \to U(Y)$, where $q$ is a weak equivalence and $p$ is a trivial fibration.
We will say that a map $k : K \to Z$ is marked if $p \circ k$ is marked.
This makes $Z$ into a marked object $Z'$ such that $p$ lifts to a trivial fibration $p' : Z' \to X$.
This implies that $Z$ is a fibrant object in $\C^m_L$.
Now, by the assumption, the map $q : Z \to U(Y)$ preserves and reflects marked maps,
which implies that it lifts to a weak equivalence $q' : Z' \to Y$.
\end{proof}

\begin{example}
Let $\mathcal{L}$ be a set of simplicial sets and let $\mathcal{K} = \{ \Delta^0 * L \mid L \in \mathcal{L} \}$.
It is proved in \cite[Proposition~4.1]{marked-obj} that there is a left Bousfield localization $\sSet_\mathcal{L}$ of the category of $\mathcal{K}$-marked simplicial sets
in which a marked simplicial set $X$ is fibrant if and only if $X$ is a quasicategory and a cone in $X$ is marked if and only if it is a limit cone.
Since an equivalence of quasicategories always preserves and reflects limit cones, the condition of \rprop{marked-mono} holds.
Thus, the $\infty$-category corresponding to this model category is the $\infty$-category of $\infty$-categories with limits of given shapes and functors preserving them.
In particular, $\sSet_{\{ \varnothing, \Lambda^2_2 \}}$ presents the $\infty$-category of finitely complete $\infty$-categories and functors preserving finite limits.
\end{example}

% TODO: Give a characterization of S-local objects.

It is often convenient to work with categories in which objects have chosen lifts for certain maps.
Let $S$ be a set of maps of a category $\C$.
Then there is a category $\C_S$ with objects $(X,\mathcal{E})$, where $X$ is an object of $\C$ and $\mathcal{E}$ is a function that, for every map $A \to B$ in $S$ and every map $A \to X$ gives a lift in the following diagram:
\[ \xymatrix{ A \ar[r] \ar[d] & X \\
              B \ar@{-->}[ur]
            } \]
Morphisms in $\C_S$ are morphisms of the underlying objects preserving chosen lifts.
We will use the following theorem to construct a semi-model structure on $\C_S$:

\begin{thm}[alg-fib-obj]
Suppose that $\C$ is a cofibrantly generated semi-model category in which all cofibrations are monomorphisms.
Let $S$ be a set of trivial cofibrations of $\C$.
Then there is a model structure on $\C_S$ in which a map is a fibration or a weak equivalence if and only if its underlying map is such in $\C$.
The forgetful functor $U : \C_S \to \C$ preserves cofibrations and it is a right Quillen functor and a part of a Quillen equivalence.
If $\C$ is a model category, then so is $\C_S$.
\end{thm}
\begin{proof}
This follows from results of \cite{algebraic-fibrant-objects}.
This theorem differs from \cite[Theorem~2.20]{algebraic-fibrant-objects} in two ways.
First, we do not assume that trivial cofibrations in $S$ determine fibrant objects, but this assumption is superfluous and was never used in \cite{algebraic-fibrant-objects}.
The second difference is that we only assume that $\C$ is a semi-model category.
To construct a semi-model structure on $\C_S$, we need to show that maps in $\Icell[F(\J)]$ with cofibrant domains are weak equivalences.
This can be done in the same way as in \cite[Theorem~2.20]{algebraic-fibrant-objects} using the fact that $U$ preserves cofibrant objects (which is true by \cite[Corollary~2.18]{algebraic-fibrant-objects}).
\end{proof}

Let $\C$ be a combinatorial semi-model category $\C$ in which all cofibrations are monomorphisms.
Let $S$ be a set of cofibrations with cofibrant codomains of $\C$.
We want to construct a semi-model structure on $\C_S$.
We cannot use \rthm{alg-fib-obj} directly since morphisms in $S$ are not weak equivalences, but we can combine this theorem with \rthm{mark-main} to get the desired result.
Let $\mathcal{F} : S \to \C$ be the codomain function considered as a functor from a discrete category.
Let $\C^m$ be the category of $\mathcal{F}$-marked objects.
We can make $S$ into a set of maps of marked objects in which only the identity maps on the codomains of morphisms in $S$ are marked.
We will denote the corresponding set of maps in $\C^m$ by $S^m$.
Let $\C^m_L$ be the left Bousfield localization of $\C^m$ at the set $S^m$.
By \rthm{alg-fib-obj}, there is a left-semi model structure on the category $\C^m_{L,S}$ of marked objects with chosen $S^m$-lifts such that the forgetful functor $\C^m_{L,S} \to \C^m_L$ is a part of a Quillen equivalence.
We can define a semi-model structure on $\C_S$ which is Quillen equivalent to $\C^m_{L,S}$:

\begin{thm}[lift-model-cat]
Let $\C$ be a combinatorial semi-model category $\C$ in which all cofibrations are monomorphisms.
Suppose that there is a set $\I$ of generating cofibrations of $\C$ in which all maps have cofibrant domains.
Let $S$ be a set of cofibrations with cofibrant codomains.
Let $\C^m_L$ be the left Bousfield localization of $\C^m$ such that maps in $S^m$ are weak equivalences in $\C^m_L$.
Then there is a semi-model structure on $\C_S$ which satisfies the following properties:
\begin{enumerate}
\item \label{it:alg-cof} If $F_S : \C \to \C_S$ is the left adjoint of the forgetful functor $U_S : \C_S \to \C$, then $F_S(\I)$ is a set generating cofibrations of $\C_S$.
\item \label{it:alg-we} If $(-)^\flat : \C_S \to \C^m_{L,S}$ be the left adjoint to the forgetful functor $U^m_{L,S} : \C^m_{L,S} \to \C_S$, then a map $f$ of $\C_S$ is a weak equivalence if and only if $f^\flat$ is a weak equivalence.
\item Both adjunctions $F_S \dashv U_S$ and $(-)^\flat \dashv U^m_{L,S}$ are Quillen adjunctions and the latter one is a Quillen equivalence.
\item \label{it:alg-qe} The semi-model category $\C_S$ is Quillen equivalent to $\C^m_L$ and this Quillen equivalence commutes with forgetful functors $U_S : \C_S \to C$ and $U^m : \C^m_L \to \C$.
\end{enumerate}
\end{thm}
\begin{proof}
Conditions~\eqref{it:alg-cof} and \eqref{it:alg-we} determine cofibrations and weak equivalences of $\C_S$.
We will construct the semi-model structure on $\C_S$ using Smith's theorem \cite[Theorem~3.1]{semi-smith}.
Since $(-)^\flat : \C_S \to \C^m_{L,S}$ is a left adjoint, most of the conditions of this theorem hold trivially.
We just need to prove that maps in $\Iinj[F_S(\I)]$ are weak equivalences.
Let $f : X \to Y$ be a map in $\Iinj[F_S(\I)]$.
Then $U_S(f)$ is a trivial fibration in $\C$.
Thus, we just need to prove that $R^m(f^\flat)$ reflects marked maps.
Let $i : A \to B$ be a map in $S$ and let $k : B \to R(X)$ be a map such that $R(f) \circ k$ is marked in $R^m(Y)$.
Then $R(f) \circ k$ is homotopic to a map of the form $B \xrightarrow{g} Y \to R(Y)$, where $g$ is the chosen lift for $g \circ i$.
Since $B$ is cofibrant and $U_S(f)$ is a trivial fibration, we have a map $g' : B \to X$ such that $U_S(f) \circ g' = g$.
If $g'' : B \to X$ is the chosen lift for $g' \circ i$, then $U_S(f) \circ g'' = g$ since $f$ preserves chosen lifts.
Since $g''$ is marked in $X^\flat$, we just need to show that $B \xrightarrow{g''} X \to R(X)$ is homotopic to $k$.
Since $B$ is cofibrant and $R(f)$ is a weak equivalence between fibrant objects, this follows from the fact that $B \xrightarrow{g''} X \to R(X) \xrightarrow{R(f)} R(Y)$ is homotopic to $R(f) \circ k$.

We have the following commutative (up to isomorphism) square of left adjoint functors:
\[ \xymatrix{ \C \ar[r]^{(-)^\flat} \ar[d]_{F_S} & \C^m_L \ar[d]^{F^m} \\
              \C_S \ar[r]_{(-)^\flat}            & \C^m_{L,S}
            } \]
The functor $F_S$ preserves cofibrations by definition and it preserves trivial cofibrations since $F^m \circ (-)^\flat$ preserves them.
The functor $(-)^\flat : C_S \to C^m_{L,S}$ preserves cofibrations since $F^m \circ (-)^\flat$ preserves them.
Also, it preserves weak equivalence by definition.
Thus, $F_S \dashv U_S$ and $(-)^\flat \dashv U^m_{L,S}$ are Quillen adjunctions.
Since $(-)^\flat$ preserves and reflects weak equivalences, to prove that the latter adjunction is a Quillen equivalence, it is enough to show that the counit $\varepsilon_X : (U^m_{L,S}(X))^\flat \to X$ is a weak equivalence for every fibrant object $X$.
Since the underlying map of $\varepsilon_X$ is the identity, we just need to prove that $R^m(\varepsilon_X)$ reflects marked maps.
Let $i : A \to B$ be a map in $S$ and let $k : B \to X$ be a marked map.
If $k' : B \to X$ be the chosen lift for the map $k \circ i$, then $k'$ is marked in $(U^m_{L,S}(X))^\flat$.
Since $i$ is a trivial cofibration, $X$ is fibrant, and $k \circ i = k' \circ i$, it follows that $k$ and $k'$ are homotopic.
Thus, $k$ is also marked in $R^m((U^m_{L,S}(X))^\flat)$.

Property~\eqref{it:alg-qe} follows from the facts that $(-)^\flat \dashv U^m_{L,S}$ and $F^m \dashv U^m$ are Quillen equivalences and the square of left adjoint functors above commutes.
\end{proof}

Let $X$ be an object of $\C_S$ and let $R(X^\flat)$ be the marked object which has $X$ as its underlying object and a map is marked in it if it is homotopic to a marked map in $X^\flat$.
If $R(X^\flat)$ is fibrant, then $X$ is also fibrant.
The converse holds if $S$ is complete in a certain sense.

\begin{lem}[lift-we]
Let $S$ be a set of maps of a category $\C$ satisfying conditions of \rthm{lift-model-cat}.
Let $X$ and $Y$ be objects such that $R(X^\flat)$ and $R(Y^\flat)$ are fibrant in $\C^m_{L,S}$.
Then a map $f : X \to Y$ is a weak equivalence in $\C_S$ if and only if $U_S(f)$ is a weak equivalence in $\C$.
\end{lem}
\begin{proof}
% The functor $U_S$ preserves fibrant objects and weak equivalences between fibrant objects since it is a right Quillen functor.
% Let $X$ be an object of $\C_S$ such that $U_S(X)$ is fibrant.
% To prove that $X$ is fibrant, it is enough to show that there is a choice of markings on $X$ which makes it into a fibrant object of $\C^m_{L,S}$.
% We let every map that a homotopic to a marked map in $X^\flat$ be marked.
% Since the forgetful functor $\C^m_{L,S} \to \C^m_L$ reflects fibrant objects, we just need to show that $U_S(X)$ with this choice of markings is fibrant in $\C^m_L$.
% We choose markings in such a way that this object is fibrant if and only if it is $S^m$-local.
% By assumption, this is true if it has the RLP with respect to $S^m$, which is true since it is an object of the form $U_S(X)$.

The functor $U_S$ preserves weak equivalences between fibrant objects since it is a right Quillen functor.
Let $f : X \to Y$ be a weak equivalence.
Since the forgetful functor $\C^m_{L,S} \to \C^m_L$ reflects weak equivalences between fibrant objects, we just need to show that $R(f^\flat)$ is a weak equivalence in $\C^m_L$.
This follows from the fact that $R(X^\flat)$ and $R(Y^\flat)$ are $S^m$-local and weak equivalences between $S^m$-local objects are just weak equivalences in the underlying category.
\end{proof}

\section{Models of type theories}

In this section, we recall the definition of algebraic type theories.
For every algebraic type theory, we define several categories of its models.
We also construct semi-model structures on these categories for sufficiently nice theories.

We will work with essentially algebraic theory presented in the form of a partial Horn theory as defined in \cite{PHL}.
Such a theory consists of a set of sorts $\mathcal{S}$, a set of function symbols $\mathcal{F}$, a set of predicate symbols $\mathcal{P}$, and a set of axioms $\mathcal{A}$.
Every function symbol $\sigma \in \mathcal{F}$ has a signature $\sigma : s_1 \times \ldots \times s_k \to s$, where $s_1, \ldots s_k, s$ are sorts.
Every predicate symbol $R \in \mathcal{P}$ has a signature $R : s_1 \times \ldots \times s_k$.
\emph{Terms} are constructed from function symbols and variables in the usual way.
\emph{Formulas} are constructed from terms, predicate symbols, equality sign, and finite conjunctions in the usual way.
A \emph{restricted term} is an expression of the form $t|_\varphi$, where $t$ is a term and $\varphi$ is a formula.
A \emph{sequent} is a pair of formulas together with a set of variables, written $\varphi \sststile{}{V} \psi$.
The set of axioms consists of sequents.
Derivations are constructed from rules for symmetry, transitivity, and congruence.
The precise set of rules can be found in \cite{PHL,alg-tt,morita-equiv}.

A \emph{derived sort} is an expression of the form $\{ (x_1, \ldots x_l) : s_1 \times \ldots \times s_l \mid \varphi \}$,
where $\varphi$ is a formula with variables in $\{ x_1 : s_1, \ldots x_l : s_l \}$.
It is convenient to think of (restricted) terms as derived function symbols.
If $t$ is a term of sort $s$ such that $\fs{FV}(t) \subseteq \{ x_1 : s_1, \ldots x_k : s_k \}$, then we can write $t : s_1 \times \ldots \times s_k \to s$.
Similarly, we can think of formulas as derived predicate symbols.

We can work with (derived) function symbols which have derived sorts in their signature.
Let $s_i' = \{ \overline{x^i} : \overline{s^i} \mid \varphi^i \}$ and $s' = \{ \overline{y} : \overline{s} \mid \psi \}$.
Then a function symbol $\sigma$ with signature $s_1' \times \ldots \times s_k' \to s'$ is a collection of function symbols
$\{ \sigma^j : \overline{s^1} \times \ldots \times \overline{s^{l_j}} \to s_i \}_{1 \leq j \leq l}$ together with the following axiom:
\[ \bigwedge_{1 \leq j \leq l} \sigma^j(\overline{x^1}, \ldots \overline{x^{l_j}})\!\downarrow\ \sststile{}{\{ \overline{x^1}, \ldots \overline{x^{l_j}} \}_{1 \leq j \leq l}} \psi[\{ \sigma^j(\overline{x^1}, \ldots \overline{x^{l_j}})/y_j \}_{1 \leq j \leq l}] \land \bigwedge_{1 \leq i \leq k} \varphi^i. \]
Predicate symbols with derived signature are define in a similar way.

A \emph{generalized morphism} of theories $T$ and $T'$ can be defined as a finitary right adjoint functor $\Mod{T'} \to \Mod{T}$.
If $f : T \to T'$ is a generalized morphism, we will denote the corresponding adjunction by $f_! \dashv f^*$.
Generalized morphisms can often be conveniently described syntactically.
To define such a morphism, we need to specify the following data:
\begin{enumerate}
\item A function $f$ from the set of sorts of $T$ to the set of derived sorts of $T'$.
\item A function $f$ from the set of function symbols of $T$ to the set of restricted terms of $T'$ such that, if $\sigma : s_1 \times \ldots \times s_k \to s$, then $f(\sigma) : f(s_1) \times \ldots \times f(s_k) \to f(s)$.
\item A function $f$ from the set of predicate symbols of $T$ to the set of formulas of $T'$ such that, if $R : s_1 \times \ldots \times s_k$, then $f(R) : f(s_1) \times \ldots \times f(s_k)$.
\end{enumerate}
These functions can be extended to functions on terms and formulas.
Thus, for every sequent $\varphi \sststile{}{V} \psi$ in $T$, we get a sequent $f(\varphi) \sststile{}{V} f(\psi)$ in $T'$.
If this function maps axioms of $T$ to theorems in $T'$, then these functions determine a generalized morphism $f : T \to T'$.

Let $\mathcal{S}_c = \{ \fs{ctx}, \fs{tm} \} \times \mathbb{N}$ be a set of sorts.
We will also write $(\fs{ty},n)$ for the sort $(\fs{ctx},n+1)$.
Let $T_0$ be the theory with function symbols $\fs{ft}_n : (\fs{ty},n) \to (\fs{ctx},n)$ and $\fs{ty}_n : (\fs{tm},n) \to (\fs{ty},n)$.
All theories that we will consider will be theories under $T_0$, that is they will be equipped with a generalized morphism from $T_0$.
Moreover, all generalized morphisms between theories will commute with morphisms from $T_0$.

Models of $T_0$ are presheaves on the poset $(\mathcal{S}_c,\leq)$, where $(\fs{ctx},n) \leq (\fs{ty},n)$ and $(\fs{ty},n) \leq (\fs{tm},n)$.
Let $Y : (\mathcal{S}_c,\leq) \to \Mod{T_0}$ be the Yoneda embedding.
Let $\I_0$ be the set of maps $Y(\fs{ctx},n) \to Y(\fs{ty},n)$ and $Y(\fs{ty},n) \to Y(\fs{tm},n)$.
If $T$ is a theory under $T_0$, then the image of $\I_0$ in $\Mod{T}$ will also be denoted by $\I_0$.
We will use this set as a set of generating cofibrations for various theories $T$.

Algebraic type theories were defined in \cite{alg-tt}.
The most basic such theory is the theory of substitution $(\mathcal{S}_c, \mathcal{F}_s, \varnothing, \mathcal{A}_s)$.
The category of models of this theory is equivalent to the category of contextual categories.
Every algebraic type theory can be presented in the form $(\mathcal{S}_c, \mathcal{F}_s \amalg \{ \sigma_m \mid \sigma \in \mathcal{F}_0, m \in \mathbb{N} \}, \{ R_m \mid R \in \mathcal{P}_0, m \in \mathbb{N} \}, \mathcal{A}_s \amalg \mathcal{A})$.
Elements of $\mathcal{F}_0$ and $\mathcal{P}_0$ are called basic function and basic predicate symbols, respectively.
If $\sigma : (p_1,n_1) \times \ldots \times (p_k,n_k) \to (p,n)$ is a basic function symbol, then $\sigma_m : (\fs{ctx},m) \times (p_1,n_1+m) \times \ldots \times (p_k,n_k+m) \to (p,n+m)$.
Similarly, if $R : (p_1,n_1) \times \ldots \times (p_k,n_k)$ is a basic predicate symbol, then $R_m : (\fs{ctx},m) \times (p_1,n_1+m) \times \ldots \times (p_k,n_k+m)$.
We will not assume that all substitution commutes with all function symbols in all type theories.
We will call type theories that satisfy this property \emph{regular}.
For every type theory $T$, we can define its regular version $T^r$ as $T$ together with axioms asserting that all function symbols commute with substitution.

By definition, type theories are extensions of the theory of substitution.
It follows that models of type theories are contextual categories with additional structures.
Another popular notion of models of type theories is categories with attributes.
A \emph{(non-split) category with attributes} is a category together with a set of types $\fs{Ty}(\Gamma)$ defined for every object $\Gamma$ and the following operations:
\begin{enumerate}
\item For every type $A$ over $\Gamma$, a map $p_A : \Gamma.A \to \Gamma$.
\item For every map $f : \Delta \to \Gamma$ and every type $A$ over $\Gamma$, a type $f^*(A)$ over $\Delta$ (called the pullback of $A$) and a map $f.A : \Delta.f^*(A) \to \Gamma.A$ such that the obvious square is a pullback.
\end{enumerate}
A category with attributes is \emph{split} if $\fs{id}^*(A) = A$ and $(g \circ f)^*(A) = g^*f^*(A)$.

For every type theory $T$, we will define another partial Horn theory $A(T)$ which extends the theory $\fs{CwA}$ of categories with attributes.
Moreover, we will show that $\Mod{T}$ is a coreflective subcategory of $\Mod{A(T)}$.
The set of sorts of $\fs{CwA}$ is defined as $\mathcal{S}_a = \{ \fs{ob}, \fs{hom}, \fs{ty} \}$.
This theory extends the theory of categories.
Thus, it has function symbols $\fs{dom},\fs{cod} : \fs{hom} \to \fs{ob}$, $\fs{id} : \fs{ob} \to \fs{hom}$, and $\circ : \fs{hom} \times \fs{hom} \to \fs{hom}$.
It also has function symbol $\fs{ext} : \fs{ty} \to \fs{hom}$.
In the standard notation, it maps a type $A$ over context $\Gamma$ to the morphism $p_A : \Gamma.A \to \Gamma$.
The theory $\fs{CwA}$ also has function symbols and axioms which assert the existence of a terminal object and pullbacks of types.

For every $s \in \mathcal{S}_c$, we define a derived sort $A(s)$ in the theory of categories with attributes as follows:
\begin{align*}
A((\fs{ctx},n)) & = \{ \overline{B} : \fs{ty}^n \mid \fs{cod}(\fs{ext}(B_{i+1})) = \fs{dom}(\fs{ext}(B_i)) \text{ for all } 1 \leq i < n \} \\
A((\fs{tm},n)) & = \{ (\overline{B}, h) : A((\fs{ty},n)) \times \fs{hom} \mid \fs{ext}(B_{n+1}) \circ h = \fs{id}(\fs{cod}(\fs{ext}(B_{n+1}))) \}
\end{align*}

Now, for every type theory $T$, we define a partial Horn theory $A(T)$.
It has function symbols and axioms of $\fs{CwA}$.
Also, for every basic function symbol $\sigma : s_1 \times \ldots s_k \to s$ of $T$, we add function symbol $\sigma : \fs{ob} \times A(s_1) \times \ldots \times A(s_k) \to A(s)$ to $A(T)$.
We also add the following axiom:
\[ \sigma(\Gamma, x_1, \ldots x_k)\!\downarrow\ \sststile{}{x_1, \ldots x_k} \fs{cod}(\fs{ext}(\sigma^1(\Gamma, x_1, \ldots x_k))) = \Gamma \land \bigwedge_{1 \leq i \leq k} \fs{cod}(\fs{ext}(x_i^1)) = \Gamma \]
For every predicate symbol of $T$, we add a predicate symbol and an axiom to $A(T)$ in a similar way.
Finally, we need to transfer axioms of $T$ to $A(T)$.
To do this, we need to define a restricted term (resp., a formula) $A(S)$ in $A(T)$ for every function (resp., predicate) symbol $S$ of $T$.
This function can be extended to a function on terms and formulas.
Then we will add an axiom $A(\varphi) \sststile{}{\overline{x}} A(\psi)$ to $A(T)$ for every axiom $\varphi \sststile{}{\overline{x}} \psi$ of $T$.

If $S = \sigma_m$ for some basic function symbol $\sigma : (p_1,n_1) \times \ldots \times (p_k,n_k) \to (p,n)$, then we define $A(\sigma_m)(\Gamma, x_1, \ldots x_k)$ as follows:
\[ (\Gamma, \sigma(\fs{dom}(\fs{ext}(\Gamma^m)), x_1^{m+1, \ldots |x_1|}, \ldots x_k^{m+1, \ldots |x_k|})|_{\bigwedge_{1 \leq i \leq k} x_i^{1, \ldots m} = \Gamma}), \]
where $x_i^{j_1, \ldots j_l} = (x_i^{j_1}, \ldots x_i^{j_l})$.
For predicate symbols, $A(S)$ is defined similarly.
For function symbols from the theory of substitution, $A(S)$ is defined in the obvious way: $A(\fs{ft}_n)$ and $A(\fs{ty}_n)$ are obvious projections,
$A(\fs{subst}_{p,n,k})$ is defined in terms of the pullback operation from the theory $\fs{CwA}$, and $A(v_{n,i})$ is defined by the universal property of pullbacks.

Let $A^s(T)$ be the split version of $A(T)$.
That is, $A^s(T)$ is just $A(T)$ together with axioms asserting that the underlying category with attributes is split.
Then there is a generalized morphism of theories $a : T \to A^s(T)$, which maps sorts $s$ to $A(s)$ and function and predicate symbols $S$ to $A(S)$.
It induces an adjunction $a_! \dashv a^*$ between $\Mod{T}$ and $\Mod{A^s(T)}$.
It is easy to describe the left adjoint $a_! : \Mod{T} \to \Mod{A^s(T)}$ explicitly.
Objects of $a_!(M)$ are contexts of $M$ and maps are morphisms of contexts.
Types are non-empty contexts and the pullback of a type $B$ along a morphism $f$ is defined as $B[f]$.

\begin{prop}[cwa-coref]
The adjunction $a_! \dashv a^*$ makes $\Mod{T}$ into a coreflective subcategory of $\Mod{A^s(T)}$.
\end{prop}
\begin{proof}
We need to prove that the unit of the adjunction $a_! \dashv a^*$ is an isomorphism.
This is a standard fact for the theory of substitutions.
In general, we just need to show that the isomorphism $M \to a^*(a_!(M))$ preserves the additional structure.
This can be verified in a strightforward way.
\end{proof}

There is a close relationship between semi-model structures on $\Mod{A^s(T)}$ and $\Mod{T}$:

\begin{prop}[coref-model]
Let $\C$ be a coreflective subcategory of $\D$, let $a_! : \C \to \D$ be the inclusion functor, and let $a^* : \D \to \C$ be the coreflector.
Suppose that $\C$ and $\D$ are locally presentable.
Then the following properties hold:
\begin{enumerate}
\item \label{it:coref-model-right}
Suppose that there is a combinatorial semi-model structure on $\C$.
Then there is a combinatorial right transferred semi-model structure on $\D$.
\item \label{it:coref-model-left}
Suppose that there is a combinatorial model structure (resp., semi-model structure) on $\D$ with $a_!(\I)$ as a set of generating cofibrations for some set $\I$ of maps of $\C$.
Then there is a combinatorial left transferred model structure (resp., semi-model structure) on $\C$.
\end{enumerate}
The adjunction $a_! \dashv a^*$ is a Quillen equivalence in both of these cases.
\end{prop}
\begin{proof}
It is easy to prove \eqref{it:coref-model-right}.
If $\J$ is a set of generating cofibrations of $\C$, then we just need to show that maps with cofibrant domains in $a^*(\Icell[a_!(\J)])$ are weak equivalences.
Since $a_!$ is fully faithful, cofibrant objects of $\D$ are precisely objects of the form $a_!(X)$ for cofibrant objects $X$.
Thus, colimits that appear in the construction of maps (with cofibrant domains) in $\Icell[a_!(\J)]$ can be computed in $\C$.
Hence, they are trivial cofibration.
Since $a^*$ preserves and reflects weak equivalences and the unit of the adjunction $a_! \dashv a^*$ is an isomorphism, this adjunction is a Quillen equivalence.

To prove \eqref{it:coref-model-left}, we can apply Smith's theorem.
Then we just need to show that if a map $f$ has RLP with respect to $\I$, then $a_!(f)$ has RLP with respect to $a_!(\I)$.
This follows from the fact that $a_!$ is fully faithful.
The adjunction $a_! \dashv a^*$ is a Quillen pair by definition.
Since $a_!$ preserves and reflects weak equivalences, we just need to show that the counit $\varepsilon_X$ of the adjunction is a weak equivalence.
Since $\eta_{a^*(X)}$ is an isomorphism, $a^*(\varepsilon_X)$ is also an isomorphism.
In particular, it is a trivial fibration.
It follows that $\varepsilon_X$ is also a trivial fibration.
\end{proof}

A \emph{category with fibrations} is a category with attributes such that, for every morphism $f$, there is at most one type $B$ such that $\fs{ext}(B) = f$.
Let $F(T)$ be the theory $A(T)$ together with the axiom asserting that this condition holds.
Similarly, we can define the theory $F^s(T)$ of split category with fibrations as $A^s(T)$ together with this axiom.

\begin{prop}
If there is a combinatorial semi-model structure on $\Mod{A(T)}$ (resp., $\Mod{A^s(T)}$) with $\I_0$ as a set of generating cofibrations,
then there is a Quillen equivalent right induced combinatorial semi-model structure on $\Mod{F(T)}$ (resp., $\Mod{F^s(T)}$).
\end{prop}
\begin{proof}
We will prove this for $A(T)$; the proof for $A^s(T)$ is the same.
Let $f : A(T) \to F(T)$ be the obvious inclusion and let $\J$ be a set of generating trivial cofibrations of $\Mod{A(T)}$.
We need to show that every map $j \in \Icell[f_!(\J)]$ with a cofibrant domain is a weak equivalences.
By \rlem{cofibrant-fib}, all colimits that appear the construction of $j$ can be computed in $\Mod{A}(T)$.
Thus, $j$ is a weak equivalence.
Since every cofibrant category with attributes is a category with fibrations, the unit of the adjunction is an isomorphism for cofibrant categories with attributes.
Thus, the adjunction is a Quillen equivalence.
\end{proof}

\begin{lem}[cofibrant-fib]
Cofibrant objects in $\Mod{A(T)}$ (resp., $\Mod{A^s(T)}$) belong to $\Mod{F(T)}$ (resp., $\Mod{F^s(T)}$).
\end{lem}
\begin{proof}
Since every cofibrant object is an equalizer of cellular objects, it is enough to prove this lemma for cellular objects.
% TODO
\end{proof}

In \cite{morita-equiv}, we defined a set of generating cofibrations on the category of type theories.
Let us recall this definition.
Let $d_\fs{ty} = \fs{ctx}$, $d_\fs{tm} = \fs{ty}$, $e_\fs{ty}(a) = \fs{ft}(a)$, and $e_\fs{tm}(a) = \fs{ty}(a)$.
For every sequence $(p_1,n_1), \ldots (p_{k+1},n_{k+1})$ of sorts, let $T_{(p_1,n_1), \ldots (p_{k+1},n_{k+1})}$ be the theory
with function symbols $\sigma_i : (p_1,n_1) \times \ldots \times (p_{i-1},n_{i-1}) \to (d_{p_i},n_i)$ for every $1 \leq i \leq k$,
$\sigma_{k+1} : (p_1,n_1) \times \ldots \times (p_k,n_k) \to (p_{k+1},n_{k+1})$,
and axioms $\varphi_1 \land \ldots \land \varphi_i \sststile{}{x_1, \ldots x_i} \sigma_{i+1}(x_1, \ldots x_i)\!\downarrow$ for every $1 \leq i \leq k$,
where $\varphi_j$ equals to $e_{p_j}(x_j) = \sigma_j(x_1, \ldots x_{j-1})$.
Let $\I$ be the set of maps of the form $T_{l, (d_p,n)} \to T_{l, (p,n)}$, where $l = s_1, \ldots s_k$ is any sequence of sorts,
$\sigma_i$ maps to $\sigma_i$ for every $1 \leq i \leq k$, and $\sigma_{k+1}$ maps to $e_p(\sigma_{k+1})$.

\begin{defn}
We will say that a type theory is \emph{cellular} (resp., \emph{cofibrant}) if it belongs to $\Icell$ (resp., $\Icof$).
\end{defn}

Let $T$ be a cellular theory.
For every function symbol $\sigma$ of $T$, there is a formula $\varphi$ such that $\varphi \sststile{}{\overline{x}} \sigma(x_1, \ldots x_k)\!\downarrow$ is derivable in $T$.
In general, the sequent $\sigma(x_1, \ldots x_k)\!\downarrow\ \sststile{}{\overline{x}} \varphi$ is not derivable in $T$.
If we add this axiom to $T$, then we get a cofibrant theory $T'$.
Indeed, there is an obvious inclusion $T \to T'$.
A section $s : T' \to T$ can be defined as $s(\sigma) = \sigma|_\varphi$.
If a theory $T'$ is a retract of a theory $T$, then $\Mod{T'}$ is a coreflective subcategory of $\Mod{T}$.
Since cofibrant theories are retracts of cellular theories, \rprop{coref-model} implies that, for every cofibrant theory $T'$,
there exists a cellular theory $T$ such that a semi-model structure exists on $\Mod{T'}$ if and only if it exists on $\Mod{T}$ and these structures are Quillen equivalent.

We can define cofibrant analogs of standard type theories.
We will present them in the usual way using derivation rules.
Every such rule is translated to the axiom that the conclusion holds if and only if its premises do.
The cofibrant theory $T_\fs{Id}$ of identity types is defined as follows:
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash a : A$}
\AxiomC{$\Gamma \vdash a' : A$}
\BinaryInfC{$\Gamma \vdash \fs{Id}_A(a, a')$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash a : A$}
\UnaryInfC{$\Gamma \vdash \fs{refl}(a) : \fs{Id}_A(a, a)$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, y : A, z : \fs{Id}_A(a, y) \vdash D$}
\AxiomC{$\Gamma \vdash d : D[a/y, \fs{refl}(a)/z]$}
\AxiomC{$\Gamma \vdash p : \fs{Id}_A(a, a')$}
\TrinaryInfC{$\Gamma \vdash \fs{J}(y z.\,D, d, a, a', p) : D[a'/y, p/z]$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, y : A, z : \fs{Id}_A(a, y) \vdash D$}
\AxiomC{$\Gamma \vdash d : D[a/y, \fs{refl}(a)/z]$}
\AxiomC{$\Gamma \vdash a : A$}
\TrinaryInfC{$\Gamma \vdash \fs{J}_\fs{eq}(y z.\,D, d, a) : \fs{Id}_{D[a/y, \fs{refl}(a)/z]}(\fs{J}(y z.\,D, d, a, a, \fs{refl}(a)), d)$}
\DisplayProof
\end{center}

The cofibrant theory of unit types $T_\top$ is the following extension of $T_\fs{Id}$:
\medskip
\begin{center}
\AxiomC{}
\UnaryInfC{$\Gamma \vdash () : \top$}
\DisplayProof
\quad
\AxiomC{$\Gamma, x : \top \vdash D$}
\AxiomC{$\Gamma \vdash d : D[()/x]$}
\AxiomC{$\Gamma \vdash u : \top$}
\TrinaryInfC{$\Gamma \vdash \top\text{-}\fs{elim}(x.D, d, u) : D[u/x]$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : \top \vdash D$}
\AxiomC{$\Gamma \vdash d : D[()/x]$}
\BinaryInfC{$\Gamma \vdash \top\text{-}\fs{elim}_\fs{eq}(x.D, d) : \Id_{D[()/x]}(\top\text{-}\fs{elim}(x.D, d, ()), d)$}
\DisplayProof
\end{center}

The cofibrant theory of $\Sigma$-types $T_\Sigma$ is defined in a similar way, we just replace the computational rule for the eliminator $\Sigma\text{-}\fs{elim}$ with a propositional equality $\Sigma\text{-}\fs{elim}_\fs{eq}$.
Let $T_{\fs{Id} + \top + \Sigma}$ be the pushout $T_\top \amalg_{T_\fs{Id}} T_\Sigma$.

Let $T$ be a theory under $T_{\fs{Id} + \top + \Sigma}$.
Then we will say that a map $f : X \to Y$ in $\Mod{T}$ is a \emph{weak equivalence} if the following conditions hold:
\begin{enumerate}
\item \label{it:we-type} For every context $\Gamma$ in $X$ and every type $f(\Gamma) \vdash A$, there exists a type $\Gamma \vdash A'$ and an equivalence $f(\Gamma) \vdash H : f(A') \simeq A$.
\item \label{it:we-term} For every type $\Gamma \vdash A$ in $X$ and every term $f(\Gamma) \vdash a : f(A)$, there exists a term $\Gamma \vdash a' : A$ and a homotopy $f(\Gamma) \vdash h : \fs{Id}_{f(A)}(f(a'),a)$.
\end{enumerate}

We will say that a map $f$ in $\Mod{A^s(T)}$ is a \emph{weak equivalence} if $a^*(f)$ is a weak equivalence.
That is, $f$ is a weak equivalence if conditions \eqref{it:we-type} and \eqref{it:we-term} hold for every context of the form $1.A_1 \ldots A_n$, but not necessarily for all contexts.
Similarly, we will say that a map in $\Mod{A(T)}$ is a \emph{weak equivalence} if these conditions hold for all contexts of this form.
Finally, a map in $\Mod{F(T)}$ (resp., $\Mod{F^s(T)}$) is a \emph{weak equivalence} when it is a weak equivalence when considered as a map in $\Mod{A(T)}$ (resp., $\Mod{A^s(T)}$).

\begin{remark}[std-we]
The definition of weak equivalences does not depend on the choice of identity types.
Moreover, all the definitions of weak equivalences in various categories agree with each other.
That is, obvious right adjoints between them preserve and reflect weak equivalences.
\end{remark}

Weak equivalences can be characterized in terms of homotopy categories.
Objects of the \emph{homotopy category} of a model $X$ of $T$ are closed types of $X$ and maps between $A$ and $B$ are equivalence classes of terms $x : A \vdash b : B$,
where $b$ and $b'$ are equivalent if there is a homotopy $x : A \vdash h : \fs{Id}(b,b')$.
We can also take a larger category which contains all contexts of $X$, but it is equivalent to the category we described since $T$ has $\Sigma$-types and unit types.
The homotopy category of a model of $A(T)$ is defined similarly.
The construction of the homotopy category is functorial, that is we have functors $\fs{Ho} : \Mod{T} \to \bcat{Cat}$ and $\fs{Ho} : \Mod{A(T)} \to \bcat{Cat}$.

\begin{prop}
A map $f$ in $\Mod{T}$ is a weak equivalence if and only if $\fs{Ho}(f)$ is isomorphism.
The same proposition holds for maps in $\Mod{A(T)}$.
\end{prop}
\begin{proof}
This was proved in \cite[Proposition~3.11]{alg-models} and \cite[Proposition~3.3]{kap-lum-model}.
Both proofs assume stronger conditions on $T$, but it is easy to see that the proposition still holds in this generality.
\end{proof}

If $R$ is a set of relations in a partial Horn theory, we will denote by $F(R)$ its model generated by these relations.
For example, the model $F(\{ \Gamma \vdash A \})$ classifies types in an arbitrary context and the model $F(\{ \Gamma \vdash A \simeq A' \})$ classifies equivalences between arbitrary types in an arbitrary context.

\begin{defn}
Let $T$ be a theory under $T_{\fs{Id} + \top + \Sigma}$.
We will say that a (semi-)model structure on $\Mod{T}$ is \emph{standard} if $\I_0$ generates cofibrations, all objects are fibrant,
and the maps $j_{(\fs{ty},n)} : F(\{ \Gamma \vdash A \}) \to F(\{ \Gamma \vdash A \simeq A' \})$ and $j_{(\fs{tm},n)} : F(\{ \Gamma \vdash a : A \}) \to F(\{ \Gamma \vdash h : \fs{Id}_A(a,a') \})$ are weak equivalences (where $n$ is the length of the context $\Gamma$).
The same terminology applies to (semi-)model structures on any category equipped with a right adjoint to either $\Mod{T_{\fs{Id} + \top + \Sigma}}$ or $\Mod{A(T_{\fs{Id} + \top + \Sigma})}$.
\end{defn}

\begin{prop}[std-indep]
The definition of standard (semi-)model structures depends only on the choice of a right adjoint functor to $\Mod{T_0}$ (that is, it does not depend on the choice of identity types, unit types, and $\Sigma$-types).
\end{prop}
\begin{proof}
We need to show that $F(\{ \Gamma \vdash p : \fs{Id}_A(a,a') \})$ and $F(\{ \Gamma \vdash p' : \fs{Id}'_A(a,a')\})$ are weakly equivalent for any pair of identity types $\fs{Id}$ and $\fs{Id}'$.
It is easy to construct maps $f$ and $g$ between them and show that $g(f(p))$ is homotopic to $p$.
That is, we have a map $H : F(\{ \Gamma \vdash h : \fs{Id}_{\fs{Id}_A(a,a')}(p,p') \}) \to F(\{ \Gamma \vdash p : \fs{Id}_A(a,a') \})$ such that $H(p) = p$ and $H(p') = g(f(p))$.
Since $F(\{ \Gamma \vdash h : \fs{Id}_{\fs{Id}_A(a,a')}(p,p') \})$ is a cylinder object for $F(\{ \Gamma \vdash p : \fs{Id}_A(a,a') \})$, it follows that $g \circ f$ is homotopic to $\fs{id}$.
Similarly, $f \circ g$ is homotopic to $\fs{id}$.
\end{proof}

Since all objects of standard semi-model structures are fibrant, their various properties follow from results in \cite{f-model-structures}.
This paper is formulated in terms of model categories, but with obvious adjustments its results apply to semi-model categories as well.

\begin{prop}
Weak equivalences in the standard semi-model structures are precisely the ones we defined above.
\end{prop}
\begin{proof}
This follows from \cite[Proposition~3.5]{f-model-structures}.
\end{proof}

\begin{prop}[std-char]
The standard model structure exists if and only if pushouts of the map $j_s$ are weak equivalences for every sort $s$.
The standard semi-model structure exists if and only if pushouts of these maps with cofibrant domains are weak equivalences.
\end{prop}
\begin{proof}
This follows from \cite[Theorem~4.3]{f-model-structures}.
\end{proof}

The following proposition shows that obvious adjoint functors between standard semi-model categories are Quillen pairs:

\begin{prop}
Adjoint functors between standard semi-model structures which commute with forgetful functors to $\Mod{T_0}$ are Quillen adjunctions.
\end{prop}
\begin{proof}
Such left adjoints preserve cofibrations by the definition of generating cofibrations.
They preserve generating trivial cofibrations $j_s$ by \rprop{std-indep}.
\end{proof}

\begin{prop}
Let $g_! : \mathcal{C} \leftrightarrow \mathcal{D} : g^*$ be an adjunction between categories over $\Mod{T_0}$.
Suppose that there is a right adjoint functor $\mathcal{C} \to \Mod{T_{\fs{Id} + \top + \Sigma}}$ and the standard semi-model structure exists on $\mathcal{D}$.
Then the following conditions are equivalent:
\begin{enumerate}
\item The unit of the adjunction $g_! \dashv g^*$ is a weak equivalence for cofibrant objects.
\item The standard semi-model structure exists on $\mathcal{C}$ and the adjunction $g_! \dashv g^*$ is a Quillen equivalence.
\end{enumerate}
\end{prop}
\begin{proof}
Clearly, the second condition implies the first one.
Let us prove the converse.
Let $f$ be a pushout of $j_s$ with a cofibrant domain.
Then $g_!(f)$ is a weak equivalence since it is a pushout of a trivial cofibration.
Thus, $g^*(g_!(f))$ is a weak equivalence.
Finally, $f$ is a weak equivalence by 2-out-of-3 since the unit of the adjunction $g_! \dashv g^*$ is a weak equivalence for cofibrant objects and the domain and the codomain of $f$ are cofibrant.
The adjunction is a Quillen equivalence since the unit is a weak equivalence and $g^*$ reflects weak equivalences by \rremark{std-we}.
\end{proof}

% TODO: Construct semi-model structures on A(T)-Mod.

Let $sF(T)$ be the pushout of theories $F(T) \amalg_{\fs{Cat}} \fs{\fs{sCat}}$, where $\fs{Cat}$ is the theories of categories and $\fs{sCat}$ is the theory of simplicial categories.
Thus, a model of $sF(T)$ is just a model $X$ of $F(T)$ with the structure of simplicial category on the underlying category of $X$.

% TODO: Construct a model sturcture on sF(T)-Mod and prove that it is equivalent to F(T)-Mod.

\section{Finite limits in categories with fibrations}

Let $\C$ be a simplicial category.
An object $1$ of $\C$ is \emph{terminal} if the simplicial set $\Hom(c,1)$ is contractible for every object of $\C$.
If $1$ is a terminal object of $\C$, then it is also a terminal objects of $N(\C)$.
A \emph{product} of objects $a$ and $b$ of $\C$ is an object $a \times b$ together with maps $\pi_1 : \Hom(a \times b, a)$ and $\pi_2 : \Hom(a \times b, b)$ such that the following map is an equivalence for every object $c$:
\[ \Hom(c, a \times b) \to \Hom(c,a) \times \Hom(c,b) \]
If $a \times b$ is a product of $a$ and $b$, then it is a product of these objects in $N(\C)$.
Now, \rprop{over-cat} implies that a pullback of two basic fibrations in $\C$ is a pullback in $N(\C)$.

\bibliographystyle{amsplain}
\bibliography{ref}

\end{document}