hotti-local-models.tex

\documentclass{amsart}

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

\hypersetup{colorlinks=true,linkcolor=blue}

\newcommand{\axlabel}[1]{(#1) \phantomsection \label{ax:#1}}
\newcommand{\axtag}[1]{\label{ax:#1} \tag{#1}}
\newcommand{\axref}[1]{(\hyperref[ax:#1]{#1})}

\newcommand{\newref}[4][]{
\ifthenelse{\equal{#1}{}}{\newtheorem{h#2}[hthm]{#4}}{\newtheorem{h#2}{#4}[#1]}
\expandafter\newcommand\csname r#2\endcsname[1]{#3~\ref{#2:##1}}
\expandafter\newcommand\csname R#2\endcsname[1]{#4~\ref{#2:##1}}
\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}

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

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

\newcommand{\fs}[1]{\mathrm{#1}}
\newcommand{\lcon}{\fs{left}}
\newcommand{\rcon}{\fs{right}}
\newcommand{\Path}{\fs{Path}}
\newcommand{\pcon}{\fs{pcon}}
\newcommand{\I}{\fs{I}}
\newcommand{\coe}{\fs{coe}}
\newcommand{\iso}{\fs{iso}}
\newcommand{\id}{\fs{id}}

\numberwithin{figure}{section}

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

\begin{document}

\title{Models of Homotopy Type Theory with an Interval Type}

\author{Valery Isaev}

\begin{abstract}
In this short note, we construct a class of models of an extension of homotopy type theory, which we call homotopy type theory with an interval type.
\end{abstract}

\maketitle

\section{Introduction}

Homotopy type theory with an interval type (HoTT-I) is a simple extension of the ordinarry homotopy type theory, which is implemented in Arend proof assistant.
Instead of identity types, HoTT-I has the interval type and path types defined as certain functions from it.
The theory is similar to cubical type theory \cite{cubical-tt}, but it does not satisfy the canonicity property.

In this note, we will show that (a basic version) HoTT-I can be interpreted in any right proper Cartesian model category in which cofibrations are precisely monomorphisms and which is locally Cartesian closed as a category.
A model category is Cartesian if, for every pair of cofibrations $f : A \to C$ and $g : B \to D$, their pushout-product $f \square g : A \times D \amalg_{A \times C} B \times C \to B \times D$ is a cofibration and is a trivial cofibration whenever one of the maps $f$ and $g$ is.
We let $\mathcal{M}$ be a fixed model category satisfying these properties, which will be used throughout this note.
To interpret some additional constructions of HoTT-I (such as univalent universes), we will later put more restrictions on $\mathcal{M}$.

We will use local universes \cite{local-universes} to solve the coherence issues.
Thus, dependent types in a context $\Gamma$ will be interpreted as diagrams
\[ \xymatrix{                     & E_A \ar@{->>}[d]^{p_A} \\
              \Gamma \ar[r]_{v_A} & V_A,
            } \]
where $p_A$ is a fibration between arbitrary objects and $v_A$ is an arbitrary map.
Terms will be interpreted as sections of $p_A$ over $v_A$.
To simplify the presentation, we will also give the "naive" interpretation for some of the constructions.
In this interpretation, dependent types correspond to fibrations in $\mathcal{M}$ and terms to their sections.

\section{Interval type}

The interval type is just the unit type with two constructors: $\lcon$ and $\rcon$.
The eliminator for it is the same as for the unit type and will be denoted by $\coe$:

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \I$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \lcon : \I$}
\DisplayProof
\quad
\AxiomC{$\Gamma \vdash$}
\UnaryInfC{$\Gamma \vdash \rcon : \I$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : \I \vdash A$}
\AxiomC{$\Gamma \vdash a : A[x := \lcon]$}
\AxiomC{$\Gamma \vdash i : \I$}
\TrinaryInfC{$\Gamma \vdash \coe(x. A, a, i) : A[x := i]$}
\DisplayProof
\end{center}

\[ \coe(x. A, a, \lcon) \equiv a \]

The interval type can be interpreted as the terminal object, but this will give us a model satisfying the K axiom.
To get a homotopic model, we will interpret $\I$ as an interval object.
Let $1 \amalg 1 \to \I \to 1$ be a factorization of the map $1 \amalg 1 \to 1$ into a cofibration $[\lcon,\rcon]$ followed by a trivial fibration.
If $\Gamma$ is any object of $\mathcal{M}$, we will also denote by $\lcon$ and $\rcon$ the maps $\langle \id, \lcon \circ !_\Gamma \rangle : \Gamma \to \Gamma \times \I$ and $\langle \id, \rcon \circ !_\Gamma \rangle : \Gamma \to \Gamma \times \I$, respectively.

Let us describe the naive interpretation of $\coe$.
Let $p_A : A \to \Gamma \times A$ be a fibration, let $a : \Gamma \to A$ be a section of $p_A$ over $\lcon : \Gamma \to \Gamma \times \I$, and let $i : \Gamma \to \I$ be any map.
Since $\lcon : 1 \to 1 \amalg 1$ is a trivial cofibration, $\mathcal{M}$ is Cartesian, and $\Gamma$ is cofibrant, the map $\lcon : \Gamma \to \Gamma \times \I$ is also a trivial cofibration.
Thus, we have a lift in the following diagram:
\[ \xymatrix{ \Gamma           \ar[r]^a \ar[d]_\lcon      & A \ar[d]^{p_A} \\
              \Gamma \times \I \ar@{=}[r] \ar@{-->}[ur]^s & \Gamma \times \I
            }\]
The naive interpretation of $\coe(A,a,i)$ is $\Gamma \xrightarrow{\langle \id, i \rangle} \Gamma \times \I \xrightarrow{s} A$.

Now, let us describe the actual interpretation of $\I$ and $\coe$.
Let $E_\I = \I$, $V_\I = 1$, and let $p_\I : \I \to 1$ and $v_\I : \Gamma \to 1$ be the unique maps.
Terms $\lcon$ and $\rcon$ are interpreted as corresponding morphisms.
To describe $\coe(A,a,i)$, consider the following pullback:
\[ \xymatrix{ T \ar[r]^e \ar[d]_d \pb             & E_A \ar[d]^{p_A} \\
              V_A^\I \ar[r]_{\fs{ev} \circ \lcon} & V_A
            } \]
Then $v_A : \Gamma \times \I \to V_A$ and $a : \Gamma \to E_A$ determine a map $c : \Gamma \to T$.
The interpretation of $\coe(A,a,i)$ is $\Gamma \xrightarrow{\langle c, i \rangle} T \times \I \xrightarrow{s} E_A$, where $s$ is a lift in the following diagram:
\[ \xymatrix{ T           \ar[rr]^e \ar[d]_\lcon                  &                                  & E_A \ar[d]^{p_A} \\
              T \times \I \ar[r]_-{d \times \id} \ar@{-->}[urr]^s & V_A^I \times I \ar[r]_-{\fs{ev}} & V_A
            }\]
If $i = \lcon$, then $\langle c, i \rangle$ factors through $e : T \to E_A$, which implies that $\coe$ satisfies the required computational rule.

We will add more computational rules for $\coe$ later.
Thus, we will need to modify the interpretation of $\coe$ to support them.
To do this, we will use the following general construction.
Let $C$ be an object of $\mathcal{M}$, let $f : C \to T$ be a cofibration, and let $g : C \times \I \to E_A$ be a map such that the following diagram commutes:
\[ \xymatrix{ C \ar[rr]^f \ar[d]_\lcon                    &                                    & T \ar[d]^e \\
              C \times \I \ar[rr]^g \ar[d]_{f \times \id} &                                    & E_A \ar[d]^{p_A} \\
              T \times \I \ar[r]_-{d \times \id}          & V_A^\I \times \I \ar[r]_-{\fs{ev}} & V_A
            } \]
Now, consider the following diagram:
\[ \xymatrix{ C \times \I \amalg_C T \ar[rr]^-{[g,e]} \ar[d]_{f \square \lcon} &                                    & E_A \ar[d]^{p_A} \\
              T \times \I \ar[r]_-{d \times \id} \ar@{-->}[urr]^{s'}           & V_A^\I \times \I \ar[r]_-{\fs{ev}} & V_A
            } \]
Conditions on $f$ and $g$ guarantee that the map $[g,e]$ is well-defined and that the diagram above consisting of solid arrows commutes.
Since $f$ is a cofibration and $\lcon$ is a trivial cofibration, $f \square \lcon$ is also a trivial cofibration.
Thus, we have a lift $s'$ in this diagram.
We can interpret $\coe(A,a,i)$ as $\Gamma \xrightarrow{\langle c, i \rangle} T \times \I \xrightarrow{s'} E_A$.
If $c : \Gamma \to T$ factors as $\Gamma \xrightarrow{c'} C \xrightarrow{f} T$, then $\coe(A,a,i)$ equals to $\Gamma \xrightarrow{\langle c', \lcon \rangle} C \times \I \xrightarrow{g} E_A$, which will give us required additional computational rules.

Let $\{ (f_j : C_j \to T, g_j : C_j \times \I \to T) \}_{j \in \{1,2\}}$ be two pairs of maps satisfying the conditions given above.
Suppose that $\mathcal{M}$ is a topos.
Then we can define the union $f : C \to T$ of subobjects $f_1$ and $f_2$ as $C_1 \amalg_{C_0} C_2 \to T$, where $C_0$ is the intersection of $f_1$ and $f_2$.
Since $- \times \I$ commutes with colimits, $(C_1 \amalg_{C_0} C_2) \times \I$ is the pushout $C_1 \times \I \amalg_{C_0 \times \I} C_2 \times \I$.
Thus, we can define the map $g : (C_1 \amalg_{C_0} C_2) \times \I$ determined by $g_1$ and $g_2$ if the following square commutes:
\[ \xymatrix{ C_0 \times \I \ar[r] \ar[d] & C_2 \times \I \ar[d]^{g_2} \\
              C_1 \times \I \ar[r]_{g_1}  & E_A
            } \]

By the universal property of pushouts, $f$ and $g$ satisfy the required conditions.
Thus, we obtained an interpretation of $\coe$ which satisfies computational rules corresponding to both $(f_1,g_1)$ and $(f_2,g_2)$.
That is, if $\mathcal{M}$ is a topos, we can combine two additional comuptational rules for $\coe$ as long as $g_1$ and $g_2$ corresponding to these rules satisfy the condition given above.
More generally, if we have a finite set of additional computational rules for $\coe$, then we just need to check that this condition holds pairwise.

\begin{remark}
Informally, the condition on $g_1$ and $g_2$ simply means that the right hand sides of the corresponding computational rules agree on the intersection of the left hand sides.
\end{remark}

\section{Path types}

Identity types are replaced with path types in HoTT-I:

\medskip
\begin{center}
\AxiomC{$\Gamma, x : \I \vdash A$}
\AxiomC{$\Gamma \vdash a : A[x := \lcon]$}
\AxiomC{$\Gamma \vdash a' : A[x := \rcon]$}
\TrinaryInfC{$\Gamma \vdash \Path(x. A, a, a')$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma, x : I \vdash a : A$}
\UnaryInfC{$\Gamma \vdash \pcon(x. a) : \Path(x. A, a[x := \lcon], a[x := \rcon])$}
\DisplayProof
\end{center}

\medskip
\begin{center}
\AxiomC{$\Gamma \vdash p : \Path(x. A, a, a')$}
\AxiomC{$\Gamma \vdash i : \I$}
\BinaryInfC{$\Gamma \vdash p\ @_{a,a'}\ i : A[x := i]$}
\DisplayProof
\end{center}

\begin{align*}
& \pcon(x. t)\ @_{a,a'}\ i \equiv t[x := i] \\
& \pcon(x. p\ @\ x) \equiv p \text{ if } x \notin \fs{FV}(p) \\
& p\ @_{a,a'}\ \lcon \equiv a \\
& p\ @_{a,a'}\ \rcon \equiv a'
\end{align*}

Let us describe the interpretation of $\Path(A,a,a')$.
We define $V_\Path$ as the following pullback:
\[ \xymatrix{ V_\Path \ar[rr] \ar[d] \pb                                                 & & E_A \times E_A \ar[d]^{p_A \times p_A} \\
              V_A^\I \ar[rr]_-{\langle \fs{ev} \circ \lcon, \fs{ev} \circ \rcon \rangle} & & V_A \times V_A
            } \]
The maps $v_A : \Gamma \times \I \to V_A$ and $a, a' : \Gamma \to E_A$ determine a map $v_\Path : \Gamma \to V_\Path$.
We let $E_\Path = E_A^\I$ and $p_\Path = \langle p_A \circ -, \langle \fs{ev} \circ \lcon, \fs{ev} \circ \rcon \rangle \rangle : E_A^\I \to V_\Path$.

If $a : \Gamma \times \I \to E_A$ is a section of $p_A$ over $v_A$, then we can define $\pcon(a)$ as the map $\Gamma \to E_A^\I$ that corresponds to $a$ via the adjunction.
If $p : \Gamma \to E_\Path$ is a section of $p_\Path$ over $v_\Path$ and $i : \Gamma \to \I$, then we can define the interpretation of $@$ as $\Gamma \xrightarrow{\langle p, i \rangle} E_A^\I \times \I \xrightarrow{\fs{ev}} E_A$.
A straightforward computation shows that all computation rules hold for this interpretation.

The identity type $a =_A a'$ can be defined as $\Path(x. A, a, a')$.
Its constructor $\fs{refl}(a)$ is defined as $\pcon(x. a)$.
The J rule also can be defined \cite[Section~3.1]{alg-models}.
The only problem is that J satisfies its computational rule only propositionally.
To fix this problem, we can add another computational rule for $\coe$:
\[ \coe(x. A, a, i) \equiv a \text{ if } x \notin \fs{FV}(A) \]

To show that this rule can be interpreted in our model, we define two maps $f$ and $g$ as described in the previous section.
Let $f$ be the map $\langle \fs{const} \circ p_A, \id \rangle : E_A \to T$, where $\fs{const} : V_A \to V_A^\I$ is the map corresponding to the projection via the adjunction.
Note that $f$ is a cofibration since $e \circ f = \id$ and monomorphisms are cofibrations.
Let $g : E_A \times \I \to E_A$ be the first projection.
It is easy to see that $f$ and $g$ satisfy the required conditions.
Now, if $x \notin A$, then $v_A : \Gamma \times \I \to V_A$ factors through $\pi_1 : \Gamma \times \I \to \Gamma$.
It follows that the map $c : \Gamma \to T$ defined in the previous section factors through $f : E_A \to T$, which gives us the required computational rule.

\bibliographystyle{amsplain}
\bibliography{ref}

\end{document}