basics.tex

\chapter{Basics of HoTT}
\label{cha:basics}

\section{Basic properties of equality}
\label{sec:equality}


We begin by introducing identity types and the basic notions that follow from them.
For any type $A$, and any $x,y:A$, we have a type $\id[A]{x}{y}$, also written $\idtype[A]{x}{y}$ or just $x=y$.
We can think of inhabitants of $x=y$ as either
\begin{enumerate}
\item proofs that $x$ and $y$ are equal,
\item paths from $x$ to $y$, or
\item isomorphisms/equivalences from $x$ to $y$.
\end{enumerate}
The induction principle for identity types says that if
\begin{itemize}
\item for every $x,y:A$ and every $p:\id[A]xy$ we have a type $D(x,y,p)$, and
\item for every $a:A$ we have an element $d(a):D(a,a,\refl a)$, 
\end{itemize}
then there exists an element $J_{D,d}(x,y,p):D(x,y,p)$ for \emph{every} $x,y:A$ and $p:\id[A]xy$, such that $J_{D,d}(a,a,\refl a) \jdeq d(a)$.
In other words, given dependently typed functions
\begin{align*}
D & :\prod_{x,y:A}\, \prod_{p:\id{x}{y}} \,\type\\
d & :\prod_{a:A} D(a,a,\refl{a})
\end{align*}
there is a dependently typed function
\[J_{D,d}:\prod_{x,y:A} \,\prod_{p:\id{x}{y}} \,D(x,y,p)\]
such that 
\begin{equation}\label{eq:Jconv}
J_{D,d}(a,a,\refl{a})\jdeq d(a)
\end{equation}
for every $a:A$.
The notation $J$ is traditional for this function, but we will not use it very much.
Usually, every time we apply this induction rule we will either not care about the specific function being defined, or we will immediately give it a different name.

As a first application, we can show that equality is symmetric.
In topological language, this means ``paths can be reversed''.

\begin{lem}\label{lem:opp}
  For every type $A$ and every $x,y:A$ there is a function
  \begin{equation*}
    (x= y)\to(y= x)
  \end{equation*}
  denoted $p\mapsto \opp{p}$, such that $\opp{\refl{x}}\jdeq\refl{x}$ for each $x:A$.
\end{lem}
\begin{proof}[First proof]
  Let $D:\prod_{x,y:A} \prod_{p:x= y} \type$ be the dependent type defined by $D(x,y,p)\defeq (y= x)$.
  Then we have
  \begin{equation*}
    d\defeq \lambda x.\refl{x}:\prod_{x:A}\, D(x,x,\refl{x}).
  \end{equation*}
  Thus, $J$ gives us a term $J_{D,d}(x,y,p): (y= x)$ for each $p:(x= y)$.
  Thus, we can define the desired function by $\lambda p. J_{D,d}(x,y,p)$.
  The conversion rule~\eqref{eq:Jconv} gives $\opp{\refl{x}}\jdeq \refl{x}$.
\end{proof}

We have written out this proof in a very formal style, which may be helpful while the induction rule on identity types is unfamiliar.
However, eventually we prefer to use more natural language, such as in the following equivalent proof.

\begin{proof}[Second proof]
  We want to construct, for each $x,y:A$ and $p:x=y$, an element $\opp{p}:y=x$.
  By induction, it suffices to do this in the case when $y$ is $x$ and $p$ is $\refl{x}$.
  But in this case, $y=x$ is $x=y$, so we can take $\opp{\refl{x}}$ to be $\refl{x}$ again.
  The conversion rule follows by definition.
\end{proof}

We will write out the next few proofs in both styles, to help the reader become accustomed to the latter one.
Next we prove the transitivity of equality, or equivalently we ``concatenate paths''.

\begin{lem}\label{lem:concat}
  For every type $A$ and every $x,y,z:A$ there is a function
  \begin{equation*}
    {(-)}\ct{(-)}:(y= z)\to (x= y)\to (x=  z)
  \end{equation*}
  which satisfies $\refl{x}\ct \refl{x}\jdeq \refl{x}$ for any $x:A$.
\end{lem}

\begin{proof}[First proof]
  Let $D:\prod_{y,z:A} \prod_{q:y=z} \type$ be the dependent type defined by
  \begin{equation*}
    D(y,z,q)\coloneqq(x= y)\to (x= z).
  \end{equation*}
  Then we have the dependent function
  \begin{equation*}
    d\coloneqq\lambda y.\idfunc[x= y]:\prod_{y:A}\, D(y,y,\refl{y}),
  \end{equation*}
  where $\idfunc[x= y]$ is the identity function on $x= y$ defined by $\lambda p.p$.
  Now we may apply the induction principle for identity types to obtain
  \[J_{D,d}(y,z,q):(x= y)\to(x= z)\]
  for every $q:y= z$.
  The conversion rule gives us $\refl{y}\ct p\jdeq p$ for any $p:\id[A]xy$, and thus in particular $\refl{x}\ct \refl{x}\jdeq \refl{x}$ for any $x:A$.
\end{proof}

\begin{proof}[Second proof]
  We want to construct, for every $x,y,z:A$ and every $p:x=y$ and $q:y=z$, an element of $x=z$.
  By induction, it suffices to assume that $z$ is $y$ and $q$ is $\refl{y}$.
  But in this case, $x=z$ is $x=y$, so we have $p$.
\end{proof}

In set-level mathematics, symmetry and transitivity of equality are mere propositions, so that the \emph{values} of \autoref{lem:opp} and \autoref{lem:concat} do not matter.
In proof-relevant (or ``homotopical'') mathematics, however, where there can be more than one proof of equality between two elements (i.e.\ more than one path between two points), these values do matter.
We need to know, for instance, that concatenation of paths is \emph{associative}, and that inversion provides \emph{inverses} with respect to concatenation.
That is the purpose of the following lemma.

A noteworthy feature is that these are themselves propositional equalities, living in the identity types of the types $x= y$.
Topologically, they are \emph{paths of paths}, and we are familiar topologically with the idea that concatenating a path with the reversed path only gives a constant path \emph{up to homotopy}, i.e.\ up to a higher path.

\begin{lem}%[The $\omega$-groupoid structure of types]
  Suppose $A$ and $B$ are types, that $x,y,z,w:A$ and that $p:x= y$, $q:y = z$ and $r:z=w$.
  We have the following:
  \begin{enumerate}
  \item $p= p\ct \refl{x}$ and $p = \refl{y} \ct p$.
  \item $\opp{p}\ct p=  \refl{x}$ and $p\ct \opp{p}= \refl{y}$.
  \item $\opp{\opp{p}}= p$.
  \item $r\ct (q\ct p)=  (r\ct q)\ct p$.
  \end{enumerate}
\end{lem}

\begin{proof}
  All the proofs use the induction principle for equalities.
  \begin{enumerate}
  \item \emph{(First proof)} Let $D:\prod_{x,y:A}\prod_{p:x=y} \type$ be the dependent type given by 
    \begin{equation*}
      D(x,y,p)\coloneqq (p= p\ct \refl{x}).
    \end{equation*}
    Then $D(x,x,\refl{x})$ is $\refl{x}=\refl{x}\ct\refl{x}$.
    Since $\refl{x}\ct\refl{x}\jdeq\refl{x}$, it follows that $D(x,x,\refl{x})\jdeq (\refl{x}=\refl{x})$.
    Thus, there is a term
    \begin{equation*}
      d\coloneqq\lambda x.\refl{\refl{x}}:\prod_{x:A} D(x,x,\refl{x}).
    \end{equation*}
    Now $J$ gives a term $J(D,d,p):(p= p\ct\refl{x})$ for each $p:x= y$.
    The other equality is proven similarly.

    \noindent
    \emph{(Second proof)} By induction, it suffices to assume that $y$ is $x$ and that $p$ is $\refl x$.
    But in this case, we have $\refl{x}\ct\refl{x}\jdeq\refl{x}$.
  \item \emph{(First proof)} Let $D:\prod_{x,y:A}\prod_{p:x=y} \type$ be the dependent type given by 
    \begin{equation*}
      D(x,y,p)\coloneqq (\opp{p}\ct p=  \refl{x}).
    \end{equation*}
    Then $D(x,x,\refl{x})$ is $\opp{\refl{x}}\ct\refl{x}=\refl{x}$.
    Since $\opp{\refl{x}}\jdeq\refl{x}$ and $\refl{x}\ct\refl{x}\jdeq\refl{x}$, we get that $D(x,x,\refl{x})\jdeq (\refl{x}=\refl{x})$.
    Hence we find the function
    \begin{equation*}
      d\coloneqq\lambda x.\refl{\refl{x}}:\prod_{x:A} D(x,x,\refl{x}).
    \end{equation*}
    Now $J$ gives a term $J(D,d,p):\opp{p}\ct p=\refl{x}$ for each $p:x= y$ in $A$.
    The other equality is similar.

    \noindent \emph{(Second proof)} By induction, it suffices to assume $p$ is $\refl x$.
    But in this case, we have $\opp{p} \ct p \jdeq \opp{\refl x} \ct \refl x \jdeq \refl x$.
  \item \emph{(First proof)} Let $D:\prod_{x,y:A} \prod_{p:x=y} \type$ be the dependent type given by
    \begin{equation*}
      D(x,y,p)\coloneqq (\opp{\opp{p}}= p).
    \end{equation*}
    Then $D(x,x,\refl{x})$ is $\opp{\opp{\refl x}}=\refl{x}$.
    Since $\opp{\refl{x}}\jdeq \refl{x}$ for each $x:A$, we see that $D(x,x,\refl{x})\jdeq(\refl{x}=\refl{x})$.
    Hence we find the function
    \begin{equation*}
      d\coloneqq\lambda x.\refl{\refl{x}}:\prod_{x:A} D(x,x,\refl{x}).
    \end{equation*}
    Now $J$ gives a term $J(D,d,p):\opp{\opp{p}}= p$ for each $p:x= y$.

    \noindent \emph{(Second proof)} By induction, it suffices to assume $p$ is $\refl x$.
    But in this case, we have $\opp{\opp{p}}\jdeq \opp{\opp{\refl x}} \jdeq \refl x$.
  \item \emph{(First proof)} Let $D:\prod_{z,w:A} \prod_{r:z=w} \type$ be the dependent type given by
    \begin{equation*}
      D(z,w,r)\coloneqq\prod_{x,y:A}\,\prod_{p:x= y}\,\prod_{q:y= z}\, \big(r\ct (q\ct p)=  (r\ct q)\ct p\big).
    \end{equation*}
    Then $D(z,z,\refl{z})$ is
    \begin{equation*}
      \prod_{x,y:A} \,\prod_{q:y= z} \,\prod_{p:x= y}\, \big(\refl{z}\ct(q\ct p)= (\refl{z}\ct q)\ct p\big),
    \end{equation*}
    which simplifies to
    \begin{equation*}
      \prod_{x,y:A}\,\prod_{q:y= z} \,\prod_{p:x= y}\, (q\ct p= q\ct p).
    \end{equation*}
    Therefore, we find
    \begin{equation*}
      d\coloneqq\lambda z.\lambda x,y,p,q.\refl{q\ct p}:\prod_{z:A} D(z,z,\refl{z}).
    \end{equation*}
    Now $J$ gives us an element $J(D,d,r,q,p):r\ct (q\ct p)= (r\ct q)\ct p$ for each $r:z= w$.

    \noindent \emph{(Second proof)} By induction, it suffices to assume $r$ is $\refl z$.
    But in this case, we have
    \[ r\ct (q\ct p) \jdeq \refl{z}\ct(q\ct p) \jdeq q\ct p \jdeq (\refl{z}\ct q)\ct p
    \jdeq (r\ct q)\ct p.\qedhere
    \]
  \end{enumerate}
\end{proof}

Now we wish to establish that functions $f:A\to B$ behave functorially on paths, or equivalently that they respect equality.
Topologically, this can be thought of as saying that every function is ``continuous''.

\begin{lem}\label{lem:map}
  Suppose that $f:A\to B$ is a function and that $p:(\id[A]xy)$. Then there is
  \begin{equation*}
    \map f p : f(x)= f(y)
  \end{equation*}
  Moreover, for each $x:A$ we have $\map {f}{\refl{x}}\jdeq \refl{f(x)}$.
\end{lem}

\begin{proof}[First proof]
  Let $D:\prod_{x,y:A} \prod_{p:x=y}$ be $D(x,y,p)\coloneqq (f(x)= f(y))$.
  Then we have
  \begin{equation*}
    d\coloneqq\lambda x.\refl{f(x)}:\prod_{x:A} D(x,x,\refl{x}).
  \end{equation*}
  Now $J$ gives us $\map f p\coloneqq f(x)= f(y)$ for each $p:x= y$.
  The conversion rule implies $\map f{\refl{x}}\jdeq\refl{f(x)}$ for each $x:A$.
\end{proof}

\begin{proof}[Second proof]
  By induction, it suffices to assume $p$ is $\refl{x}$, in which case we have $\refl{f(x)}:f(x)\jdeq f(x)$.
\end{proof}

Since \emph{dependently typed} functions are very important in type theory, we will also need a version of \autoref{lem:map} for these.
However, this is not quite so simple to state, because if $f:\prod_{x:A} B(x)$ and $p:x=y$, then $f(x):B(x)$ and $f(y):B(y)$ are elements of distinct types, so that \emph{a priori} we cannot even ask whether they are equal.
The missing ingredient is that $p$ itself gives us a way to relate the types $B(x)$ and $B(y)$.

\begin{lem}[Transport]\label{lem:transport}
  Suppose that $P$ is a dependent type over $A$ and that $p:\id[A]xy$.
  Then there is a function $\transf{p}:P(x)\to P(y)$.
\end{lem}

\begin{proof}[First proof]
  Let $D:\prod_{x,y:A} \prod_{p:\id{x}{y}} \type$ be $D(x,y,p)\coloneqq P(x)\to P(y)$.
  Then we have the function
  \begin{equation*}
    d\coloneqq\lambda x.\idfunc[P(x)]:\prod_{x:A} D(x,x,\refl{x}),
  \end{equation*}
  so that the induction principle gives us $J_{D,d}(x,y,p):P(x)\to P(y)$ for $p:x= y$, which we define to be $\transf p$.
\end{proof}

\begin{proof}[Second proof]
  By induction, it suffices to assume $p$ is $\refl x$.
  But in this case, we can take $\transf{(\refl x)}:P(x)\to P(x)$ to be the identity function.
\end{proof}

Recall that a dependent type $P$ over a type $A$ can be seen as a property of elements of $A$, which holds at $x$ in $A$ if $P(x)$ is inhabited.
Then the transportation lemma says that if $x$ is propositionally equal to $y$, then $P(x)$ holds if and only if $P(y)$ holds.
In fact, we will see later on that if $x=y$ then actually $P(x)$ and $P(y)$ are \emph{equivalent}.

Now we can prove the dependent version of \autoref{lem:map}.

\begin{lem}[Dependent map]\label{lem:mapdep}
  Suppose $f:\prod_{x: A} P(x)$ and $p:\id[A]xy$.
  Then we have $\mapdep fp:\id[P(y)]{\trans p{f(x)}}{f(y)}$.
\end{lem}

\begin{proof}[First proof]
  Let $D:\prod_{x,y:A}\prod_{p:x=y}$ be the dependent type given by
  \begin{equation*}
    D(x,y,p)\coloneqq \trans p {f(x)}= f(y).
  \end{equation*}
  Then $D(x,x,\refl{x})$ is $\trans{\refl{x}}{f(x)}= f(x)$.
  But since $\trans{(\refl{x})}{f(x)}\jdeq f(x)$, we get that $D(x,x,\refl{x})\jdeq (f(x)= f(x))$.
  Thus, we find the term
  \begin{equation*}
    d\coloneqq\lambda x.\refl{f(x)}:\prod_{x:A} D(x,x,\refl{x})
  \end{equation*}
  and now $J$ gives us $\mapdep fp:\trans p{f(x)}= f(y)$ for each $p:x= y$.
\end{proof}

\begin{proof}[Second proof]
  By induction, it suffices to assume $p$ is $\refl x$.
  But in this case, we have $\trans{(\refl{x})}{f(x)}\jdeq f(x)$.
\end{proof}

From now on, we will stick to the second, more concise, style of proof by induction on identity types.


% Local Variables:
% TeX-master: "main"
% End: