alg-models-mscs.tex

\documentclass{mscs}

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

\hypersetup{colorlinks=true,linkcolor=blue,citecolor=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{\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}
\newref{defn}{Definition}{Definition}
\newref{example}{Example}{Example}
\newref{rem}{Remark}{Remark}

\newcommand{\deq}{\equiv}
\newcommand{\repl}{:=}
\newcommand{\IdT}{\mathrm{Id}}
\newcommand{\wUA}{\mathrm{wUA}}
\newcommand{\UA}{\mathrm{UA}}
\newcommand{\coeT}{\mathrm{coe}}
\newcommand{\PathT}{\mathrm{Path}}
\newcommand{\HPath}{\mathrm{HPath}}
\newcommand{\sqT}{\mathrm{sq}}
\newcommand{\dcT}{\mathrm{dc}}
\newcommand{\FillT}{\mathrm{Fill}}
\newcommand{\Eq}{\mathrm{Eq}}
\newcommand{\UEq}{\mathrm{UEq}}
\newcommand{\id}{\mathrm{id}}
\newcommand{\Lang}{\mathrm{Lang}}
\newcommand{\Ho}{\mathrm{Ho}}

\newcommand{\subst}{\mathit{subst}}
\newcommand{\wk}{\mathit{wk}}
\newcommand{\Id}{\mathit{Id}}
\newcommand{\refl}{\mathit{refl}}
\newcommand{\Jeq}{\mathit{Jeq}}
\newcommand{\leftI}{\mathit{left}}
\newcommand{\rightI}{\mathit{right}}
\newcommand{\coe}{\mathit{coe}}
\newcommand{\sq}{\mathit{sq}}
\newcommand{\dc}{\mathit{dc}}
\newcommand{\idtype}{\rightsquigarrow}
\newcommand{\Path}{\mathit{Path}}
\newcommand{\pathI}{\mathit{path}}
\newcommand{\at}{\mathit{at}}
\newcommand{\Ic}{\mathit{Ic}}
\newcommand{\Fill}{\mathit{Fill}}
\newcommand{\Square}{\mathit{Square}}
\newcommand{\sym}{\mathit{sym}}
\newcommand{\iso}{\mathit{iso}}
\newcommand{\inv}{\mathit{inv}}
\newcommand{\pair}{\mathit{pair}}

\newcommand{\cat}[1]{\mathbf{#1}}
\newcommand{\C}{\cat{C}}
\newcommand{\Mod}[1]{#1\text{-}\cat{Mod}}
\newcommand{\Th}{\cat{Th}}
\newcommand{\emptyCtx}{*}
\newcommand{\substTh}{\mathbb{S}}
\newcommand{\type}{\mathrm{type}}

\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{\Jcell}[1][]{\Icell[\J#1]}
\newcommand{\cyli}{\upgamma}

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

\title{Model Structures on Categories of Models of Type Theories}

\author{Valery Isaev}

\begin{document}

\maketitle

\begin{abstract}
Models of dependent type theories are contextual categories with some additional structure.
We prove that if a theory $T$ has enough structure, then the category $\Mod{T}$ of its models carries the structure of a model category.
We also show that if $T$ has $\Sigma$-types, then weak equivalences can be characterized in terms of homotopy categories of models.
\end{abstract}

\section{Introduction}

It is well-known that algebraic models (such as categories with attributes \cite{pitts}, categories with families \cite{cwf} and contextual categories \cite{GAT})
of dependent type theories are related to categories with additional structure.
For example, it was prove in \cite{ext-eq} that models of the type theory with extensional $\IdT$- and $\Sigma$-types are equivalent (in a weak bicategorical sense)
to finitely complete categories, and if we assume $\Pi$-types, then we obtain an equivalence with locally Cartesian closed categories.

Ideas of homotopy type theory suggest that models of dependent type theories with intentional $\IdT$-types should be related to $\infty$-categories.
There are several results (for example, \cite{shul-inv}, \cite{local-universes}, \cite{kapulkin}) that support this intuition,
but to make this relationship precise we need an appropriate definition of equivalences of models of type theories.

The main contribution of this paper is the construction of a model structure on categories of models of dependent type theories.
We will to this for any dependent type theory (with enough structure) that can be described as an essentially algebraic theory.
The formal definition of such theories is given in section~\ref{sec:alg-th}.
Now, we can state a formal conjecture about the relationship between models of type theories and $\infty$-categories.
Let $T_\Sigma$ be the theory with path types and $\Sigma$-types (see subsection~\ref{sec:sigma} for a precise definition).
\begin{conj}[main]
The $(\infty,1)$-category presented by model category $\Mod{T_\Sigma}$ is equivalent to the $(\infty,1)$-category of finitely complete $(\infty,1)$-categories.
\end{conj}
Analogous conjectures can be stated for other theories such as the theory with path types, $\Sigma$-types and $\Pi$-types.

It was shown in \cite{szumilo} that the fibration category of fibration categories is equivalent to the fibration category of finitely complete quasicategories.
Thus it is natural to study the relationship between fibration categories and models of $T_\Sigma$.
For every model $X$ of $T_\Sigma$, we can define a fibration category $U(X)$ (see \cite{tt-fibr-cat}), and this correspondence defines a functor $U : \Mod{T_\Sigma} \to \cat{FibCat}$
from the category of models of $T_\Sigma$ to the category of fibration categories.
Since both $\Mod{T_\Sigma}$ and $\cat{FibCat}$ are fibration categories, it is natural to conjecture that $U$ is exact, but it seems that it is not.
The main problem is that it seems that $U$ does not preserve fibrations.
Nevertheless, we can show that $U$ preserves and reflects weak equivalences (see \rprop{sigma-we-ho}), which indicates that $\Mod{T}$ has the correct class of weak equivalences.

We will describe a theory with the interval type and define a model structure on the category of models of theories that have the interval type.
We can define usual $\IdT$-types in this theory, but it is stronger than the theory of $\IdT$-types.
For example, function extensionality holds in this theory.
It might be possible to define a model structure on the category of models of theories with $\IdT$-types,
but it is more difficult, and we do not know how to do it.
Independently, Kapulkin and Lumsdaine constructed a semi-model structure on such category in \cite{kap-lum-model}.

The paper is organized as follows.
In section~\ref{sec:alg-th}, we briefly discuss the formalism of essentially algebraic theories, which we use to give a general definition of a dependent type theory.
In section~\ref{sec:HoTT-I}, we define different theories with the interval type and describe several constructions in these theories.
We also define a weak univalence axiom and prove that it implies a part of the usual version of this axiom.
In section~\ref{sec:model-structure}, we define a model structure on the category of models of a dependent type theory
and prove a characterization of weak equivalences in this category.

\section{Essentially algebraic theories}
\label{sec:alg-th}

We will construct model structures on categories of models of different dependent type theories.
A model of a dependent type theory is a contextual category with some additional structure, which depends on the theory.
Our construction of model structure is general, so it applies to any category of such models if the additional structure is algebraic enough.
To make this precise, we need to recall the notion of essentially algebraic theories.
There are several (equivalent) definitions of essentially algebraic theories in the literature.
We will use the one described in \cite{PHL} since the usual syntax of dependent type theories is very close to the syntax described in this paper.

Let us recall the basic definitions from \cite{PHL}.
A many sorted first-order signature $(\mathcal{S},\mathcal{F},\mathcal{P})$ consists of a set $\mathcal{S}$ of sorts,
a set $\mathcal{F}$ of function symbols and a set $\mathcal{P}$ of predicate symbols.
Each function symbol $\sigma$ is equipped with a signature of the form $\sigma : s_1 \times \ldots \times s_k \to s$, where $s_1$, \ldots $s_k$, $s$ are sorts.
Each predicate symbol $R$ is equipped with a signature of the form $R : s_1 \times \ldots \times s_k$.

An atomic formula is an expression either of the form $t_1 = t_2$ or of the form $R(t_1, \ldots t_n)$,
where $R$ is a predicate symbol and $t_1$, \ldots $t_n$ are terms.
We abbreviate $t = t$ to $t\!\downarrow$.
A Horn formula is an expression of the form $\varphi_1 \land \ldots \land \varphi_n$, where $\varphi_1$, \ldots $\varphi_n$ are atomic formulas.
A sequent is an expression of the form $\varphi \sststile{}{x_1, \ldots x_n} \psi$, where $x_1$, \ldots $x_n$ are variables
and $\varphi$ and $\psi$ are Horn formulas such that $FV(\varphi) \cup FV(\psi) \subseteq \{ x_1, \ldots x_n \}$.

A \emph{partial Horn theory} consists of a signature and a set of Horn sequents in this signature.
The rules of \emph{partial Horn logic} are listed below.
A \emph{theorem} of a partial Horn theory $T$ is a sequent derivable from $T$ in this logic.
\begin{center}
$\varphi \sststile{}{V} \varphi$ \axlabel{b1}
\qquad
\AxiomC{$\varphi \sststile{}{V} \psi$}
\AxiomC{$\psi \sststile{}{V} \chi$}
\RightLabel{\axlabel{b2}}
\BinaryInfC{$\varphi \sststile{}{V} \chi$}
\DisplayProof
\qquad
$\varphi \sststile{}{V} \top$ \axlabel{b3}
\end{center}

\medskip
\begin{center}
$\varphi \land \psi \sststile{}{V} \varphi$ \axlabel{b4}
\qquad
$\varphi \land \psi \sststile{}{V} \psi$ \axlabel{b5}
\qquad
\AxiomC{$\varphi \sststile{}{V} \psi$}
\AxiomC{$\varphi \sststile{}{V} \chi$}
\RightLabel{\axlabel{b6}}
\BinaryInfC{$\varphi \sststile{}{V} \psi \land \chi$}
\DisplayProof
\end{center}

\medskip
\begin{center}
$\sststile{}{x} x\!\downarrow$ \axlabel{a1}
\qquad
$x = y \land \varphi \sststile{}{V,x,y} \varphi[y/x]$ \axlabel{a2}
\end{center}

\medskip
\begin{center}
\AxiomC{$\varphi \sststile{}{V} \psi$}
\RightLabel{, $x \in FV(\varphi)$ \axlabel{a3}}
\UnaryInfC{$\varphi[t/x] \sststile{}{V,V'} \psi[t/x]$}
\DisplayProof
\end{center}
\medskip

An $\mathcal{S}$-set $M$ is a collection of sets $\{ M_s \}_{s \in \mathcal{S}}$.
An interpretation $M$ of a signature $(\mathcal{S},\mathcal{F},\mathcal{P})$ is an $\mathcal{S}$-set $M$
together with a collection of \emph{partial} functions $M(\sigma) : M_{s_1} \times \ldots \times M_{s_k} \to M_s$
for every function symbol $\sigma : s_1 \times \ldots \times s_k \to s$ of $T$
and relations $M(R) \subseteq M_{s_1} \times \ldots \times M_{s_k}$ for every predicate symbol $R : s_1 \times \ldots \times s_k$.
A model of a partial Horn theory $T$ is an interpretation of the underlying signature such that the axioms of $T$ hold in this interpretation.

We will consider theories with the set of sorts $\mathcal{S} = \{ ctx, tm \} \times \mathbb{N}$.
We will write $(ty,n)$ for $(ctx,n+1)$.
The idea is that terms of sort $(ctx,n)$ represent contexts of length $n$,
terms of sort $(ty,n)$ represent types in a context of length $n$,
and terms of sort $(tm,n)$ represent terms in a context of length $n$.
Note that we use the word ``term'' in two different meanings here.
A term of a sort $s$ is a term of our partial Horn theory.
If $M$ is a model of a partial Horn theory, then elements of $M_{(tm,n)}$ are also called terms.
Since we use partial Horn theories to discuss dependent type theories and their properties, the former kind of terms could be called \emph{metaterms},
but it is usually clear from the context in which sense the word ``term'' is used.

An important example of a partial Horn theory is the theory $\substTh$ which consists of the following symbols:
\begin{align*}
\emptyCtx     & : (ctx,0) \\
ft_n          & : (ty,n) \to (ctx,n) \\
ty_n          & : (tm,n) \to (ty,n) \\
v_{n,i}       & : (ctx,n) \to (tm,n) \text{, } 0 \leq i < n \\
\subst_{p,n,k} & : (ctx,n) \times (p,k) \times (tm,n)^k \to (p,n) \text{, } p \in \{ tm, ty \}
\end{align*}
We often omit subscripts in these function symbols.

Let $ctx^i_{p,n} : (p,n+i) \to (ctx,n)$ be the following derived operations:
\begin{align*}
ctx^0_{ty,n}(t) & = ft_n(t) \\
ctx^0_{tm,n}(t) & = ft_n(ty_n(t)) \\
ctx^{i+1}_{p,n}(t) & = ft_n(ctx^i_{p,n+1}(t))
\end{align*}

Axioms of $\substTh$ are defined in \cite{alg-tt}.
This theory is analogous to the theory of B-systems defined in \cite{b-systems},
and the category of models of this theory is equivalent to the category of contextual categories.

We think of $v_{n,i}$ as De Bruijn indices.
We will use a (slightly informal) named representation of terms,
from which a formal presentation in terms of De Bruijn indices can be recovered.
We write $x_1 : A_1, \ldots x_n : A_n \vdash A_{n+1}\ \type$ for the formula $\bigwedge_{1 \leq i \leq n} ft_i(A_{i+1}) = A_i$.
We write $x_1 : A_1, \ldots x_n : A_n \vdash a : A_{n+1}$ for the formula $ty_n(a) = A_{n+1} \land \bigwedge_{1 \leq i \leq n} ft(A_{i+1}) = A_i$.
Also, if $X : (p,n+k)$, $p \in \{ ty, tm \}$, $\Gamma, x_1 : A_1, \ldots x_n : A_n \vdash X$, and $a_1, \ldots a_k : (tm,n)$,
then we write $X[x_1 \repl a_1, \ldots x_k \repl a_k]$ for
\[ \subst_{p,n,k}(ctx^k_{p,n}(X), X, v_{n,n-1}, \ldots v_{n,0}, a_1, \ldots a_k). \]
As usual, we left the weakening operations implicit.
Also, if we have a function symbol $\sigma : (p,n+k) \to (p',n)$, then we may write $\sigma(x_1 \ldots x_k.\,t)$ to indicate the names of additional variable in the context of $t$.
For example, $\sigma(x y.\,\tau(y,x), x y.\,\tau(x,x))$ translates to $\sigma(\tau(v_0,v_1), \tau(v_1,v_1))$.

If we have some construction in a type theory, then it is usually can be used in any context.
This means that if we have a function symbol $\sigma : (p_1,n_1) \times \ldots \times (p_k,n_k) \to (p,n)$,
then we should also have a function symbol (or a term) $\sigma_1 : (ty,0) \times (p_1,n_1+1) \times \ldots \times (p_k,n_k+1) \to (p,n+1)$,
where the first argument represents the first type in the context of $\sigma_1$.
We will assume that all function symbols in our theory (except for $\emptyCtx$) are of the form $\sigma_m : (ctx,m) \times (p_1,n_1+m) \times \ldots \times (p_k,n_k+m) \to (p,n+m)$.
Analogously, we assume that all predicate symbols are of the form $R_m : (ctx,m) \times (p_1,n_1+m) \times \ldots \times (p_k,n_k+m)$.
Note that the theory $\substTh$ is already in this form.
We usually omit the subscript in $\sigma_m$.
We also may omit the first argument of $\sigma_m$ in expression of the form $\sigma_m(\Gamma, t_1, \ldots t_k)$ since it coincides with the context in which this term is used.
That is, instead of $\sigma_m(\Gamma, t_1, \ldots t_k)$ we may write $\Gamma \vdash \sigma(t_1, \ldots t_k)$.

Let $c$ be a closed type (that is, a term of sort $(ty,0)$).
If $\varphi$ is a formula of a theory that have the form described above,
then let $\alpha(c,\varphi)$ be the formula in which subscripts in all function and predicate symbols are increased by one and contexts are extended with $c$.
We call this operation \emph{lifting}.
For example, if $\varphi$ equals to $\Gamma \vdash \sigma_n(\sigma_n(x,y),z) \deq \sigma_n(x,\sigma_n(y,z))$,
then its lifting equals to $c,\Gamma \vdash \sigma_{n+1}(\sigma_{n+1}(x,y),z) \deq \sigma_{n+1}(x,\sigma_{n+1}(y,z))$.
We will say that a theory $T$ is $c$-stable if the following sequents are derivable:
\begin{align*}
\sigma_{m+1}(\Gamma, x_1, \ldots x_k)\!\downarrow & \sststile{}{\Gamma, x_1, \ldots x_k} ft^m(\Gamma) = c \\
R_{m+1}(\Gamma, x_1, \ldots x_k) & \sststile{}{\Gamma, x_1, \ldots x_k} ft^m(\Gamma) = c \\
\alpha(c,\varphi) \land \bigwedge_{1 \leq i \leq k} ctx^{n_i}(x_i) = c & \sststile{}{x_1, \ldots x_k} \alpha(c,\psi)
\end{align*}
for every function symbol $\sigma_m$, every predicate symbol $R_m$, and every axiom $\varphi \sststile{}{x_1, \ldots x_k} \psi$.

We will give several examples of theories in the next section.
For every function symbol of a theory, we give its signature:
\[ \sigma : (p_1,n+n_1) \times \ldots \times (p_k,n+n_k) \to (p,n). \]
Note that we omit the subscript in $\sigma_n$ and the first parameter of $\sigma_n$.
Thus the real signature looks like this:
\[ \sigma_n : (ctx,n) \times (p_1,n+n_1) \times \ldots \times (p_k,n+n_k) \to (p,n). \]
For every function symbol we give an inference rule either of the form
\medskip
\begin{center}
\AxiomC{$\varphi_1 \ldots \varphi_n$}
\UnaryInfC{$\Gamma \vdash \sigma(x_1, \ldots x_k)\ \type$}
\DisplayProof
\end{center}
or of the form
\medskip
\begin{center}
\AxiomC{$\varphi_1 \ldots \varphi_n$}
\UnaryInfC{$\Gamma \vdash \sigma(x_1, \ldots x_k) : A$}
\DisplayProof
\end{center}
In both cases we add the following axioms to our theory:
\begin{align*}
\varphi_1 \land \ldots \land \varphi_n \sststile{}{x_1, \ldots x_k} \sigma(x_1, \ldots x_k)\!\downarrow \\
\sigma(x_1, \ldots x_k)\!\downarrow\ \sststile{}{x_1, \ldots x_k} \varphi_1 \land \ldots \land \varphi_n
\end{align*}
In the second case we also add the following axiom:
\[ \sigma(x_1, \ldots x_k)\!\downarrow\ \sststile{}{x_1, \ldots x_k} ty(\sigma(x_1, \ldots x_k)) = A \]
Finally, we may have several inference rules of the form
\medskip
\begin{center}
\AxiomC{$\varphi_1 \ldots \varphi_n$}
\UnaryInfC{$\Gamma \vdash t \deq t'$}
\DisplayProof
\end{center}
Each such inference rule correspond to the following axiom:
\[ \varphi_1 \land \ldots \land \varphi_n \sststile{}{V} \Gamma \vdash t_1 \deq t_2, \]
where $V$ is the set of variables that appear in the inference rule.

We assume that all function symbols of our theories are of the form $\sigma : (p_1,n_1+m) \times \ldots \times (p_k,n_k+m) \to (p,m)$.
We also assume that all theories have axioms asserting that all function symbols commute with $\subst_{p,n,k}$.
That is, for every function symbol $\sigma_0 : (p_1,n_1) \times \ldots \times (p_k,n_k) \to (p,0)$ and every predicate symbol $R_0 : (p_1,n_1) \times \ldots \times (p_k,n_k)$,
the following axioms are derivable:
\medskip
\begin{center}
\AxiomC{$A_1, \ldots A_n \vdash \sigma_n(b_1, \ldots b_k) \downarrow$}
\AxiomC{$\bigwedge_{1 \leq i \leq n} \Gamma \vdash a_i : \subst_{ty,m,i-1}(A_i, a_1, \ldots a_{i-1})$}
\BinaryInfC{$\Gamma \vdash \subst_{p,m,n}(\sigma_n(b_1, \ldots b_k), a_1, \ldots a_n) \deq \sigma_m(b_1', \ldots b_k')$}
\DisplayProof
\end{center}
\medskip

\begin{center}
\AxiomC{$A_1, \ldots A_n \vdash R_n(b_1, \ldots b_k)$}
\AxiomC{$\bigwedge_{1 \leq i \leq n} \Gamma \vdash a_i : \subst_{ty,m,i-1}(A_i, a_1, \ldots a_{i-1})$}
\BinaryInfC{$\Gamma \vdash R_m(b_1', \ldots b_k')$}
\DisplayProof
\end{center}
\medskip
where $b_i' = \subst_{p,m+n_i,n+n_i}(b_i, \wk^{n_i}_m(a_1), \ldots \wk^{n_i}_m(a_n), v_{n_i-1}, \ldots v_0)$,
where $\wk^{n_i}_m$ are the weakening operations defined as follows:
\[ \wk^{n_i}_m(a) = \subst_{tm,m+n_i,m}(a, v_{m+n_i-1}, \ldots v_{n_i}). \]

A \emph{restricted term} of a theory $\mathbb{T}$ is a term $t$ together with a formula $\varphi$.
We denote such a restricted term by $t|_\varphi$.
If we think of terms as representations for partial functions,
then we can think of a restricted term $t|_\varphi$ as a restriction of the partial function represented by $t$ to a subset of its domain.
Let us define the substitution function for restricted terms.
If $x \in FV(t|_\varphi)$ and $x \in FV(\psi)$, then it is defined as follows:
\begin{align*}
t|_\varphi[t'|_{\varphi'}/x] & = t[t'/x]|_{\varphi[t'/x] \land \varphi'} \\
\psi[t'|_{\varphi'}/x] & = \psi[t'/x] \land \varphi'
\end{align*}

An \emph{interpretation} of a theory $\mathbb{T}$ in a theory $\mathbb{T}'$ is a function $f$ such that the following conditions hold:
\begin{enumerate}
\item For every function symbol $\sigma : s_1 \times \ldots \times s_k \to s$ of $\mathbb{T}$,
the function $f$ defines a restricted term $f(\sigma)$ of $\mathbb{T}'$ of sort $s$ such that $FV(f(\sigma)) = \{ x_1 : s_1, \ldots x_k : s_k \}$.
\item For every predicate symbol $P : s_1 \times \ldots \times s_k$,
the function $f$ defines a formula $f(P)$ of $\mathbb{T}'$ such that $FV(f(P)) = \{ x_1 : s_1, \ldots x_k : s_k \}$.
\item For every axiom $\varphi \sststile{}{V} \psi$ of $\mathbb{T}$, the sequent $f(\varphi) \sststile{}{V} f(\psi)$ is derivable in $\mathbb{T}'$.
\end{enumerate}

\section{Theories with an interval type}
\label{sec:HoTT-I}

In this section we describe the theory of an interval type.
We describe several constructions in this theory which we will need later.
In particular, we will show that theories with an interval type and path types also have $\IdT$-types.

Theories with an interval type are closely related to theories with identity types.
So, let us first recall its definition from \cite{alg-tt}.
The theory $\IdT$ has the following function symbols:
\begin{align*}
\Id & : (tm,n) \times (tm,n) \to (ty,n) \\
\refl & : (tm,n) \to (tm,n) \\
J & : (ty,n+3) \times (tm,n+1) \times (tm,n) \times (tm,n) \times (tm,n) \to (tm,n)
\end{align*}
and the following axioms:
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash ty(a) \deq ty(a')$}
\UnaryInfC{$\Gamma \vdash \Id(a, a')\ \type$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash a : A$}
\UnaryInfC{$\Gamma \vdash \refl(a) : \Id(a, a)$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : A, y : A, z : \Id(x,y) \vdash D\ \type$}
\AxiomC{$\Gamma, x : A \vdash d : D'$}
\AxiomC{$\Gamma \vdash p : \Id(a,a')$}
\TrinaryInfC{$\Gamma \vdash J(D,d,a,a',p) : D[a,a',p]$}
\DisplayProof
\end{center}
where $D' = D[y \repl x, z \repl \refl(x)]$ and $A = ty(a)$.

\medskip
\begin{center}
\AxiomC{$\Gamma, x : ty(a), y : ty(a), z : \Id(x,y) \vdash D\ \type$}
\AxiomC{$\Gamma, x : ty(a) \vdash d : D'$}
\BinaryInfC{$\Gamma \vdash J(D,d,a,a,\refl(a)) \deq d[a]$}
\DisplayProof
\end{center}
\medskip
where $D' = D[y \repl x, z \repl \refl(x)]$.

We will also need slightly weaker version of $\IdT$ which we will denote by $\IdT_-$.
It has all of the function symbols of $\IdT$ together with the following one:
\[ \Jeq : (tm,n+3) \times (tm,n+1) \times (tm,n) \to (tm,n) \]
The theory $\IdT_-$ has all of the axioms of $\IdT$ except the last one; instead it has the following additional axiom:
\begin{center}
\AxiomC{$\Gamma, x : A, y : A, z : \Id(x,y) \vdash D\ \type$}
\AxiomC{$\Gamma, x : A \vdash d : D'$}
\AxiomC{$\Gamma \vdash a : A$}
\TrinaryInfC{$\Gamma \vdash \Jeq(D,d,a) : \Id(J(D,d,a,a,\refl(a)),d[a])$}
\DisplayProof
\end{center}
where $D' = D[y \repl x, z \repl \refl(x)]$.
The idea is that the last axiom of $\IdT$ holds in $\IdT_-$ only propositionally.

Now, we can define the theory of the interval type.
Actually, there are several different ways to define such theory.
These theories are not isomorphic, but should be equivalent in some weaker sense.
First, let us define the most basic theory which has only the interval type and its constructors, but lacks any kind of eliminator for it.
The theory $I$ has function symbols $I : (ty,n)$, $\leftI : (tm,n)$, $\rightI : (tm,n)$ and the following axioms:
\begin{center}
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash I\ \type$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \leftI : I$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \rightI : I$}
\DisplayProof
\end{center}

There are at least three different ways to define an eliminator for $I$.
The idea always the same: given a fibration over $I$ and a point in the fibre over
some point $i : I$, we can transport it to the fibre over some other point $j : I$.
In different eliminators, we can take different $i$ and $j$.
In $\coeT_0$, we can only take $i = \leftI$ and $j = \rightI$.

\medskip
\begin{center}
\AxiomC{$\Gamma, x : I \vdash D\ \type$}
\AxiomC{$\Gamma \vdash d : D[x \repl \leftI]$}
\BinaryInfC{$\Gamma \vdash \coe_0(D, d) : D[x \repl \rightI]$}
\DisplayProof
\end{center}

In $\coeT_1$, we can take $i = \leftI$ and arbitrary $j$.

\medskip
\begin{center}
\AxiomC{$\Gamma, x : I \vdash D\ \type$}
\AxiomC{$\Gamma \vdash d : D[x \repl \leftI]$}
\AxiomC{$\Gamma \vdash i : I$}
\TrinaryInfC{$\Gamma \vdash \coe_1(D, d, i) : D[x \repl i]$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : I \vdash D\ \type$}
\AxiomC{$\Gamma \vdash d : D[x \repl \leftI]$}
\BinaryInfC{$\Gamma \vdash \coe_1(D, d, \leftI) \deq d$}
\DisplayProof
\end{center}

In $\coeT_2$, both $i$ and $j$ may be arbitrary.

\medskip
\begin{center}
\AxiomC{$\Gamma, x : I \vdash D\ \type$}
\AxiomC{$\Gamma \vdash i : I$}
\AxiomC{$\Gamma \vdash d : D[x \repl i]$}
\AxiomC{$\Gamma \vdash j : I$}
\QuaternaryInfC{$\Gamma \vdash \coe_2(D, i, d, j) : D[x \repl j]$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : I \vdash D\ \type$}
\AxiomC{$\Gamma \vdash d : D[x \repl \leftI]$}
\BinaryInfC{$\Gamma \vdash \coe_2(D, \leftI, d, \leftI) \deq d$}
\DisplayProof
\end{center}

It turns out that $\coeT_0$ is too weak.
To make it equivalent to other two theories, we need to add the theory $\sqT$ to it,
which has one function symbol $\sq : (tm,n) \times (tm,n) \to (tm,n)$ and the following axioms:
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash i : I$}
\AxiomC{$\Gamma \vdash j : I$}
\BinaryInfC{$\Gamma \vdash \sq(i,j) : I$}
\DisplayProof
\qquad
\AxiomC{$\Gamma \vdash i : I$}
\UnaryInfC{$\Gamma \vdash \sq(i,\leftI) \deq \leftI$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash j : I$}
\UnaryInfC{$\Gamma \vdash \sq(\leftI,j) \deq \leftI$}
\DisplayProof
\qquad
\AxiomC{$\Gamma \vdash j : I$}
\UnaryInfC{$\Gamma \vdash \sq(\rightI,j) \deq j$}
\DisplayProof
\end{center}

Also, these theories correspond to $\IdT_-$.
To get theories that correspond to $\IdT$, we need to add one additional rule to each of them:
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash a : A$}
\UnaryInfC{$\Gamma \vdash \coe_0(A, a) \deq a$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash a : A$}
\UnaryInfC{$\Gamma \vdash \coe_1(A, a, \rightI) \deq a$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash a : A$}
\UnaryInfC{$\Gamma \vdash \coe_2(A, \leftI, a, \rightI) \deq a$}
\DisplayProof
\end{center}
\smallskip
We denote these theories by $\coeT_0 + \sigma$, $\coeT_1 + \sigma$ and $\coeT_2 + \sigma$.

We will also consider additional axioms $\beta_1$ and $\beta_2$ for $\coeT_2$.
The axiom $\beta_1$ is defined as follows:
\medskip
\begin{center}
\AxiomC{$\Gamma, x : I \vdash D\ \type$}
\AxiomC{$\Gamma \vdash d : D[x \repl \leftI]$}
\BinaryInfC{$\Gamma \vdash \coe_2(D, \rightI, d, \rightI) \deq d$}
\DisplayProof
\end{center}
\medskip
The axiom $\beta_2$ is defined as follows:
\medskip
\begin{center}
\AxiomC{$\Gamma, x : I \vdash D\ \type$}
\AxiomC{$\Gamma \vdash d : D[x \repl \leftI]$}
\AxiomC{$\Gamma \vdash i : I$}
\TrinaryInfC{$\Gamma \vdash \coe_2(D, i, d, i) \deq d$}
\DisplayProof
\end{center}
Obviously, we have maps from $\coeT_2$ to $\coeT_2 + \beta_1$ and from $\coeT_2 + \beta_1$ to $\coeT_2 + \beta_2$.

The theory $\coeT_2 + \beta_2$ is slightly stronger than other theories.
To make them equivalent to $\coeT_2 + \beta_2$, we need to assume additional operations.
For example, we can consider the theory $\dcT$, which has one function symbol
$\dc : (tm,n) \times (tm,n) \times (tm,n) \to (tm,n)$ and the following axioms:
\medskip
\begin{center}
\AxiomC{$\Gamma \vdash i : I$}
\AxiomC{$\Gamma \vdash j : I$}
\AxiomC{$\Gamma \vdash k : I$}
\TrinaryInfC{$\Gamma \vdash \dc(i,j,k) : I$}
\DisplayProof
\qquad
\AxiomC{$\Gamma \vdash i : I$}
\AxiomC{$\Gamma \vdash j : I$}
\BinaryInfC{$\Gamma \vdash \dc(i,j,\leftI) \deq i$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash i : I$}
\AxiomC{$\Gamma \vdash j : I$}
\BinaryInfC{$\Gamma \vdash \dc(i,j,\rightI) \deq j$}
\DisplayProof
\qquad
\AxiomC{$\Gamma \vdash i : I$}
\AxiomC{$\Gamma \vdash k : I$}
\BinaryInfC{$\Gamma \vdash \dc(i,i,k) \deq i$}
\DisplayProof
\end{center}

\subsection{Homogeneous path types}

To define maps between theories with $\IdT$-types and theories with an interval type,
we need to add an additional construction to the latter, which we call \emph{homogeneous path types}.
Let $\HPath$ be the theory with function symbols $\idtype\ : (tm,n) \times (tm,n) \to (ty,n)$,
$\pathI : (ty,n) \times (tm,n+1) \to (tm,n)$, and $\at : (tm,n) \times (tm,n) \times (tm,n) \times (tm,n) \to (tm,n)$ and the following axioms:
\begin{center}
\AxiomC{$\Gamma \vdash a : A$}
\AxiomC{$\Gamma \vdash a' : A$}
\BinaryInfC{$\Gamma \vdash a \idtype a'\ \type$}
\DisplayProof
\end{center}

\smallskip
\begin{center}
\AxiomC{$\Gamma \vdash A\ \type$}
\AxiomC{$\Gamma, x : I \vdash a : A$}
\BinaryInfC{$\Gamma \vdash \pathI(A, a) : a[x \repl \leftI] \idtype a[x \repl \rightI]$}
\DisplayProof
\end{center}

\smallskip
\begin{center}
\AxiomC{$\Gamma \vdash a : A$}
\AxiomC{$\Gamma \vdash p : a \idtype a'$}
\AxiomC{$\Gamma \vdash i : I$}
\TrinaryInfC{$\Gamma \vdash \at(a, a', p, i) : A$}
\DisplayProof
\end{center}

\smallskip
\begin{center}
\AxiomC{$\Gamma \vdash A\ \type$}
\AxiomC{$\Gamma, x : I \vdash a : A$}
\AxiomC{$\Gamma \vdash i : I$}
\TrinaryInfC{$\Gamma \vdash \at(a[x \repl \leftI], a[x \repl \rightI], \pathI(A, a), i) \deq a[x \repl i]$}
\DisplayProof
\end{center}

\smallskip
\begin{center}
\AxiomC{$\Gamma \vdash p : a \idtype a'$}
\UnaryInfC{$\Gamma \vdash \pathI(ty(a),\,x.\,\at(a, a', p, x)) \deq p$}
\DisplayProof
\end{center}

\smallskip
\begin{center}
\AxiomC{$\Gamma \vdash p : a \idtype a'$}
\UnaryInfC{$\Gamma \vdash \at(a, a', p, \leftI) \deq a$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash p : a \idtype a'$}
\UnaryInfC{$\Gamma \vdash \at(a, a', p, \rightI) \deq a'$}
\DisplayProof
\end{center}

We can summarize the relationship between different theories in the following diagram of theories:
\[ \xymatrix{ & \IdT_- \ar[rr] \ar[d] & & \IdT \ar[d] \\
              \coeT'_0 + \sqT \ar[r] & \coeT'_1 \ar[r] & \coeT'_2 \ar[d]    \ar[r] & \coeT'_0 + \sigma + \sqT \ar@<1.5pt>[r] \ar[d] & \coeT'_1 + \sigma \ar[d] \ar@<1.5pt>[l] \\
              \sqT           \ar[r]  & \dcT     \ar[r] & \coeT'_2 + \beta_2 \ar[r] & \coeT'_0 + \sigma + \dcT \ar@<1.5pt>[r]        & \coeT'_1 + \sigma + \dcT \ar@<1.5pt>[l]
            } \]
where $\coeT'_\alpha = \coeT_\alpha + \HPath$ and each arrow $T \to T'$ represents an interpretation of $T$ in $T'$.

Interpretations $\IdT_- \to \IdT$ and $\coeT'_1 \to \coeT'_2$ are obvious.
Let us construct the vertical arrows.
Define $\refl$ and $J$ as follows:
\begin{align*}
\refl(a) & = \pathI(ty(a), a) \\
J(D, d, a, a', p) & = \coe_0(i.\,D', d[a])
\end{align*}
where $D'$ is defined as follows:
\[ D[a, \at(a, a', p, \sq(i,\rightI)), \pathI(ty(a),\,j.\,\at(a, a', p, \sq(i,j)))]. \]
Note that $J(D, d, a, a, \refl(a))$ equals to $\coe_0(i.\,D[a,a,\refl(a)], d[a])$.
Thus if we have the $\sigma$ rule, then the following equation holds:
\[ \vdash J(D, d, a, a, \refl(a)) \deq d[a] \]
If we have $\coe_1$, then we can define $\Jeq(D,d,a)$ as follows:
\[ \coe_0(j.\,\coe_1(i. D[a,a,\refl(a)], d[a], j) \idtype d[a], \refl(d[a])). \]

We can define an interpretation $\sqT \to \coeT'_1$ as follows:
\[ \sq(i,j) = \at(\leftI, j, \coe_1(x.\,\leftI \idtype x, \refl(\leftI), j), i). \]

Now, let us define an interpretation $\coeT_2 \to \coeT'_0 + \sqT + \sigma$.
First, note that we can define an interpretation $\coeT_1 \to \coeT_0 + \sqT + \sigma$ as follows: $\coe_1(D, d, j) = \coe_0(i.\,D[\sq(i,j)], d)$.
Then let $\Ic(i) = \pathI(I, j.\,\sq(j,i))$.
Since $\Ic(i) : \leftI \idtype i$, we can define a term $\dc'(i,j)$ of type $i \idtype j$.
Now, let $\coe_2(D, i, d, j)$ be equal to $\coe_0(x.\,D[\at(i, j, \dc'(i,j), x)], d)$.
Note that $\dc'(\leftI,\leftI) \deq \refl(\leftI)$; hence we have the following equality:
\[ \coe_2(D, \leftI, d, \leftI) \deq d. \]

Arrows in the bottom row are easy to define:
\begin{align*}
\sq(i,j) & = \dc(\leftI,j,i) \\
\dc(i,j,k) & = \at(i,j,\coe_2(x.\,i \idtype x, i, \refl(i), j),k) \\
\coe_2(D, i, d, j) & = \coe_0(x.\,D[x \repl \dc(i,j,x)], d)
\end{align*}

\subsection{Heterogeneous path types}

\emph{Heterogeneous path types} is a useful generalization of homogeneous path types.
Let $\PathT$ be the theory with function symbols $\Path : (ty,n+1) \times (tm,n) \times (tm,n) \to (ty,n)$,
$\pathI : (tm,n+1) \to (tm,n)$, and $\at : (ty,n+1) \times (tm,n) \times (tm,n) \times (tm,n) \times (tm,n) \to (tm,n)$, and the following axioms:
\begin{center}
\AxiomC{$\Gamma, x : I \vdash A\ \type$}
\AxiomC{$\Gamma \vdash a : A[x \repl \leftI]$}
\AxiomC{$\Gamma \vdash a' : A[x \repl \rightI]$}
\TrinaryInfC{$\Gamma \vdash \Path(A, a, a')\ \type$}
\DisplayProof
\end{center}

\smallskip
\begin{center}
\AxiomC{$\Gamma, x : I \vdash a : A$}
\UnaryInfC{$\Gamma \vdash \pathI(a) : \Path(A, a[x \repl \leftI], a[x \repl \rightI])$}
\DisplayProof
\end{center}

\smallskip
\begin{center}
\AxiomC{$\Gamma \vdash p : \Path(A, a, a')$}
\AxiomC{$\Gamma \vdash i : I$}
\BinaryInfC{$\Gamma \vdash \at(A, a, a', p, i) : A[i]$}
\DisplayProof
\end{center}

\smallskip
\begin{center}
\AxiomC{$\Gamma, x : I \vdash a : A$}
\AxiomC{$\Gamma \vdash i : I$}
\BinaryInfC{$\Gamma \vdash \at(A, a[x \repl \leftI], a[x \repl \rightI], \pathI(a), i) \deq a[x \repl i]$}
\DisplayProof
\end{center}

\smallskip
\begin{center}
\AxiomC{$\Gamma \vdash p : \Path(A, a, a')$}
\UnaryInfC{$\Gamma \vdash \pathI(y.\,\at(A, a, a', p, y)) \deq p$}
\DisplayProof
\end{center}

\smallskip
\begin{center}
\AxiomC{$\Gamma \vdash p : \Path(A, a, a')$}
\UnaryInfC{$\Gamma \vdash \at(A, a, a', p, \leftI) \deq a$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash p : \Path(A, a, a')$}
\UnaryInfC{$\Gamma \vdash \at(A, a, a', p, \rightI) \deq a'$}
\DisplayProof
\end{center}

We will often omit the first three arguments of $\at$ since it is easy to infer them from the type of the fourth argument.
We can interpret $\HPath$ in $\PathT$ as follows: $a \idtype a' = \Path(x.\,ty(a), a, a')$.

The theory we are describing has many similarities to the theory of cubical sets.
The reason is that we can think of contexts $x_1 : I, \ldots x_n : I \vdash$ as $n$-dimensional cubes.
Let $M$ be a model of $I$ and let $A,B \in M_{(ty,0)}$, then the sequence of sets
$\{\,b \in M_{(tm,n+1)}\ |\ x : A, x_1 : I, \ldots x_n : I \vdash b : B\,\}$ has a natural structure of a cubical set.
If $M$ is a model of $\coeT_1 + \PathT$, then these cubical sets are fibrant; that is, have fillers for all boxes (a box in a cubical set is an analog of a horn in a simplicial set).
We will define operations $\Fill^n$, which give us these fillers, in subsection~\ref{sec:fillers}.
Now we need these fillers to define several operations that we will use in the next subsection.

First, let us define $\sqT_l$ which satisfies all of the axioms of $\sq$ together with axiom $\Gamma \vdash \sq(i,\rightI) \deq i$.
This operation is analogous to connections in cubical sets.
Actually, this construction shows that cubical sets that we defined before from a model of the theory have connections.
We can define $\sqT_l$ by filling the following box:
\[ \xymatrix @C=0.5pc @R=0.5pc
    { \leftI \ar[rrrr] \ar[dddd] &            & &                        & \leftI \ar[dddd] \\
             & \leftI \ar[rr] \ar[dd] \ar[ul] & & \leftI \ar[dd] \ar[ur] & \\
             &                                & &                        & \\
             & \leftI \ar[rr] \ar[dl]         & & \leftI \ar[dr]         & \\
      \leftI \ar[rrrr]           &            & &                        & \rightI
    }\]
The inner, left, and top squares are $\lambda i\,j.\,\leftI$, the bottom and right squares are $\sq$,
and the filler gives us the outer square which is the required operation $\sq_l$.
Formally, we define $\sq_l(i,j)$ as
\[ \at(\at(\coe_0(x_1.\,\Path(x_2.\,\leftI \idtype \sq(x_1,x_2), \refl(\leftI), p_1), p_2),i),j) \]
where $p_1 = \pathI(x_3.\,\sq(x_1,x_3))$, $p_2 = \refl(\refl(\leftI))$.

Operation $\sq_r$ is similar to $\sq_l$; it satisfies the following axioms:
\begin{align*}
\Gamma & \vdash \sq_r(\leftI,j) \deq j \\
\Gamma & \vdash \sq_r(\rightI,j) \deq \rightI \\
\Gamma & \vdash \sq_r(i,\leftI) \deq i \\
\Gamma & \vdash \sq_r(i,\rightI) \deq \rightI
\end{align*}
We can define $sq_r$ by filling the following box:
\[ \xymatrix @C=0.5pc @R=0.5pc
    { \leftI \ar[rrrr] \ar[dddd] &            & &                        & \rightI \ar[dddd] \\
             & \leftI \ar[rr] \ar[dd] \ar[ul] & & \leftI \ar[dd] \ar[ur] & \\
             &                                & &                        & \\
             & \leftI \ar[rr] \ar[dl]         & & \leftI \ar[dr]         & \\
      \rightI \ar[rrrr]           &           & &                        & \rightI
    }\]
The inner square is $\lambda x_1\,x_2.\,\leftI$, the left square is $\lambda x_2\,x_3.\,\sq_l(x_2,x_3)$,
the top square is $\lambda x_1\,x_3.\,\sq_l(x_1,x_3)$, the right square is $\lambda x_2\,x_3.\,x_3$,
and the bottom square is $\lambda x_1\,x_3.\,x_3$.
The outer square gives us the required operation $\sq_r$.

We will also need operation $\dc'$ which satisfies the following axioms:
\begin{align*}
\Gamma & \vdash \dc'(i,j,\leftI) \deq i \\
\Gamma & \vdash \dc'(i,j,\rightI) \deq j \\
\Gamma & \vdash \dc'(\leftI,\leftI,k) \deq \leftI \\
\Gamma & \vdash \dc'(\rightI,\rightI,k) \deq \rightI
\end{align*}
Thus we need to find a map from $I^3$ to $I$, and we can do this by filling some box.
Conditions that we put on $\dc'$ are not enough to define a box, but we can fill missing parts.
Consider the following picture:
\[ \xymatrix @C=0.5pc @R=0.5pc
    { \rightI \ar[rrrr] \ar[dddd] &           & &                        & \rightI \ar[dddd] \\
             & \leftI \ar[rr] \ar[dd] \ar[ul] & & \leftI \ar[dd] \ar[ur] & \\
             &                                & &                        & \\
             & \leftI \ar[rr] \ar[dl]         & & \rightI \ar[dr]        & \\
      \leftI \ar[rrrr]            &           & &                        & \rightI
    }\]
Here $j$ is going from left to right, $k$ is going from top to bottom, and $i$ is going diagonally.
Top square is $\lambda j\,i.\,i$, bottom square is $\lambda j\,i.\,j$, left side of the inner square is $\lambda k.\,\leftI$,
and the right side of the outer square is $\lambda k.\,\rightI$.
We can take the inner square to be $\lambda j\,k.\,\sq_l(j,k)$ and the right square to be $\lambda j\,k.\,\sq_r(j,k)$.
The left square we can define by the filler operation.

For every $\Gamma \vdash a : A$, $\Gamma \vdash a' : A$, we have a type of 1-dimensional cubes (that is, paths) between $a$ and $a'$.
We could also consider the type of $n$-dimensional cubes with given boundary.
For $n = 2$ this can be described as follows.
Suppose that we have terms $\Gamma, x : I \vdash p_{-0} : A$, $\Gamma, x : I \vdash p_{-1} : A$, $\Gamma, y : I \vdash p_{0-} : A$ and $\Gamma, y : I \vdash p_{1-} : A$
such that $p_{-0}[x \repl \leftI] = p_{0-}[y \repl \leftI] = a_{00}$, $p_{-0}[x \repl \rightI] = p_{1-}[y \repl \leftI] = a_{10}$,
$p_{0-}[y \repl \rightI] = p_{-1}[x \repl \leftI] = a_{01}$ and $p_{1-}[y \repl \rightI] = p_{-1}[x \repl \rightI] = a_{11}$.
\[ \xymatrix{ a_{00} \ar[r]^{p_{-0}} \ar[d]_{p_{0-}} & a_{10} \ar[d]^{p_{1-}} \\
              a_{01} \ar[r]_{p_{-1}}                 & a_{11}
            } \]
Then we define type $\Square(p_{-0},p_{-1},p_{0-},p_{1-})$ of 2-dimensional cubes as
\[ \Path(x.\,p_{-0} \idtype p_{-1}, \pathI(y.\,p_{0-}), \pathI(y.\,p_{1-})). \]

We can analogously define types of $n$-dimensional cubes for all $n$.
It is difficult to describe such types without heterogeneous path types,
but we can do this at least for small $n$.
For example, for $n = 2$ we can define it as either $\pathI(p_{-0}) * \pathI(p_{1-}) \idtype \pathI(p_{0-}) * \pathI(p_{-1})$
(where $*$ is a concatenation of paths) or $\pathI(p_{0-}) \idtype \pathI(p_{-0}) * \pathI(p_{1-}) * \sym(\pathI(p_{-1}))$.
It is easy to see that these types are (homotopy) equivalent; that is, we can define mutually inverse functions between them.
We can show that they are also equivalent to $\Square(p_{-0},p_{-1},p_{0-},p_{1-})$:

\begin{lem}[squares-eq]
Types $\Square(p_{-0},p_{-1},p_{0-},p_{1-})$ and $\pathI(p_{0-}) \idtype \pathI(p_{-0}) * \pathI(p_{1-}) * \sym(\pathI(p_{-1}))$ are equivalent.
\end{lem}
\begin{proof}
Let $*_l$ be a concatenation of paths such that $\refl(x) *_l p \idtype p$ and let $*_r$ be a concatenation such that $p *_r \refl(y) \idtype p$.
Since all concatenations are equivalent, we can replace $*$ with either of these operations.
We construct a type $\Gamma, i : I \vdash H$ such that $H[\rightI] = \Square(p_{-0},p_{-1},p_{0-},p_{1-})$ and $H[\leftI] = (\pathI(p_{0-}) \idtype \pathI(p_{-0}) *_l \pathI(p_{1-}) *_r \sym(\pathI(p_{-1})))$.
Let $H$ be equal to
\[ \Path(x.\,p_{-0}[\sq_l(x,i)] \idtype p_{-1}[\sq_l(x,i)], \pathI(y.\,p_{0-}), t), \]
where $t$ equals to
\[ \pathI(j.\,p_{-0}[\sq_r(i,j)]) *_l \pathI(y.\,p_{1-}) *_r \sym(\pathI(j.\,p_{-1}[\sq_r(i,j)])). \]
Then $H$ satisfies the required conditions.
It is easy to define an equivalence between $H[\leftI]$ and $H[\rightI]$.
\end{proof}

\subsection{Local versions of $\coeT$}

Usually, we can define two different versions of an eliminator for a type in type theory, one of which is stronger.
For example, stronger versions of $\coeT$ look like this:

\medskip
\begin{center}
\AxiomC{$\Gamma, x : I, \Delta \vdash D\ \type$}
\AxiomC{$\Gamma, \Delta[x \repl \leftI] \vdash d : D[x \repl \leftI]$}
\BinaryInfC{$\Gamma, \Delta[x \repl \rightI] \vdash \coe^l_0(D, d) : D[x \repl \rightI]$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : I, \Delta \vdash D\ \type$}
\AxiomC{$\Gamma, \Delta[x \repl \leftI] \vdash d : D[x \repl \leftI]$}
\AxiomC{$\Gamma \vdash i : I$}
\TrinaryInfC{$\Gamma, \Delta[x \repl i] \vdash \coe^l_1(D, d, i) : D[x \repl i]$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : I, \Delta \vdash D\ \type$}
\AxiomC{$\Gamma, \Delta[x \repl \leftI] \vdash d : D[x \repl \leftI]$}
\BinaryInfC{$\Gamma, \Delta[x \repl \leftI] \vdash \coe^l_1(D, d, \leftI) \deq d$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : I, \Delta \vdash D\ \type$}
\AxiomC{$\Gamma \vdash i : I$}
\AxiomC{$\Gamma, \Delta[x \repl i] \vdash d : D[x \repl i]$}
\AxiomC{$\Gamma \vdash j : I$}
\QuaternaryInfC{$\Gamma, \Delta[x \repl j] \vdash \coe^l_2(D, i, d, j) : D[x \repl j]$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : I, \Delta \vdash D\ \type$}
\AxiomC{$\Gamma, \Delta[x \repl \leftI] \vdash d : D[x \repl \leftI]$}
\BinaryInfC{$\Gamma, \Delta[x \repl \leftI] \vdash \coe^l_2(D, \leftI, d, \leftI) \deq d$}
\DisplayProof
\end{center}

We can also consider theory $\coeT^l_2 + \beta^l_2$ which is $\coeT^l_2$ together with the following axiom:
\begin{center}
\AxiomC{$\Gamma, x : I, \Delta \vdash D\ \type$}
\AxiomC{$\Gamma \vdash i : I$}
\AxiomC{$\Gamma, \Delta[x \repl i] \vdash d : D[x \repl i]$}
\TrinaryInfC{$\Gamma, \Delta[x \repl i] \vdash \coe^l_2(D, i, d, i) \deq d$}
\DisplayProof
\end{center}

We call such versions of these operations \emph{local}, and the ones that were defined before \emph{global}.
The relationship between local versions of these operations is the same as between global ones.
Usually, if we have $\Pi$-types, then we can define local versions in terms of global, but without them local are strictly stronger.
But this is not the case for $\coeT_2 + \beta_2$; it turns out that $\coeT^l_2 + \beta^l_2$ can be defined in $\coeT_2 + \beta_2$ even without $\Pi$-types.

It is not convenient to work with such local operations directly since context in the conclusion is extended, but we can always rewrite them in the usual form.
For example, if $\Delta$ equals to $y_1 : B_1, \ldots y_k : B_k$, then we can rewrite $\coeT^l_2$ as follows:
\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter \Gamma, x : I, \Delta \vdash D\ \type$
\noLine
\UnaryInf$\fCenter \Gamma \vdash i : I$
\noLine
\UnaryInf$\fCenter \Gamma, \Delta[x \repl i] \vdash d : D[x \repl i]$
\noLine
\UnaryInf$\fCenter \Gamma \vdash j : I$
\def\extraVskip{2pt}
\Axiom$\fCenter \Gamma \vdash b_1 : B_1[x \repl j]$
\noLine
\UnaryInf$\fCenter \ldots$
\noLine
\UnaryInf$\fCenter \Gamma \vdash b_k : B_k[x \repl j, y_1 \repl b_1, \ldots y_{k-1} \repl b_{k-1}]$
\BinaryInfC{$\Gamma \vdash \coe^{l'}_2(D, i, d, j, b_1, \ldots b_k) : D[x \repl j, y_1 \repl b_1, \ldots y_k \repl b_k]$}
\DisplayProof
\end{center}
Then theories $\coeT^l_2$ and $\coeT^{l'}_2$ are isomorphic; that is, we can interpret $\coeT^l_2$ in $\coeT^{l'}_2$, and vice versa, and the interpretations are mutually inverse.
The interpretations are defined as follows:
\begin{align*}
\coe^l_2(D, i, d, j) & = \coe^{l'}_2(D, i, d, j, y_1, \ldots y_k) \\
\coe^{l'}_2(D, i, d, j, b_1, \ldots b_k) & = \coe^l_2(D, i, d, j)[b_1, \ldots b_k]
\end{align*}

Now, we can define an interpretation $\coeT^{l'}_2 + \beta^l_2 \to \coeT_2 + \beta_2$.
First, let $b'_m(z)$ be equal to
\[ \coe_2(x.\,B_m[y_1 \repl b_1'(x), \ldots y_{m-1} \repl b_{m-1}'(x)], j, b_m, z) \]
for every $1 \leq m \leq k$.
If $\Gamma \vdash z : I$, then $\Gamma \vdash b_m'(z) : B_m[x \repl z, y_1 \repl b_1'(z), \ldots b_{m-1}'(z)]$.
Now, we can define $\coe^{l'}_2(D, i, d, j, b_1, \ldots b_m)$ as follows:
\[ \coe_2(x.\,D[y_1 \repl b_1'(x), \ldots y_k \repl b_k'(x)], i, d[y_1 \repl b'_1(i), \ldots y_k \repl b'_k(i)], j) \]

Theories $\coeT^{l'}_0$ and $\coeT^{l'}_1$ are defined similarly to $\coe^{l'}_2$.
Theory $\coeT^{l'}_1 + \sigma^l$ is $\coeT^{l'}_1$ together with the following axiom:
\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter \Gamma, \Delta \vdash D\ \type$
\noLine
\UnaryInf$\fCenter \Gamma, \Delta \vdash d : D$
\noLine
\UnaryInf$\fCenter \Gamma \vdash i : I$
\def\extraVskip{2pt}
\Axiom$\fCenter \Gamma \vdash b_1 : B_1$
\noLine
\UnaryInf$\fCenter \ldots$
\noLine
\UnaryInf$\fCenter \Gamma \vdash b_k : B_k[y_1 \repl b_1, \ldots y_{k-1} \repl b_{k-1}]$
\BinaryInfC{$\Gamma \vdash \coe^{l'}_1(D, d, i, b_1, \ldots b_k) \deq d[b_1, \ldots b_k]$}
\DisplayProof
\end{center}

If we have heterogeneous path types, then we can define $\coeT^{l'}_0 + \sigma^l + \sqT$ in terms of $\coeT_0 + \sigma + \sqT$ and $\coeT^{l'}_1 + \sigma^l$ in terms of $\coeT_1 + \sigma$.
We can define map $\coeT^{l'}_1 \to \coeT^{l'}_0$ as before:
\[ \coe^{l'}_1(x\,y_1 \ldots y_k.\,D, d, i, b_1, \ldots b_k) = \coe^{l'}_0(x\,y_1 \ldots y_k.\,D[x \repl \sq(x,i)], d, b_1, \ldots b_k) \]
Since we already know that there are arrows going in both directions between $\coeT_0 + \sigma + \sqT$ and $\coeT_1 + \sigma$,
we just need to construct a map $\coeT^{l'}_0 + \sigma^l + \sqT + \PathT \to \coeT_0 + \sigma + \sqT + \PathT$.

To do this, first we define a map $\coeT_2 + \beta_1 \to \coeT_0 + \sigma + \sqT + \PathT$:
\[ \coe_2(D, i, d, j) = \coe_0(x.\,D[\dc'(i,j,x)], d) \]
Now, we can define $\coe^{l'}_0(D, d, b_1, \ldots b_m)$ as follows:
\[ \coe_0(x.\,D[y_1 \repl b_1'(x), \ldots y_k \repl b_k'(x)], d[y_1 \repl b'_1(\leftI), \ldots y_k \repl b'_k(\leftI)]) \]
where $b'_m(z)$ equals to
\[ \coe_2(x.\,B_m[y_1 \repl b_1'(x), \ldots y_{m-1} \repl b_{m-1}'(x)], \rightI, b_m, z) \]

\subsection{Fillers}
\label{sec:fillers}

We already saw examples of two- and three-dimensional filler operations.
Here we define theories $\FillT^l_{tm}$ and $\FillT_{tm}$ of local and global filler operations.
We will also construct morphisms between $\FillT_{tm} + \PathT$ and $\coeT_1 + \PathT$;
It might be possible to construct a map from $\FillT^l_{tm}$ to $\coeT_2 + \beta_2 + \PathT$, but it is more complicated and we will not need this construction.
In this subsection we switch back to the presentation of terms using De Bruijn indices since it will be notationally more convenient.

The theory $\FillT^l_{tm}$ has function symbol $\Fill^n_{(tm,n+k)} : (ty,n+k) \times (tm,n-1+k)^{2n-1} \to (tm,n+k)$
for every $n,k \in \mathbb{N}$, $n > 0$, and the following axioms:
\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter x_1 : I, \ldots x_n : I, \Delta \vdash D\ \type$
\noLine
\UnaryInf$\fCenter x_1 : I, \ldots x_{i-1} : I, x_{i+1} : I, \ldots x_n : I, \Delta[x_i \repl c] \vdash d_{[x_i = c]} : D[x_i \repl c]$
\noLine
\UnaryInf$\fCenter d_{[x_{i_2} = c']}[x_{i_1} \repl c] \deq d_{[x_{i_1} = c]}[x_{i_2} \repl c'],\ 0 \leq i_1 < i_2 \leq n-1$
\def\extraVskip{2pt}
\UnaryInf$\fCenter x_1 : I, \ldots x_n : I, \Delta \vdash \Fill^n_{(tm,n+k)}(D, d_{[x_n = \leftI]}, d_{[x_n = \rightI]}, \ldots d_{[x_1 = \leftI]}) : D$
\DisplayProof
\end{center}
where $\Fill^n_{(tm,n+k)}$ has arguments of the form $d_{[i = c]}$ for every $0 \leq i < n$ and $c \in \{ \leftI, \rightI \}$ except for $d_{[n-1 = \rightI]}$.

\medskip
\begin{center}
\def\extraVskip{1pt}
\Axiom$\fCenter x_1 : I, \ldots x_n : I, \Delta \vdash D\ \type$
\noLine
\UnaryInf$\fCenter x_1 : I, \ldots x_{i-1} : I, x_{i+1} : I, \ldots x_n : I, \Delta[x_i \repl c] \vdash d_{[x_i = c]} : D[x_i \repl c]$
\noLine
\UnaryInf$\fCenter d_{[x_{i_2} = c']}[x_{i_1} \repl c] \deq d_{[x_{i_1} = c]}[x_{i_2} \repl c'],\ 0 \leq i_1 < i_2 \leq n-1$
\def\extraVskip{2pt}
\UnaryInf$\fCenter \Fill^n_{(tm,n+k)}(D, d_{[x_n = \leftI]}, d_{[x_n = \rightI]}, \ldots d_{[x_1 = \leftI]})[x_i = c] \deq d_{[x_i = c]}$
\DisplayProof
\end{center}
\medskip

The theory $\FillT_{tm}$ of global filler operations is the subtheory of $\FillT^l_{tm}$ which has only function symbols of the form $\Fill^n_{(tm,n+0)}$.
We will denote such function symbols by $\Fill_{(tm,n)}$.

It is easy to define an interpretation of $\coeT^l_1$ in $\FillT^l_{tm}$: $\coe^l_1(D, d, i) = \Fill^1(D, d)[x_1 \repl i]$.
We can also define $\Fill^1_{(tm,1+k)}(D, d_{[x_1 = \leftI]})$ in terms of $\coe^l_1$ as $\coe^l_1(D, d_{[x_1 = \leftI]}, x_1)$.
Actually, the theory $\coeT^l_1$ and the subtheory of $\FillT^l_{tm}$ which consists of $\Fill^1_{(tm,1+k)}$ are isomorphic.

We can define analogous maps between $\FillT_{(tm,1)}$ and $\coeT_1$, but we can also define an interpretation $\FillT_{tm} \to \coeT_1 + \PathT$.
We define terms $\Fill_{(tm,n)}$ by induction on $n$.
We already defined this term for $n = 1$, and we can define $\Fill_{(tm,n+1)}$ as
\[ \at(\Fill_{(tm,n)}(\Path(x_{n+1}.\,D, d_{[x_{n+1} = \leftI]}, d_{[x_{n+1} = \rightI]}), p_{n,\leftI}, p_{n,\rightI}, \ldots p_{1,\leftI}), x_1), \]
where $p_{i,c} = \pathI(x_{n+1}.\,d_{[x_i = c]})$.

\subsection{Univalence}
\label{sec:univalence}

Let $\wUA$ be an extension of $\coeT_0$ with one additional symbol:
\[ \iso : (ty,n)^2 \times (tm,n+1)^4 \times (tm,n) \to (ty,n). \]

Axioms of this theory have a lot of premises, so we list them now.
We will denote by $S$ the following set of formulae:
\begin{align*}
\Gamma & \vdash A\ \type \\
\Gamma & \vdash B\ \type \\
\Gamma, x : A & \vdash b : B \\
\Gamma, y : B & \vdash a : A \\
\Gamma, x : A & \vdash p : a[y \repl b] \idtype x \\
\Gamma, y : B & \vdash q : b[x \repl a] \idtype y
\end{align*}

Now, we can define axioms of $\wUA$:
\medskip
\begin{center}
\AxiomC{$S$}
\AxiomC{$\Gamma \vdash j : I$}
\BinaryInfC{$\Gamma \vdash \iso(A, B, b, a, p, q, j)\ \type$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$S$}
\UnaryInfC{$\Gamma \vdash \iso(A, B, b, a, p, q, \leftI) \deq A$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$S$}
\UnaryInfC{$\Gamma \vdash \iso(A, B, b, a, p, q, \rightI) \deq B$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$S$}
\AxiomC{$\Gamma \vdash a' : A$}
\BinaryInfC{$\Gamma \vdash \coe_0(j.\,\iso(A, B, b, a, p, q, j), a') \deq b[a']$}
\DisplayProof
\end{center}
\medskip

This theory is similar to the univalence axiom, but it is defined for all types.
Actually, it seems that it is weaker than ordinary univalence, therefore we call this theory weak univalence.
We can add some additional rules to get the full univalence axiom, but this version will suffice for our purposes.
The (weak) univalence axiom for a universe follows from the assumption that this universe is closed under $\iso$.

Although rules of $\wUA$ do not imply that equivalences and paths between types are equivalent, we still can show that they are related.
First, we need to define a theory of equivalences.
Several equivalent definitions of equivalences are given in \cite{hottbook},
but some of them require additional constructions such as $\Sigma$- or $\Pi$-types.
Thus we will use a definition which requires only path types (actually, we can formulate it in such a way that $I$ will suffice).
Let $\Eq$ be the theory with the following axioms:
\begin{align*}
\Gamma & \vdash A\ \type \\
\Gamma & \vdash B\ \type \\
\Gamma, x : A & \vdash b : B \\
\Gamma, y : B & \vdash a_1 : A \\
\Gamma, x : A & \vdash p : a_1[y \repl b] \idtype x \\
\Gamma, y : B & \vdash a_2 : A \\
\Gamma, y : B & \vdash q : b[x \repl a_2] \idtype y
\end{align*}

Let $\UEq$ be the theory with one axiom $\Gamma, i : I \vdash H\ \type$.
There is a canonical morphism $\varphi : \Eq + \coeT_2 + \beta_1 \to \UEq + \coeT_2 + \beta_2$.
To define it, let us first introduce auxiliary terms: $f(k) = \coe_2(i.\,H, \leftI, x, k)$ and $g(k) = \coe_2(i.\,H, \rightI, y, k)$.
If $\Gamma \vdash k : I$, then $\Gamma, x : H[i \repl \leftI] \vdash f(k) : H[i \repl k]$ and $\Gamma, y : H[i \repl \rightI] \vdash g(k) : H[i \repl k]$.
Now, we can define $\varphi$ as follows:
\begin{align*}
\varphi(A) & = H[i \repl \leftI] \\
\varphi(B) & = H[i \repl \rightI] \\
\varphi(b) & = f(\rightI) \\
\varphi(a_1) & = g(\leftI) \\
\varphi(a_2) & = g(\leftI) \\
\varphi(p) & = \coe_2(j.\,\coe_2(i.\,H, j, f(j), \leftI) \idtype x, \leftI, \refl(x), \rightI) \\
\varphi(q) & = \coe_2(j.\,\coe_2(i.\,H, j, g(j), \rightI) \idtype y, \rightI, \refl(x), \leftI)
\end{align*}

A theory $\UA$ of univalence should satisfy condition that $\varphi + \id_{\UA} : \Eq + \coeT_2 + \beta_1 + \UA \to \UEq + \coeT_2 + \beta_1 + \UA$ is an equivalence of theories (in some sense).
In the case of $\wUA$, we still can construct an interpretation $\psi : \UEq + \coeT_2 + \beta_1 + \wUA \to \Eq + \coeT_2 + \beta_1 + \wUA$ such that $\psi \circ \varphi'$ is homotopic to $\id_{\Eq + \coeT_2 + \beta_1 + \wUA}$, where $\varphi' = \varphi + \id_{\wUA}$.
This means that for every symbol $x$ of $\Eq$ such that $\Delta \vdash x$ we can define a term $h(x)$ in $\Eq$ such that
$\Delta, i : I \vdash h(x)$, axioms of $\Eq$ hold, $\Delta \vdash h(x)[\leftI] \deq \psi(\varphi(x))$ and $\Delta \vdash h(x)[\rightI] \deq x$.

\begin{lem}[UA]
There exists an interpretation $\psi : \UEq + \coeT_2 + \beta_1 + \wUA \to \Eq + \coeT_2 + \beta_1 + \wUA$ such that $\psi \circ \varphi'$ is homotopic to $\id$.
\end{lem}
\begin{proof}
Let $q_1$ be the concatenation of paths $\pathI(j.\,b[x \repl \at(a_1, a_2, p_a,j)])$ and $q$.
Let $p_a$ be the path between $a_1$ and $a_2$ which can be obtained from $p$ and $q$ as the following concatenation:
\[ a_1 = a_1[y \repl y] \idtype a_1[y \repl b[x \repl a_2]] = a_1[y \repl b][x \repl a_2] \idtype x[x \repl a_2] = a_2. \]
Then we define $\psi(H)$ as $\iso(A, B, b, a_1, p, q_1, i)$.

We can define $h(A)$ as $A$, $h(B)$ as $B$ and $h(b)$ as $b$.
Thus we only need to construct $h(a_1)$, $h(a_2)$, $h(p)$ and $h(q)$.
Terms $h(a_1)$ and $h(a_2)$ should be the following paths:
\begin{align*}
& h(a_1) : \coe_2(i.\,\psi(H), \rightI, y, \leftI) \idtype a_1 \\
& h(a_2) : \coe_2(i.\,\psi(H), \rightI, y, \leftI) \idtype a_2
\end{align*}
Terms $h(p)$ and $h(q)$ should be squares with the following boundaries:
\[ \xymatrix{ \coe_2(i.\,\psi(H), \rightI, b, \leftI) \ar[rr]^-{\psi(\varphi'(p))} \ar[d]_{h(a_1)[y \repl b]} & & x \ar[d]^{\refl(x)} \\
              a_1[y \repl b] \ar[rr]_-p                                                                       & & x
            } \]
\[ \xymatrix{ b[x \repl \coe_2(i.\,\psi(H), \rightI, y, \leftI)] \ar[rr]^-{\psi(\varphi'(q))} \ar[d]_{b[x \repl h(a_2)]} & & y \ar[d]^{\refl(y)} \\
              b[x \repl a_2] \ar[rr]_-q                                                                                  & & y
            } \]
We construct $h(a_1)$ and $h(p)$, the other two terms are constructed analogously.
First, note that to construct a square with boundary given on the left, it is enough to construct a square with boundary given on the right:
\[ \xymatrix{ a_{00} \ar[r]^{p_{-0}} \ar[d]_{p_{0-}} & a_{10} \ar[d]^{p_{1-}} \\
              a_{01} \ar[r]_{p_{-1}}                 & a_{11}
            }
\qquad
   \xymatrix{ a_{00}[x \repl a_1] \ar[rr]^{p_{-0}[x \repl a_1]} \ar[d]_{p_{0-}[x \repl a_1]} & & a_{10}[x \repl a_1] \ar[d]^{p_{1-}[x \repl a_1]} \\
              a_{01}[x \repl a_1] \ar[rr]_{p_{-1}[x \repl a_1]}                              & & a_{11}[x \repl a_1]
            } \]
Indeed, if $T$ is a filler for the square on the right, then we can construct the following diagram:
\[ \xymatrix{ a_{00} \ar[rr]^-{a_{00}[x \repl \sym(p)]} \ar[d]_{p_{0-}} & & a_{00}[x \repl a_1'] \ar[rr]^{p_{-0}[x \repl a_1']} \ar[d]_{p_{0-}[x \repl a_1']} & & a_{10}[x \repl a_1'] \ar[d]_{p_{1-}[x \repl a_1']} \ar[rr]^-{a_{10}[x \repl p]} & & a_{10} \ar[d]_{p_{1-}} \\
              a_{01} \ar[rr]_-{a_{01}[x \repl \sym(p)]}                 & & a_{01}[x \repl a_1'] \ar[rr]_{p_{-1}[x \repl a_1']}                               & & a_{11}[x \repl a_1']                               \ar[rr]_-{a_{10}[x \repl p]} & & a_{11}
            } \]
where $a_1' = a_1[y \repl b]$, the middle square is $T[y \repl b]$ and side squares are naturality squares.
The right one, for example, is defined as $p_{1-}[x \repl p]$.
\Rlem{squares-eq} implies that these squares commute (up to homotopy).
By naturality and \rlem{squares-eq}, top and bottom rows are homotopic to $p_{-0}$ and $p_{-1}$ respectively.
Thus $p_{-0} * p_{1-} \idtype p_{0-} * p_{-1}$, and \rlem{squares-eq} implies that there exists a filler for the corresponding square.

Thus to construct $h(p)$, it is enough to define $h(a_1)$ in such a way that the outer square in the following diagram commutes:
\[ \xymatrix{ \coe_2(i.\,\psi(H), \rightI, y, \leftI) \ar[r]^{q_1'} \ar[d]_{h(a_1)} & \coe_2(i.\,\psi(H), \rightI, b', \leftI) \ar[rr]^-{\psi(\varphi'(p))[x \repl a_1]} \ar[d]_{h(a_1)[y \repl b[x \repl a_1]]} & & a_1 \ar[d]_{\refl(a_1)} \\
              a_1 \ar[r]_{a_1[y \repl \sym(q_1)]} & a_1[y \repl b'] \ar[rr]_-{p[x \repl a_1]}                                                                                                                     & & a_1
            } \]
where $b' = b[x \repl a_1]$ and $q_1' = \coe_2(i.\,\psi(H), \rightI, \sym(q_1), \leftI)$.
The left square commutes by naturality.
Since $q_1'$ has an inverse, the right square also commutes.
\end{proof}

\section{Model structure on models of theories with an interval type}
\label{sec:model-structure}

Let $T$ be an $I$-stable theory in which $\coeT_1 + \sigma + \PathT + \wUA$ can be interpreted.
Then we construct a model structure on the category of models of $T$.
Every object of this model category is fibrant and weak equivalences have several equivalent descriptions.

\subsection{Model structure}

Models of a partial Horn theory $T$ can be described by generators and relations.
If $X$ is an $\mathcal{S}$-set and $R$ is a set of formulas with free variables in $X$,
then there is a model $F(X,R)$ which has the following universal property.
For every model $M$, there is a natural isomorphism between the set of morphisms $F(X,R) \to M$
and the set of functions $X \to U(M)$ (where $U(M)$ is the underlying $\mathcal{S}$-set of $M$) for which formulas in $R$ hold.
Sometimes we will omit the set of generators if it can be inferred from the set of relations.
For examples, we will write $F(\{\,\vdash p : \Id(a,a')\,\})$ for the model $F(\{\,a : (tm,0), a' : (tm,0), p : (tm,0)\,\}, \{\,ty(p) = \Id(a,a')\,\})$.
Another examples is $F(\{\,x_1 : A_1, \ldots x_n : A_n \vdash a : A\,\})$,
which equals to $F(\{\,A_i : (ty,i), A : (ty,n), a : (tm,n)\,\}, \{\,ty(a) = A, ctx^i_{ty,n-i}(A) = A_{n-i}\,\})$.
Thus this model is isomorphic to the free model $F(\{\,a : (tm,n)\,\})$.

For every model $M$ of a theory $T$, we define a theory $\Lang(M)$.
It has function and predicate symbols of $T$ together with function symbol $O_a : s$ for every $a \in M_s$.
Axioms of $\Lang(M)$ are axioms of $T$ together with the following sequents:
\begin{align*}
& \sststile{}{} O_a \downarrow \\
& \sststile{}{} \sigma(O_{a_1}, \ldots O_{a_k}) = O_{M(\sigma)(a_1, \ldots a_k)} \\
& \sststile{}{} R(O_{a_1}, \ldots O_{a_k})
\end{align*}
for every $a \in M_s$, every $a_i \in M_{s_i}$,
every $\sigma \in \mathcal{F}$ such that $M(\sigma)(a_1, \ldots a_k)$ is defined,
and every $R \in \mathcal{P}$ such that $(a_1, \ldots a_k) \in M(R)$.

To construct a model structure on $\Mod{T}$, we need to recall a few definitions from \cite{f-model-structures}.
A reflexive path object $P(X)$ for an object $X$ is any factorization of the diagonal $X \to X \times X$.
A reflexive cylinder object $C_U(V)$ for a map $i : U \to V$ is any factorization of $[\id_V,\id_V] : V \amalg_U V \to V$.
The maps $f,g : V \to X$ are homotopic relative to a cylinder object $[\cyli_0,\cyli_1] : V \amalg_U V \to C_U(V)$, if there exists a map $h : C_U(V) \to X$
such that $h \circ \cyli_0 = f$ and $h \circ \cyli_1 = g$.
In this case we will write $f \sim_i g$.
We say that a map $f : X \to Y$ has RLP up to $\sim_i$ with respect to $i : U \to V$ if for every commutative square of the form
\[ \xymatrix{ U \ar[r]^u \ar@{}[dr]|(.7){\sim_i} \ar[d]_i & X \ar[d]^f \\
              V \ar[r]_v \ar@{-->}[ur]^g                  & Y,
            } \]
there is a dotted arrow $g : V \to X$ such that $g \circ i = u$ and $(f \circ g) \sim_i v$.

We will also need the following theorem from \cite{f-model-structures}:
\begin{thm}[model-structures]
Let $\C$ be a complete and cocomplete category, and let $\I$ be a set of maps of $\C$
such that the domains and the codomains of maps in $\I$ are cofibrant and small relative to $\Icell$.
For every $i : U \to V \in \I$, choose a reflexive relative cylinder object $C_U(V)$
such that $[\cyli_0,\cyli_1] : V \amalg_U V \to C_U(V) \in \Icof$.
Let $\J_\I = \{\ \cyli_0 : V \to C_U(V)\ |\ i : U \to V \in \I \ \}$, and
let $\we_\I$ be the set of maps which have RLP up to $\sim_i$ with respect to every $i \in \I$.

Suppose that for every object $X$, there exists a reflexive path object $P(X)$ such that the following conditions hold:
\begin{enumerate}
\item $p_0$ has RLP with respect to $\I$.
\item For every $f : X \to Y$, there exists a morphism of path objects $(f,P(f)) : P(X) \to P(Y)$,
\item For every object $X$, there exists a map $s : P(X) \to P(X)$ such that $p_0 \circ s = p_1$ and $p_1 \circ s = p_0$.
\item Either maps $\langle p_0, p_1 \rangle : P(X) \to X \times X$ have RLP with respect to $\J_\I$
or maps in $\Jcell[_\I]$ have RLP up to $\sim^{r*}$ with respect to the domains of maps in $\I$.
\end{enumerate}
Then there exists a cofibrantly generated model structure on $\C$ with $\I$ as a set of generating cofibrations,
$\J_\I$ as a set of generating trivial cofibrations, and $\we_\I$ as a class of weak equivalences.
\end{thm}
Here $\sim^{r*}$ denotes the reflexive transitive closure of the relation of right homotopy with respect to $P(X)$.

Let $\I_{tm}$ be the set of the following morphisms:
\[ i_{(tm,n)} : F(\{\,\Gamma \vdash A\ \type\,\}) \to F(\{\,\Gamma \vdash a : A\,\}) \]
Let $\I_{ty}$ be the set of the following morphisms:
\[ i_{(ty,n)} : F(\{\,\Gamma \vdash ctx\,\}) \to F(\{\,\Gamma \vdash A\ \type\,\}) \]
The set $\I$ of generating cofibrations is the union $\I_{tm} \cup \I_{ty}$.

For every $i : U \to V \in \I$, we need to define a relative cylinder object $C_U(V)$.
Let $C_{(tm,n)} = F(\{\,(\Gamma \vdash A\ \type), (\Gamma, x : I \vdash h : A)\,\})$.
If we define $\cyli_0(a)$ as $h[\leftI]$, $\cyli_1(a)$ as $h[\rightI]$ and $s(h)$ as $a$,
then these maps make $C_{(tm,n)}$ into a reflexive cylinder object for $i_{(tm,n)}$.

Let $C_{(ty,n)}$ be the initial $T$-model of the theory $\Eq$ defined in subsection~\ref{sec:univalence}.
Let $\cyli_0(A) = A$, $\cyli_1(A) = B$, and let $s : C_{(ty,n)} \to F(\{\,\Gamma \vdash A\ \type\,\})$ be defined as follows:
$s(A) = A$, $s(B) = A$, $s(b) = s(a_1) = s(a_2) = v_{n+1,0}$, $s(p) = s(q) = \refl(v_{n+1,0})$.
Then $C_{(ty,n)}$ is a reflexive cylinder object for $i_{(ty,n)}$.

Note that for every $i : U \to V \in \I$, $[\cyli_0,\cyli_1] : V \amalg_U V \to C_U(V)$ belongs to $\Icell[\I_{tm}]$.
If $i \in \I_{tm}$, then $[\cyli_0,\cyli_1]$ is (isomorphic to) $F(\{\,(\Gamma \vdash a : A), (\Gamma \vdash a' : A)\,\}) \to F(\{\,(\Gamma \vdash A), (\Gamma, x : I \vdash h : A)\,\})$,
and this map is isomorphic to $F(\{\,(\Gamma \vdash a : A), (\Gamma \vdash a' : A)\,\}) \to F(\{\,(\Gamma \vdash a : A), (\Gamma \vdash a' : A), (\Gamma \vdash p : a \idtype a')\,\})$,
which is a pushout of a map from $\I_{tm}$.
If $i \in \I_{ty}$, then it is easy to see that $[\cyli_0,\cyli_1]$ is a composition of five maps which are pushouts of maps from $\I_{tm}$.

There is another class of cylinder objects for maps in $\I_{ty}$.
Let $C'_{(ty,n)}$ be equal to $F(\{\,\Gamma, i : I \vdash H\ \type\,\})$, $\cyli_0(A) = H[i \repl \leftI]$, $\cyli_1(A) = H[i \repl \rightI]$.
We cannot use these cylinder objects directly since $[\cyli_0,\cyli_1]$ is not a cofibration; nevertheless, they will be useful later.
We will denote the set of maps of the form $\cyli_0 : F(\{\,\Gamma \vdash A\ \type\,\}) \to C'_{(ty,n)}$ by $\J'_{\I_{ty}}$.

Now, let us describe a general definition of a functor $P : \Mod{T} \to \Mod{T}$ that works for every $I$-stable theory $T$.
Let $P(X)_{(p,n)} = \{\,a \in X_{(p,n+1)}\ |\ ctx^n_{p,1}(a) = I\,\}$.
For every function and predicate symbol $S_n$, define $P(X)(S_n)(a_1, \ldots a_k)$ as $X(S_{n+1})(I, a_1, \ldots a_k)$.
For every morphism of models $f : X \to Y$, let $P(f)(a) = f(a)$.
The fact that $f$ is a morphism of models implies that $P(f)$ is a morphism too.
It is obvious that $P$ preserves identity morphisms and compositions.

Let us define maps $t : X \to P(X)$ and $p_0,p_1 : P(X) \to X$.
If $a \in X_{(p,n)}$ is such that $\Gamma \vdash a$, then define $t(a)$ as $x : I, \Gamma \vdash a$.
If $a \in P(X)_{(p,n)}$ is such that $x : I, \Gamma \vdash a$, then let $p_0(a) = (\Gamma[x \repl \leftI] \vdash a[x \repl \leftI])$
and $p_1(a) = (\Gamma[x \repl \rightI] \vdash a[x \repl \rightI])$.
Since function and predicate symbols are stable under the substitution operations, these definitions indeed determine morphisms of models.
The fact that $p_0 \circ t = p_1 \circ t = \id_X$ follows from properties of the substitution operations.
If the theory $\HPath + \coeT_0$ can be interpreted in $T$, then we can define a map $s : P(X) \to P(X)$ such that $p_0 \circ s = p_1$ and $p_1 \circ s = p_0$.
If $a \in P(X)_{(p,n)}$ is such that $x : I, \Gamma \vdash a$, then define $s(a)$ as $x : I, \Gamma[x \repl \inv(x)] \vdash a[x \repl \inv(x)]$, where
\[ \inv(i) = \at(\rightI, \leftI, \coe_0(x.\,x \idtype \leftI, \refl(\leftI)), i). \]

Now, let us prove some of the conditions of \rthm{model-structures}.
\begin{lem}[Jtm]
The map $\langle p_0, p_1 \rangle : P(X) \to X \times X$ have RLP with respect to $\J_{\I_{tm}}$.
\end{lem}
\begin{proof}
We are given a type $x : I, \Delta \vdash A\ \type$ and terms $x : I, \Delta \vdash f_1 : A$, $\Delta[x \repl \leftI], y : I \vdash f_0 : A[x \repl \leftI]$ and $\Delta[x \repl \rightI], y : I \vdash f_2 : A[x \repl \rightI]$,
and we need to find a term $t$ that satisfies $x : I, \Delta, y : I \vdash t : A$, $t[y \repl \leftI] = f_1$, $t[x \repl \leftI] = f_0$ and $t[x \repl \rightI] = f_2$.
Thus, $t$ is just a local two-dimensional filler.
We cannot construct such fillers in general, but we can do it in our case since $A$ depends only on one of the coordinates.
Thus, the construction will be similar to the construction of $\coe^l_1$.

Let $\Delta$ be equal to $z_1 : B_1, \ldots z_k : B_k$.
Then to construct a term $t$, we just need for every $\vdash i : I$, $\vdash j : I$ and $\vdash b_1 : B_1[x \repl i]$, \ldots $\vdash b_k : B_k[x \repl i, z_1 \repl b_1, \ldots z_{k-1} \repl b_{k-1}]$,
to find a term $t'(i, j, b_1, \ldots b_k)$ such that $\vdash t'(i, j, b_1, \ldots b_k) : A[x \repl i, y_1 \repl b_1, \ldots y_k \repl b_k]$, $t'(i, \leftI, b_1, \ldots b_k) = f_1[x \repl i, y_1 \repl b_1, \ldots y_k \repl b_k]$,
$t'(\leftI, j, b_1, \ldots b_k) = f_0[y \repl j, y_1 \repl b_1, \ldots y_k \repl b_k]$ and $t'(\rightI, j, b_1, \ldots b_k) = f_2[y \repl j, y_1 \repl b_1, \ldots y_k \repl b_k]$.
Thus, $t'$ is an analog of $\coe^{l'}_1$.

First, let $b'_m(w)$ be equal to
\[ \coe_2(x.\,B_m[y_1 \repl b_1'(x), \ldots y_{m-1} \repl b_{m-1}'(x)], i, b_m, w) \]
Then the following conditions are satisfied:
\begin{align*}
& \vdash b'_m(w) : B_m[x \repl w, z_1 \repl b'_1(w), \ldots z_{m-1} \repl b'_{m-1}(w)] \\
x : I & \vdash f_1[\overline{z} \repl \overline{b'(x)}] : A[\overline{z} \repl \overline{b'(x)}] \\
y : I & \vdash f_0[\overline{z} \repl \overline{b'(\leftI)}] : A[x \repl \leftI, \overline{z} \repl \overline{b'(\leftI)}] \\
y : I & \vdash f_2[\overline{z} \repl \overline{b'(\rightI)}] : A[x \repl \rightI, \overline{z} \repl \overline{b'(\rightI)}]
\end{align*}
\end{proof}

If our theory has some additional structure (local fillers for types),
then we can prove that maps $\langle p_0, p_1 \rangle : P(X) \to X \times X$ have RLP with respect to $\J_{\I_{ty}}$, but we cannot do this in general.
Hence, we will use the second option and will prove that objects of the form $F(\{\,\Delta : (ctx,n)\,\})$ have LLP up to $\sim^{r*}$ with respect to $\Jcell[_\I]$.

\begin{lem}[Jty]
Pushouts of maps from $\J'_{\I_{ty}}$ have RLP up to $\sim^r$ with respect to objects of the form $F(\{\,\Delta : (ctx,n)\,\})$.
\end{lem}
\begin{proof}
Maps from $F(\{\,\Delta : (ctx,n)\,\})$ to $Y$ may be identified with elements of $Y_{(ctx,n)}$.
Since $Y$ is a pushout $X \amalg_{F(\{\,\Gamma \vdash A\ \type\,\})} F(\{\,\Gamma, x : I \vdash H\ \type\,\})$,
its elements can be described as closed terms of the theory
$T' = \Lang(X) \cup \{\,\sststile{}{} (\Gamma, x : I \vdash H\ \type) \land (\Gamma \vdash O_{u(A)} \deq H[\leftI])\,\}$,
where $u$ is the map $F(\{\,\Gamma \vdash A\ \type\,\}) \to X$.

For every set of variables $V$ and every term $t$ of sort $(p,n)$ with free variables in $V$,
we construct a term $h(t)$ of sort $(p,n+1)$ with free variables in $L(V) = \{\,x : (p,k+1)\ |\ (x : (p,k)) \in V\,\}$.
\begin{align*}
h(x) & = x \text{, if } x \in V \\
h(O_a) & = x : I, z_1 : B_1, \ldots z_n : B_n \vdash O_a \text{, if } z_1 : B_1, \ldots z_n : B_n \vdash O_a \\
h(\emptyCtx) & = I \\
h(\sigma_n(\Gamma, t_1, \ldots t_k)) & = \sigma_{n+1}(h(\Gamma), h(t_1), \ldots h(t_k)) \\
h(H) & = y : I, \Gamma, x : I \vdash H[x \repl \sq(y, x)]
\end{align*}

For every formula $\varphi$ with free variables in $V$, we can define formula $h(\varphi)$ with free variables in $L(V)$ as follows:
\begin{align*}
h(t_1 = t_2) & = (h(t_1) = h(t_2)) \\
h(R_n(\Gamma, t_1, \ldots t_k)) & = R_{n+1}(h(\Gamma), h(t_1), \ldots h(t_k)) \\
h(\varphi_1 \land \ldots \land \varphi_n) & = h(\varphi_1) \land \ldots \land h(\varphi_n)
\end{align*}
It is easy to see that $h$ is stable under substitution.
Thus to prove that for every theorem $\varphi \sststile{}{V} \psi$ of $T'$, sequent $h(\varphi) \land \bigwedge_{x \in L(V)} ctx^n(x) = I \sststile{}{L(V)} h(\psi)$
is also a theorem of $T'$, it is enough to show that this is true for the axioms.
If a formula $\varphi$ does not mention $H$, then $h(\varphi)$ coincides with the lifting of $\varphi$.
Hence, if a sequent $\varphi \sststile{}{V} \psi$ does not use $H$, then $h(\varphi) \sststile{}{L(V)} h(\psi)$ is a theorem by the stability.
The only axiom that mentions $H$ is $\sststile{}{} (\Gamma, x : I \vdash H\ \type) \land (\Gamma \vdash O_{u(A)} \deq H[\leftI])$.
It is easy to see that the application of $h$ to this axiom gives us a theorem.

If $t$ is closed term, then $h(t)$ is also closed.
Thus for every element $t \in Y_{(p,n)}$, we defined an element $h(t) \in Y_{(p,n+1)}$ such that $ctx^n(h(t)) = I$.
Thus $h(t)$ defines an element of $P(Y)_{(p,n)}$.
Moreover, $p_1 \circ h(t) = t$ and $p_0 \circ h(t)$ factors through $X$,
which shows that $X \to Y$ has RLP up to $\sim^r$ with respect to objects of the form $F(\{\,\Delta : (p,n)\,\})$.
\end{proof}

\begin{lem}[Jhom]
Let $u : F(\{\,\Gamma \vdash A\ \type\,\}) \to X$ be a map.
Let $Y = X \amalg_{F(\{ \Gamma \vdash A\ \type \})} C_{(ty,n)}$ and $Y' = X \amalg_{F(\{ \Gamma \vdash A\ \type \})} C'_{(ty,n)}$.
Then there exist maps $v : Y \to Y'$ and $v' : Y' \to Y$ such that $v' \circ v \sim^r \id_Y$.
\end{lem}
\begin{proof}
The maps $\varphi$ and $\psi$ that were defined in subsection~\ref{sec:univalence} induce maps $C_{(ty,n)} \to C'_{(ty,n)}$ and $C'_{(ty,n)} \to C_{(ty,n)}$, which induce maps $v$ and $v'$.
We can define a homotopy $h' : Y \to P(Y)$ between $v' \circ v$ and $\id_Y$ as follows.
For every $x \in X_{(p,k)}$ such that $\Gamma \vdash x$, let $h'(x) = (i : I, \Gamma \vdash x)$.
For every symbol $x$ of $\Eq$, let $h'(x) = (i : I, \Delta \vdash \subst(h(x), v_{n-1}, \ldots v_0, v_n))$, where $h$ is a homotopy constructed in \rlem{UA}.
Note that $h'(A) = (i : I, \Delta \vdash A)$, so $h'$ is a well-defined map by the universal property of pushouts.
\end{proof}

Now, we can complete the construction of the model structure:
\begin{thm}[main]
For every $I$-stable theory $T$ in which the theory $\coeT_1 + \sigma + \PathT + \wUA$ can be interpreted,
sets $\I$ and $\J_\I$ and functor $P : \Mod{T} \to \Mod{T}$ satisfy conditions of \rthm{model-structures}.
\end{thm}
\begin{proof}
First, let us prove that $p_0 : P(X) \to X$ has RLP with respect to $\I$.
Indeed, given a type $i : I, \Delta \vdash H$ and a term $\Delta[i \repl \leftI] \vdash a : H[i \repl \leftI]$ in $X$,
we need to find a term $i : I, \Delta \vdash h : H$ such that $h[i \repl \leftI] = a$.
We can define $h$ as $\Fill^1_{(tm,1+n)}(H, a, i)$.
Given a context $j : I, \Delta$, where $\Delta = (x_1 : B_1, \ldots x_n : B_n)$, and a type $\Delta[j \repl \leftI] \vdash A$,
we need to find a type $j : I, \Delta \vdash H$ such that $\Delta[j \repl \leftI] \vdash H[j \repl \leftI] \deq A$.
We can define $H$ as $j : I, \Delta \vdash A[x_1 \repl b_1, \ldots x_n \repl b_n)$, where $b_i = \coe^l_2(j.\,B_i, j, x_i, \leftI)$.

To prove the last condition, note that objects of the form $F(\{\,\Gamma : (ctx,n)\,\})$ are finite.
Thus it is enough to prove that they have LLP up to $\sim^{r*}$ with respect to pushouts of maps in $\J_\I$.
For pushouts of maps from $\J_{\I_{tm}}$, this follows from \rlem{Jtm}.
Let $f : X \to Y$ be a pushout of a map in $\J_{\I_{ty}}$ along a map $u : V \to X$ and let $f' : X \to Y'$ be the pushout of the corresponding map from $\J'_{\I_{ty}}$ along $u$.
Then \rlem{Jty} implies that for every $t : F(\{\,\Gamma : (ctx,n)\,\}) \to Y$, there exists a map $t' : F(\{\,\Gamma : (ctx,n)\,\}) \to X$ such that $f' \circ t' \sim^r v \circ t$.
By \rlem{Jhom}, $t \sim^r v' \circ v \circ t \sim^r v' \circ f' \circ t' = f \circ t'$.
Thus $t'$ is the required lifting.
\end{proof}

\subsection{Theories with sigma types}
\label{sec:sigma}

In this section we give several equivalent descriptions of weak equivalences between models of theories with $\Sigma$-types.
We also discuss the relationship between such models and fibration categories.

Recall that the theory of $\Sigma$-types with eta has the following rules:
\medskip
\begin{center}
\AxiomC{$\Gamma, x : A \vdash B\ \type$}
\UnaryInfC{$\Gamma \vdash \Sigma(A, B)\ \type$}
\DisplayProof
\quad
\AxiomC{$\Gamma, x : A \vdash B\ \type$}
\AxiomC{$\Gamma \vdash a : A$}
\AxiomC{$\Gamma \vdash b : B[x \repl a]$}
\TrinaryInfC{$\Gamma \vdash \pair(A, B, a, b) : \Sigma(A, B)$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash p : \Sigma(A, B)$}
\UnaryInfC{$\Gamma \vdash \pi_1(A, B, p) : A$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash p : \Sigma(A, B)$}
\UnaryInfC{$\Gamma \vdash \pi_2(A, B, p) : B[x \repl \pi_1(A, B, p)]$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : A \vdash B\ \type$}
\AxiomC{$\Gamma \vdash a : A$}
\AxiomC{$\Gamma \vdash b : B[x \repl a]$}
\TrinaryInfC{$\Gamma \vdash \pi_1(A, B, \pair(A, B, a, b)) \deq a$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : A \vdash B\ \type$}
\AxiomC{$\Gamma \vdash a : A$}
\AxiomC{$\Gamma \vdash b : B[x \repl a]$}
\TrinaryInfC{$\Gamma \vdash \pi_2(A, B, \pair(A, B, a, b)) \deq b$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash p : \Sigma(A, B)$}
\UnaryInfC{$\Gamma \vdash \pair(A, B, \pi_1(A, B, p), \pi_2(A, B, p)) \deq p$}
\DisplayProof
\end{center}
We will usually omit first two arguments to $\pair$, $\pi_1$ and $\pi_2$.

If $T$ has $\Sigma$-types and $X$ is a model of $T$, then every nonempty context of $X$ is isomorphic to a context of length 1.
Indeed, for every $(x_1 : A_1, \ldots x_n : A_n \vdash) \in X_{(ctx,n)}$, we define $\Sigma(A_1, \ldots A_n) \in X_{(ty,0)}$ as $\Sigma(A_1, x_1.\,\ldots \Sigma(A_{n-1}, x_{n-1}.\,A_n))$.
We define context morphisms between $\Gamma$ and $\Sigma(\Gamma)$ as follows:
$c : \Gamma \to \Sigma(\Gamma)$ is $\pair(v_{n-1}, \ldots \pair(v_1,v_0), \ldots))$ and $d : \Sigma(\Gamma) \to \Gamma$ is $b_0, \ldots b_{n-1}$,
where $b_{n-1} = \pi_2(\ldots \pi_2(v_0) \ldots )$, where $\pi_2$ is repeated $n-1$ times, and
for every $0 \leq i < n-1$, $b_i = \pi_1(\pi_2(\ldots \pi_2(v_0) \ldots ))$, where $\pi_2$ is repeated $i$ times,
It is easy to see that $c$ and $d$ are mutually inverse.
If $f : \Delta \to \Gamma$ is a morphism of contexts and $\Gamma \vdash A$, then we have a term $\Delta \vdash f^*(A)$ (using the notation of contextual categories).
If $f = (b_1, \ldots b_n)$, then it can be defined as follows: $f^*(A) = \subst(\Delta, A, b_1, \ldots b_n)$.

\begin{prop}[sigma-we-i]
Let $T$ be a theory in which the theory $\coeT_1 + \sigma + \PathT + \wUA + \Sigma$ can be interpreted.
Then a map between models of $T$ is a weak equivalence if and only if it has RLP up to $\sim_i$ with respect to $i = i_{(ty,0)}$ and $i = i_{(tm,1)}$.
\end{prop}
\begin{proof}
Since $i_{(ty,0)},i_{(tm,1)} \in \I$, the ``only if'' direction is obvious.
Let us prove the converse.
Let $f : X \to Y$ be a map which has RLP up to $\sim_{i_{(tm,1)}}$ with respect to $i_{(tm,1)}$.
Let $A \in X_{(ty,n)}$ and $a \in Y_{(tm,n)}$ be such that $ty(a) = f(A)$.
If $n = 0$, then there exist terms $x : I \vdash a' : A$ and $x : I \vdash p : f(a') \idtype a$.
Then $\vdash a'[\leftI] : A$ and $\vdash p[\leftI] : f(a'[\leftI]) \idtype a$.
If $n > 0$, then there exist terms $z : \Sigma(\Gamma) \vdash a' : d^*(A)$ and $z : f(\Sigma(\Gamma)) \vdash p : f(a') \idtype d^*(a)$.
Then $\Gamma \vdash c^*(a') : A$ and $f(\Gamma) \vdash c^*(p) : f(c^*(a')) \idtype a$.
Thus $f$ has RLP up to $\sim_i$ with respect to every $i \in \I_{tm}$.

Now, suppose that $f$ also has RLP up to $\sim_{i_{(ty,0)}}$ with respect to $i_{(ty,0)}$.
Factor $f$ into a trivial cofibration $g$ followed by a fibration $f'$.
By \cite[lemma~3.4]{f-model-structures}, $f'$ has the same right lifting properties as $f$.
If we can prove that $f'$ is a weak equivalence, then $f$ is a weak equivalence as well by 2-out-of-3 property.
Thus we may assume that $f$ is a fibration.
Then $f$ has RLP with respect to $i_{(ty,0)}$ and $i_{(tm,1)}$.

Let $\Gamma \in X_{(ctx,n)}$ and $A \in Y_{(ty,n)}$ be such that $f(\Gamma) \vdash A$.
Then there exists a type $A' \in X_{(ty,0)}$ such that $f(A') = \Sigma(\Sigma(\Gamma), d^*(A))$.
There exists a term $y : A' \vdash a : \Sigma(\Gamma)$ such that $f(a) = \pi_1(y)$.
Now, consider the type $z : \Sigma(\Gamma) \vdash A''$ which is defined as $\Sigma(A', y.\,a \idtype z)$.

Let us prove that there is an equivalence between $f(A'')$ and $d^*(A)$ in the context $y : \Sigma(f(\Gamma))$.
Actually, this is a well-known fact.
For example, it follows from \cite[lemmas 3.11.8 and 3.11.9]{hottbook}.
But since we are working in a restricted context (we do not have $\Pi$-types), we will give a direct proof.

To simplify the notation, let $B = \Sigma(f(\Gamma))$ and $C(t) = d^*(A)[y \repl t]$.
A map from $f(A'')$ to $d^*(A)$ is a term $g$ which satisfies
\[ y : B, w : \Sigma(\Sigma(B, z.\,C(z)), x.\,\pi_1(x) \idtype y) \vdash g : C(y). \]
Let $t(i) = \coe_1(i.\,C(\at(\pi_2(w),i)), \pi_2(\pi_1(w)), i)$.
Then we can define a map $g$ from $f(A'')$ to $d^*(A)$ as $t(\rightI)$.

A map from $d^*(A)$ to $f(A'')$ is a term $g'$ which satisfies
\[ y : B, c : C(y) \vdash g' : \Sigma(\Sigma(B, z.\,C(z)), x.\,\pi_1(x) \idtype y). \]
We can define such map $g'$ as $\pair(\pair(y,c),\refl(y))$.
Then $g[g'] = c$ and we can construct a path between $g'[g]$ and $w$ as follows:
\[ \pathI(i.\,\pair(\pair(\at(\pi_2(w),i), t(i)), \pathI(j.\,\at(\pi_2(w),\sq_r(i,j))))) \]

Thus $g$ and $g'$ define an equivalence between $f(A'')$ and $d^*(A)$.
Then $c^*(g)$ and $c^*(g')$ define an equivalence between $f(c^*(A''))$ and $A$.
Thus $\Gamma \vdash c^*(A'')$ is the required lift of $A$.
\end{proof}

If $T$ has homogeneous path types, then for every model $X$ of $T$ we can define its homotopy category $\Ho(X)$.
To define it, we need to introduce an equivalence relation on the set of terms.
We will say that terms $a,a' \in X_{(tm,n)}$ are equivalent if $ty(a) = ty(a')$ and there exists a term $p$ such that $ctx^0(a) \vdash p : a \idtype a'$.
Objects of $\Ho(X)$ are closed types (that is, elements of $X_{(ty,0)}$).
For every $A,B \in X_{(ty,0)}$, morphisms from $A$ to $B$ are equivalence classes of terms $b \in X_{(tm,1)}$ such that $x : A \vdash b : B$.
The identity morphism is $x : A \vdash x : A$ and the composition of $b : A \to B$ and $c : B \to C$ is $c[x \repl b]$.
If $x : A \vdash p : b \idtype b'$ and $y : B \vdash q : c \idtype c'$, then $x : A \vdash \pathI(i.\,\at(c,c',q,i)[y \repl \at(b,b',p,i)]) : c[y \repl b] \idtype c'[y \repl b']$.
Thus the composition is well-defined.

For every morphism $f : X \to Y$ of models of $T$, we define a functor $\Ho(f) : \Ho(X) \to \Ho(Y)$ in the obvious way:
$\Ho(f)(A) = f(A)$ for every object $A$, and $\Ho(f)(b) = f(b)$ for every morphism $b$.
It is obvious that $\Ho$ preserves identity morphisms and the composition.
Thus $\Ho$ is a functor $\Mod{T} \to \cat{Cat}$.

If $T$ has $\Sigma$-types, then there is an equivalent characterization of weak equivalences in terms of the homotopy category.
This proposition is similar to \cite[Th\'eor\`eme 3.25]{cis10b}.
Actually, we can probably derive it from results of \cite{cis10b}, but it is easier to give a direct proof.

\begin{prop}[sigma-we-ho]
Let $T$ be a theory in which the theory $\coeT_1 + \sigma + \PathT + \wUA + \Sigma$ can be interpreted, and let $f : X \to Y$ be a morphism of models of $T$.
Then a map $f : X \to Y$ between models of $T$ is a weak equivalence if and only if $\Ho(f)$ is an equivalence of categories.
\end{prop}
\begin{proof}
Note that $\Ho(f)$ is essentially surjective on objects if and only if $f$ has RLP up to $\sim_{i_{(ty,0)}}$ with respect to $i_{(ty,0)}$.

Assume that $f$ is a weak equivalence.
Let $A$ and $B$ be objects of $\Ho(X)$, and let $x : f(A) \vdash b : f(B)$ be a morphism of $\Ho(Y)$.
Then there exists a term $x : A \vdash b' : B$ such that $f(b')$ and $b$ are homotopic.
Hence, $f(b')$ and $b$ are equals as morphisms of $\Ho(Y)$; so $\Ho(f)$ is full.
Let $b$ and $b'$ be terms such that $x : A \vdash b : B$ and $x : A \vdash b' : B$ and there exists a term $p$ such that $x : f(A) \vdash p : f(b) \idtype f(b')$.
Then there exists a term $p'$ such that $x : A \vdash p' : b \idtype b'$.
Hence, $\Ho(f)$ is faithful.

Now, assume that $\Ho(f)$ is an equivalence of categories.
By \rprop{sigma-we-i}, we just need to prove that $f$ has RLP up to $\sim_{i_{(tm,1)}}$ with respect to $i_{(tm,1)}$.
Factor $f$ intro a trivial cofibration $g$ followed by a fibration $f'$.
Since $\Ho(g)$ is an equivalence, $f'$ is also an equivalence by 2-out-of-3 property.
If we can prove that $f'$ is a weak equivalence, then $f$ is a weak equivalence as well by 2-out-of-3 property.
Thus we may assume that $f$ is a fibration.

Let $x : A \vdash B$ be a type in $X_{(ty,1)}$, and let $b$ be a term in $Y_{(tm,1)}$ such that $x : f(A) \vdash b : f(B)$.
Since $\Ho(f)$ is full, there exists a term $x : A \vdash b' : \Sigma(A,B)$ such that $f(b')$ is homotopic to $\pair(x,b)$.
Since $f$ is a fibration, we can assume that $f(b') = \pair(x,b)$.
We need to find a term $s$ such that $x : A \vdash s : \pi_1(b') \idtype x$ and $f(s)$ is homotopic to $\refl(x)$.
If such a term exists, then since $f$ is a fibration, there exists a term $s'$ such that $x : A \vdash s' : \pi_1(b') \idtype x$ and $f(s') = \refl(x)$.
Then we can define $x : A \vdash b'' : B$ as $\coe_0(i.\,B[x \repl \at(s',i)], \pi_2(b'))$.
This $b''$ is the required lift since $f(b'') = b$.

It is easy to find a term $s$ which satisfies the first condition using the fact that $\Ho(f)$ is faithful, but the second condition is more difficult.
Let us show how to construct a term which satisfies both of them.
Since $\Ho(f)$ is full, there exists a term $x : A \vdash s' : \Sigma(A, x.\,\pi_1(b') \idtype x)$ such that $f(s')$ is homotopic to $\pair(x, \refl(x))$.
Since $f$ is a fibration, we can assume that $f(s') = \pair(x, \refl(x))$.
Since $\Ho(f)$ is faithful and $f(\pi_1 \circ s') = f(x)$, there exists a term $h$ such that $x : A \vdash h : \pi_1(s') \idtype x$.
Let $t(i) = \coe_1(j.\,\pi_1(b')[x \repl \at(h,j)] \idtype \at(h,j), \pi_2(s'), i)$.
If we define $s$ as $t(\rightI)$, then $x : A \vdash s : \pi_1(b') \idtype x$.

Let us prove that $f(s)$ is homotopic to $\refl(x)$.
If we define $h'$ as
\[ \pathI(i.\,\pair(\at(h,i), t(i))), \]
then $x : A \vdash h' : s' \idtype \pair(x,s)$.
Hence, we have the following homotopy:
\[ x : f(A) \vdash f(h') : \pair(x, \refl(x)) \idtype \pair(x, f(s)). \]
If we have $\Gamma \vdash p : \Sigma(A, x.\,x \idtype x)$ and $\Gamma \vdash p' : \Sigma(A, x.\,x \idtype x)$ and $\Gamma \vdash h : p \idtype p'$,
then it is easy to see that there exist terms $\Gamma \vdash q_1 : \pi_1(p) \idtype \pi_1(p')$ and $\Gamma \vdash q_2 : \sym(q_1) * \pi_2(p) * q_1 \idtype \pi_2(p')$.
If we take $p = \pair(x, \refl(x))$, $p' = \pair(x, f(s))$ and $h = f(h')$, then $x : f(A) \vdash q_2 : \sym(q_1) * q_1 \idtype f(s)$,
which implies that $f(s)$ is homotopic to $\refl(x)$.
\end{proof}

Let $T_\Sigma = \coeT_1 + \sigma + \PathT + \wUA + \Sigma$.
Every model of $T_\Sigma$ carries the structure of a fibration category, which was proved in \cite{tt-fibr-cat}.
Let us briefly describe this construction.
If $X$ is a model of $T_\Sigma$, then we define category $U(X)$, which has contexts (that is, elements of $X_{(ctx,n)}$) as objects and context morphisms as morphisms.
A map $f : A \to B$ is a fibration if and only if it is isomorphic over $B$ to a map of the form $\pi_1 : \Sigma(B, x.\,C) \to B$.
Weak equivalences of $U(X)$ are homotopy equivalences.

The homotopy category $\Ho(X)$ is equivalent to the localization of $U(X)$ with respect to homotopy equivalences.
Indeed, first note that since we have $\Sigma$-types, $U(X)$ is equivalent to its full subcategory on contexts of length $\leq 1$.
Let $\Ho'(X)$ be the category which has contexts of length $\leq 1$ as objects,
and morphisms of $\Ho'(X)$ are equivalence classes of maps of $U(X)$ with respect to the homotopy relation.
Then $\Ho'(X)$ is equivalent to the localization of $U(X)$, which can be proved as usual (see, for example, \cite[Corollary~1.2.9]{hovey}).
Then $\Ho(X)$ is a full subcategory of $\Ho'(X)$.
The only object that $\Ho(X)$ lacks is the empty context.
But it contains the interval type which is isomorphic to the empty context in the homotopy category
(both of them are terminal objects in $\Ho'(X)$), so $\Ho(X)$ is equivalent to $\Ho'(X)$.

Thus, \rprop{sigma-we-ho} implies that a map $f : X \to Y$ of models is a weak equivalence if and only if
corresponding map $U(f)$ of fibration categories is a weak equivalence.

\section{Final remarks}

In this paper, we defined a model structure on the category of models of a dependent type theory.
We gave a characterization of weak equivalences in terms of homotopy categories of models.
We believe that this model structure is a useful tool in the search for a proof of \rconj{main}.

\begin{thebibliography}{}
\bibitem[Avigad \emph{et al.} 2015]{tt-fibr-cat}
J.~{Avigad}, K.~{Kapulkin}, and P.~L.~{Lumsdaine}, \emph{Homotopy
  limits in type theory}, Mathematical Structures in Computer Science
  \textbf{25} (2015), Special issue 05, 1040--1070.

\bibitem[Cartmell 1986]{GAT}
J.~{Cartmell}, \emph{Generalised algebraic theories and contextual categories},
  Annals of Pure and Applied Logic \textbf{32} (1986), 209 -- 243.

\bibitem[Cisinski 2010]{cis10b}
D.-C.~{Cisinski}, \emph{Invariance de la {K-Th\'eorie} par \'equivalences
  d\'eriv\'ees}, Journal of K-theory: K-theory and its Applications to Algebra,
  Geometry, and Topology \textbf{6} (2010), iss.~03, 505--546.

\bibitem[Clairambault and Dybjer 2011]{ext-eq}
P.~{Clairambault} and P.~{Dybjer}, \emph{The biequivalence of locally
  Cartesian closed categories and Martin-L{\"o}f type theories}, pp.~91--106,
  Springer Berlin Heidelberg, Berlin, Heidelberg, 2011.

\bibitem[Dybjer 1996]{cwf}
P.~{Dybjer}, \emph{Internal type theory}, pp.~120--134, Springer Berlin
  Heidelberg, Berlin, Heidelberg, 1996.

\bibitem[Hovey 1999]{hovey}
M.~{Hovey}, \emph{Model categories}, Mathematical Surveys and Monographs,
  American Mathematical Society, 1999.

\bibitem[Isaev 2013]{f-model-structures}
V.~{Isaev}, \emph{On fibrant objects in model categories}, unpublished, (2013),
  \href {http://arxiv.org/abs/1312.4327} {\path{arXiv:1312.4327}}.

\bibitem[Isaev 2016]{alg-tt}
V.~{Isaev}, \emph{{Algebraic Presentations of Dependent Type Theories}},
  unpublished, (2016), \href {http://arxiv.org/abs/1602.08504} {\path{arXiv:1602.08504}}.

\bibitem[Kapulkin 2015]{kapulkin}
C.~{Kapulkin}, \emph{{Locally Cartesian Closed Quasicategories from Type
  Theory}}, unpublished, (2015), \href {http://arxiv.org/abs/1507.02648}
  {\path{arXiv:1507.02648}}.

\bibitem[Lumsdaine and Warren 2015]{local-universes}
P.~L.~{Lumsdaine} and M.~A.~{Warren}, \emph{The local universes model:
  An overlooked coherence construction for dependent type theories}, ACM Trans.
  Comput. Logic \textbf{16} (2015), no.~3, 23:1--23:31.

\bibitem[Palmgren and Vickers 2007]{PHL}
E.~{Palmgren} and S.~J.~{Vickers}, \emph{Partial horn logic and Cartesian
  categories}, Annals of Pure and Applied Logic \textbf{145} (2007), no.~3, 314
  -- 353.

\bibitem[Pitts 2000]{pitts}
A.~M.~{Pitts}, \emph{Categorical logic}, Handbook of Logic in Computer Science,
  Volume 5. Algebraic and Logical Structures (S.~Abramsky, D.~M. Gabbay, and
  T.~S.~E. Maibaum, eds.), Oxford University Press, 2000, pp.~39--128.

\bibitem[Shulman 2012]{shul-inv}
M.~{Shulman}, \emph{Univalence for inverse diagrams and homotopy
  canonicity}, Mathematical Structures in Computer Science \textbf{25} (2015),
  Special issue 05, 1203--1277.

\bibitem[Szumi{\l}o 2014]{szumilo}
K.~{Szumi{\l}o}, \emph{{Two Models for the Homotopy Theory of Cocomplete
  Homotopy Theories}}, Ph.D. thesis, University of Bonn, (2014)

\bibitem[The {Univalent Foundations Program} 2013]{hottbook}
The {Univalent Foundations Program}, \emph{Homotopy type theory: Univalent
  foundations of mathematics}, \url{https://homotopytypetheory.org/book},
  Institute for Advanced Study, 2013.

\bibitem[Kapulkin and Lumsdaine 2016]{kap-lum-model}
C.~{Kapulkin} and P.~L.~{Lumsdaine}, \emph{{The homotopy theory of type
  theories}}, unpublished, (2016), \href {http://arxiv.org/abs/1610.00037}
  {\path{arXiv:1610.00037}}.

\bibitem[Voevodsky 2014]{b-systems}
V.~{Voevodsky}, \emph{{B-systems}}, unpublished, (2014), \href
  {http://arxiv.org/abs/1410.5389} {\path{arXiv:1410.5389}}.
\end{thebibliography}

\end{document}