notes_week9.tex

\documentclass[11pt]{article}

\usepackage{tikz-cd}

\usepackage{proof-dashed}
\input{macros}

\setlength{\inferLineSkip}{4pt}

\metadata{Lewis and Tassarotti}{2013/11/11 and 2013/11/13}

\newcommand*{\Void}{\mathsf{0}}
\newcommand*{\Unit}{\mathsf{1}}
\newcommand*{\Bool}{\mathsf{2}}

\newcommand*{\Interval}{I}
\newcommand*{\Izero}{0_I}
\newcommand*{\Ione}{1_I}
\newcommand*{\Iseg}{\mathsf{seg}}

\newcommand*{\ap}{\mathsf{ap}}
\newcommand*{\apd}{\mathsf{apd}}

\newcommand*{\funext}{\mathsf{funext}}
\newcommand*{\isSet}{\mathsf{isSet}}
\newcommand*{\isProp}{\mathsf{isProp}}
\newcommand*{\elimtrunc}{\mathsf{elim}}
\newcommand*{\isContr}{\mathsf{isContr}}
\newcommand*{\squash}{\mathsf{squash}}
\newcommand{\iseq}{\mathsf{isequiv}}
\newcommand{\qinv}{\mathsf{qinv}}
\newcommand*{\comp}{\mathbin{\circ}}

\newcommand{\biequiv}{\mathsf{biequiv}}
\newcommand{\isContrf}{\mathsf{isContr}}
\newcommand{\ishae}{\mathsf{ishae}}
\newcommand{\fib}{\mathsf{fib}}

\newcommand*{\isNtype}[1]{\mathsf{is}\mbox{-}#1\mbox{-}\mathsf{type}}

\newtheorem{lemma}{Lemma}
\newtheorem{thm}{Theorem}
\newtheorem{proposition}{Proposition}
\newtheorem{defn}{Definition}

\title{15-819 Homotopy Type Theory\\Lecture Notes}
\author{Robert Lewis and Joseph Tassarotti}
\date{November 11 and 13, 2013}

\begin{document}

\maketitle

\section{Contents}
These notes cover Robert Harper's lectures on Homotopy Type Theory from
November 11 and 13, 2013. Discussions include Hedberg's theorem, contractibility,
propositional truncation, and the ``axiom'' of choice.


\section{Refresher: Sets and Propositions}
Recall from previous lectures the definitions of sets and propositions within HoTT.
A type is called a set if there is only ``one way'' for any two of its elements to be equal:
$$ \isSet(A) \defeq \prod_{x,y:A}\prod_{p,q: x=_Ay}(p=_{x=_A y}q) $$

Relatedly, a type is called a proposition if it is a ``subsingleton'': that is, it has at most one inhabitant.
$$ \isProp(A) \defeq \prod_{x,y:A}(x=_A y) $$

We can define $\isSet$ in terms of $\isProp$: a type is a set if equality for that type is propositional.
$$ \isSet(A) \equiv \prod_{x,y:A}\isProp(x=_A y) $$

What it means for a type to be a set is that there are no nontrivial relationships between 
elements of the type. The higher homotopy structure we have seen in previous weeks does not exist
in a set, as the only paths between elements are trivial, which trivializes the higher structure.
In this sense, sets (and propositions) ``reclaim'' some properties of classical mathematics.
%: for instance, $\isProp(A)\to\neg\neg A\to A$. (True?)

\begin{proposition}
 For any type $A$, we have $\isProp(\neg A)$, where $\neg A\defeq A\to \zero$.
\end{proposition}
\begin{proof}
 We want to find $$\_:\prod_{x,y:\neg A}(x=_{\neg A} y).$$ Since $\neg A$ is a function type, 
 via $\funext$ it suffices to find $$\_:\prod_{u: A}(x(u) =_\zero y(u)).$$ 
 We have $\lambda u.\, \abort{x(u)=_\zero y(u)}(x(u))$ of this type.
 %Where in notes was abort defined? I can't find it.
\end{proof}

From this, we can derive the (perhaps surprising) result that $\neg\neg (\neg A)\to \neg A$,
even though we do not necessarily have $\neg\neg A \to A$.

\section{Hedberg's Theorem}
These considerations lead us to the following important theorem.

\begin{defn}
 A type $A$ has \emph{decidable equality} if one can prove of any two inhabitants of $A$ 
 that they are either equal or unequal.
 $$\prod_{x,y:A}(\Id{A}(x,y)\vee \neg \Id{A}(x,y)).$$
 
 A type $A$ has \emph{stable equality} if double-negation elimination holds in its identity type:
 $$\prod_{x,y:A}(\neg\neg \Id{A}(x,y)\to \Id{A}(x,y))$$
\end{defn}

\begin{thm}
 A type with decidable equality is a set.
\end{thm}
\begin{proof}
 
 The proof of Hedberg's theorem goes in two parts:
 \begin{enumerate}
  \item Decidable equality implies stable equality. In fact, we can prove in general that for 
  any type $A$, $(A+\neg A)\to \neg\neg A \to A$. This part is simple and left as an exercise.
  
  \item Stable equality implies sethood. This is the heart of Hedberg's theorem.
 \end{enumerate}
 
 We prove 2. Suppose $h:\prod x,y:A.(\neg \neg x=_A y)\to (x=_Ay)$ is evidence
 that equality in $A$ is stable.  To show $\isSet(A)$, is suffices to show that
 $x:A, p:x=_A x\entails p=_{x=_A x} \refl{A}(x)$, since we can reduce the
 identity of $p,q:x=_A y$ to showing that $p \concat q^{-1} = \refl{A}(x)$.
 
 Fix $x:A$. We then have $h(x):\prod y:A.(\neg\neg x=_A y)\to(x=_A y)$.
 
 Using dependent function application $\apd$ (defined previously), we see that
 $$\apd_{h(x)}(p): p_*(h(x)(x))=_{(\neg\neg x=_A x)\to(x=_A x)}h(x)(x)$$

 By lemma 2.9.6 of~\cite{HoTTBook2013}, it follows that for that for any $r:\neg\neg(x=_A x)$,
 $$ p_*(h(x)(x))(r)=_{x=_A x} h(x)(x)(p_* r). $$

 Next, from a proven property of transport in identity types, we have that
 $$ p_*(h(x)(x))(r) =_{x=_A x} h(x)(x)(r)\cdot p $$ % This shouldn't be definitional, is it?
 and because negated types are propositions (from above),
 $$ h(x)(x)(p_* r) =_{x=_A x} h(x)(x)(r)$$
 so we have by transitivity
 $$ h(x)(x)(r)\cdot p =_{x=_A x} h(x)(x)(r) $$
 and cancellation gives us $p =_{x=_A x} \refl{A}(x)$ as desired.
\end{proof}

For an example of the power of Hedberg's theorem, note that it implies $\isSet(\Nat)$.
Using double induction, one can show 
$$\prod_{x,y:\Nat}(x=_\Nat y)\vee \neg (x=_\Nat y).$$ This is left as an exercise.

\section{More Results on Propositions and Sets}
\begin{thm}
 Every proposition is a set:
 $$\text{\emph{If} }\prod_{x,y:A}x=_A y\text{ \emph{then} }\prod_{x,y:A}\prod_{p,q:x=_A y}p=_{x=_A y} q$$
\end{thm}

\begin{proof}
 Suppose $f:\prod x,y:A.x=_A y$. Given two inhabitants of $A$, $f$ returns a path between them.
 
 Fix $x_0:A$ and let $g \defeq f(x_0):\prod y:A.x_0=_A y$. For $p:y=_A y'$, we have 
 $$\apd_g(p): p_*(g(y)) =_{x_0=_A y'} g(y')$$
 
 and by property of transport within identity type,
 $$p_*(g(y))=_{x_0=_A y'} g(y)\cdot p.$$
 
 By transitivity, we thus have
 $$g(y)\cdot p =_{x_0=_A y'} g(y')$$
 $$p =_{x_0=_A y'} g(y)^{-1}\cdot g(y)$$
 
 For $q:y=_A y'$, these same calculations give us 
 $$q =_{x_0=_A y'} g(y)^{-1}\cdot g(y).$$
 
 Thus, $p =_{x_0=_A y'} q$ as desired.
\end{proof}

\begin{thm}
 $\isProp(\isProp(A))$ -- that is, there is only one proof that $A$ has only one inhabitant.
\end{thm}
\begin{proof}
 Let $f,g:\isProp(A)$ be given. To show $f =_{\isProp(A)} g$, it suffices to show (by $\funext$)
 $x,y:A\entails \_: f x y =_{x=_A y} g x y$. This follows since $\isProp(A)\to \isSet(A)$.
\end{proof}

We can similarly prove $\isProp(\isSet(A))$. For $f:A\to B$, with the proper notion of 
$\mathsf{isEquiv}(f)$, we will soon be able to prove $\isProp(\mathsf{isEquiv}(f))$.
If we take equivalence to mean having a quasi-inverse, though, this is not the case.


\section{Contractibility}
In preparation for what follows, we define the notion of contractibility:
$$\isContr(A):\sum_{x:A}\prod_{y:A}x=_A y$$

That is, a type is contractible if there is some inhabitant which all other
inhabitants are equal to. This is equivalent to saying that $A$ is a prop, and
it is inhabited. Alternatively, a $A$ type is contractibile if it is equivalent
to $1$. 

Notice that for any type $A$, given $a{:}A$, we have that $\isContr(\Sigma
x{:}A a = x)$. In particular, $\tuple{a}{\refl{A}(a))}$ is an inhabitant of
this type which all other elements are equal to.

\begin{figure}
\label{fig:contractible}
\begin{center}
\begin{tikzpicture}
   \draw (0, 0) ellipse (3cm and 3cm);

   \node [above] at (0 cm, 0cm) {$x$};
   \draw [fill] (0 cm, 0cm) circle [radius=.05cm];
   \draw [fill] (1.5 cm, 1.5cm) circle [radius=.05cm];
   \draw [fill] (-1.5 cm, 1.5cm) circle [radius=.05cm];
   \draw [fill] (-1.50 cm, -1.5cm) circle [radius=.05cm];
   \draw [fill] (1.5 cm, -1.5cm) circle [radius=.05cm];
   \draw [double equal sign distance, shorten <= .25cm, shorten >= .25cm] (0cm, 0cm) -- (1.5cm, 1.5cm);
   \draw [double equal sign distance, shorten <= .25cm, shorten >= .25cm] (0cm, 0cm) -- (1.5cm, -1.5cm);
   \draw [double equal sign distance, shorten <= .25cm, shorten >= .25cm] (0cm, 0cm) -- (-1.5cm, -1.5cm);
   \draw [double equal sign distance, shorten <= .25cm, shorten >= .25cm] (0cm, 0cm) -- (-1.5cm, 1.5cm);
\end{tikzpicture}
\end{center}
\caption{A contractible type. There is some element $x$, and paths between $x$ and all other elements}
\end{figure}

The notions of contraction and truncation are related to the (n)-type hierarchy: 
specifically, contractions sit at the bottom of the hierarchy. For historical reasons,
we begin with (-2) types, and define inductively:
\begin{align*}
 \isNtype{(-2)}(A)\defeq&\ \isContr(A) \\ %Better way to format this?
 \isNtype{(n+1)}(A)\defeq &\ \prod_{x,y:A}\isNtype{n}(x=_A y)
\end{align*}

Now, we have that: 

 $$\isProp(A)\leftrightarrow \prod_{x,y:A}\isContr(x=_A y).$$
which implies that
$$\isProp(A)\leftrightarrow \isNtype{(-1)}(A).$$

We can further prove the following:
\begin{align*}
 \isSet(A)\leftrightarrow &\ \isNtype{0}(A) \\
 \mathsf{isGpd}(A)\leftrightarrow &\ \isNtype{1}(A) \\
 \mathsf{is}\mbox{-}2\mbox{-}\mathsf{Gpd}(A)\leftrightarrow &\ \isNtype{2}(A) \\
 \vdots\ & 
\end{align*}

As well as
$$\prod_{A:\mathcal{U}}\left( \isNtype{n}(A)\to \isNtype{(n+1)}(A) \right).$$

However, it is \emph{not} the case that every type is an $n$-type for some $n$: consider $\mathcal{U}$.

\section{Propositional Truncation (Squashing)}

The notion of ``squashing'' introduced last week was perhaps too heavy-handed:
it was used toward a number of goals, among them to recover classical logic
within constructive logic. We now introduce the more general idea of
\emph{abstract truncation}, which for now will be taken as a primitive idea of
HoTT. Truncation serves to reduce types to sets, without all the byproducts of
the double negation translation.

Let $\|A\|_{-1}$ be read as the \emph{(-1)-truncation} of $A$. When the context
is clear, we omit the subscript. When the type $\|A\|$ is inhabited, we say $A$
is ``merely inhabited'', to emphasize that this is a proof-irrelevant setting.
We have the following $\|\cdot \|$-introduction rules:

\begin{mathpar}
  \infer[{}]{\Gamma \entails |M|:\|A\|}{
    \Gamma \entails M:A}
  \and
  \infer[{}]{\Gamma, x: \|A\|, y: \|A\| \entails \squash(x, y): \Id{\|A\|}(x, y)}{
    }
\end{mathpar}

As we would expect, $\isProp(\|A\|)$ because of the rule for $\squash(\cdot, \cdot)$. The corresponding elimination rule s:
$$
  \infer[{\|\cdot\|}E]{\elimtrunc[B](M; x.N; P):B}{
    \Gamma \entails M:\|A\| & \Gamma, x:A\entails N:B & \Gamma \entails P:\isProp(B)}
$$

We require a proof of $\isProp(B)$ to ensure that the behavior of $N$ does not depend on the
representative $x:A$. There are other ways to ensure this property: for instance, we could instead
require $u,v:A\entails [u/x]N =_B [v/x]N$. Note that $\isProp(B)$ implies that this is the case.

The $\beta$ rule works as one might expect:
$$\elimtrunc(|M|; x.N; P)\equiv [M/x]N$$

One would similarly like some $\beta$ like rule to hold for the 1-cell, $\squash$. For
example, something of the form $$\ap(\lambda z. \elimtrunc(z; x. N;
P))(\squash(|M|, |M'|)) \jdeq P([M/x]N)([M'/x]N)$$ which corresponds to the
idea that $P$ is a proof that $N$ is equal under substitutions of different
terms of type $A$, because $B$ is a proposition. However, just as in the case of 
$\mathsf{seg}$, we do not have this.

\section{Revisiting the Axiom of Choice}

Previously, we explored how the axiom of choice is provable in ITT. That is, there is a term $AC_\infty$ such that
$$AC_\infty{:} \prod_{A{:}U} \prod_{B{:}A \to U} \prod_{C{:}\Pi x:A. B \to U}
\left(\left( \prod_{x{:}A} \sum_{y: B(x)} C(x,y) \right ) \to \left(\sum_{f: \Pi x{:} A. B} \prod_{x:A} C(x, f(x))\right)\right)
$$

In fact, we can strengthen this and say that the two types are equivalent.
Recall that this type is inhabited because the witness that the relation $C$ is
total provides precisely the choice we should make, because the specification
is proof relevant. The situation is similar to the example that motivated our
introduction of propositional truncation, where we wanted to write a total
function that returned the index of the first occurrence of 0 in an infinite
sequence. The proof that the infinite sequence actually contained a 0 also
immediately told us where the 0 was.

Now that we have developed the notion of propositional truncation, we can state
a version of the axiom of choice that is closer in meaning to its typical
statement:
\begin{multline*}
\prod_{A{:}U} \prod_{B{:}A \to U} \prod_{C{:}\Pi x:A. B \to U}
\left(\isSet(A) \to \left(\prod_{x:A} \isSet(B(x))\right) \to \left(\prod_{x:A} \prod_{y: B(x)} \isProp(C(x,y))\right) \right. \\
\left. \to \left(\left( \prod_{x{:}A} \left|\left|\sum_{y: B_x} C(x,y) \right|\right| \right ) \to 
  \left|\left| \sum_{f: \Pi x{:} A. B} \prod_{x:A} C(x, f(x)) \right|\right| \right)\right)
\end{multline*}

%% This is how it was scoped when written on the board, but it is really hard to typeset it 
%%$$\prod_{A{:}U}\left(\isSet(A) \to 
%%     \prod_{B{:}A \to U} \left(\prod_{x{:}A} \isSet(B(x))\right) \to 
%%  \prod_{C{:}\Pi x:A. B \to U} \prod_{x{:}A} \prod_{y{:}B_x} \isProp(C(x, y)) \to ...
%%$$

This restated form is not provable. What has happened is now that we say that
there merely exists some $y$ for each $x$ such that $C(x,y)$. The axiom says
that given such weaker evidence, there merely exists such a function $f$ where
for each $x$, $C(x,f(x))$. We might call an axiom of such a type $AC_{-1}$, to
emphasize that it involves the $-1$-truncation.

Now, the truncations of equivalent types are equivalent. Since the
non-truncated form of the axiom of choice, $AC_{\infty}$, gives us the
equivalence
$$
\left(\left( \prod_{x{:}A} \sum_{y: B(x)} C(x,y) \right ) \simeq \left(\sum_{f: \Pi x{:} A. B} \prod_{x:A} C(x, f(x))\right)\right)
$$
so that the type of $AC_{-1}$ is equivalent to
\begin{multline*}
\prod_{A{:}U} \prod_{B{:}A \to U} \prod_{C{:}\Pi x:A. B \to U}
\left(\isSet(A) \to \left(\prod_{x:A} \isSet(B(x))\right) \to \left(\prod_{x:A} \prod_{y: B(x)} \isProp(C(x,y))\right) \right. \\
\left. \to \left(\left( \prod_{x{:}A} \left|\left|\sum_{y: B_x} C(x,y) \right|\right| \right ) \to 
  \left|\left| \prod_{x{:}A} \sum_{Y: B(x)} C(x,y) \right|\right| \right)\right)
\end{multline*}

Now, for all $Y: A \to U$, we have that $\Pi_{x:A} Y(x) \simeq \Pi_{x:A}(\Sigma_{a:Y(x)} 1)$, so we can simplify the above type to:
\begin{multline*}
\prod_{A{:}U} \prod_{Y{:}A \to U}
\left(\isSet(A) \to \left(\prod_{x:A} \isSet(Y(x))\right)
\to \left(\left( \prod_{x{:}A} \left|\left|Y(x) \right|\right| \right) \to 
  \left|\left| \prod_{x{:}A} Y(x) \right|\right| \right)\right)
\end{multline*}

In this form, we see that the axiom is saying that a product of a family of
merely inhabited sets is merely inhabited, which is well-known to be equivalent
to the axiom of choice in classical mathematics. It is crucial here that
$\isSet(A)$, since if $A$ is not a set, there is a counter example (see lemma
3.8.5 in~\cite{HoTTBook2013})


\section{Equivalence and Propositions}

A few weeks ago, we defined what it meant for a map $f: A \to B$ to be an
equivalence between $A$ and $B$, written $\iseq(f)$. The definition we gave
was: $$\iseq(f)\defeq (\Sigma g: B\to A.f\comp g \sim \id_B)\times (\Sigma h:
B\to A.h\comp f \sim \id_A).$$

We also gave the related notion of a quasi-inverse, written $\qinv(f)$, which
was defined as: $$\qinv(f)\defeq \Sigma g:B\to A.(f\comp g\sim \id_B \times
g\comp f\sim \id_A).$$

In some ways, the definition of $\qinv$ may at first appear to be a more
natural definition than $\iseq$, since it states that there is some function
$g$ which is a left and right inverse of $f$. This is the definition of an
isomorphism in category theory, for example. Of course, we explained that
$\iseq(f) \to \qinv(f)$ and $\qinv(f) \to \iseq(f)$, and this enabled us to use
whatever definition was more convenient over the past few weeks.

Why did we choose the above definition for $\iseq$ instead of using the
definition we gave for $\qinv$? The issue is that we would like there to be
only one proof that a given function $f$ is an equivalence. That is, we want
$\isProp(\iseq(f))$ to hold for all $f$. This is the case for the definition we
gave, but it is not true that $\isProp(\qinv(f))$ for every $f$. We can show this 
by establishing two lemmas:

\begin{proposition}
If $f: A \to B$ and $e: \qinv(f)$ then $\qinv(f) \simeq \Pi x{:}A. (x = x)$
\end{proposition}

\begin{proposition}
There exists some type $X$ such that $\Pi x{:}X (x = x)$ is not a proposition.
\end{proposition}

See the discussion in section 4.1 in~\cite{HoTTBook2013} for proofs of these
lemmas. This makes $\qinv$ unsuitable as a definition for $\iseq$. 
Nevertheless, we would still like a definition of $\iseq$ to be interprovable with $\qinv$,
while also being a proposition. There are three candidates which satisfy these properties, all of which are equivalent:

\begin{enumerate}
\item $\biequiv(f) \defeq (\Sigma g: B\to A.f\comp g \sim \id_B)\times (\Sigma h:
B\to A.h\comp f \sim \id_A).$

We say that $f$ is \emph{bi-invertible}, which means that $f$ has a left
inverse and a right inverse. This is the definition we have been using.

\medskip

\item $\isContrf(f) \defeq \Pi y{:}B.\, \isContr(\fib_f(y))$ where $\fib_f(y) =
\Sigma x{:}A. f(x) = y$.

This says that $f$ is contractible if given any $y$ in the codomain, the set of
all things that $f$ maps to $y$ (the fiber), is contractible. That is, for
every point in the codomain, there is an element $x$ in the domain such that
$f(x) = y$, and if $f(x') = y$ then $x = x'$. But that precisely means that $f$
is a bijection up to homotopy. 

\medskip
\item $\ishae(f) \defeq \Sigma g{:} B \to A. \Sigma \alpha{:} (f \comp g \sim id). \Sigma \beta{:} (g \comp f \sim id). \\ \smallskip \qquad \qquad \qquad \Pi x{:A}. f(\beta x) = \alpha(f x)  $:

We read this as saying that $f$ is a \emph{half-adjoint equivalence}. We did
not talk about this definition in class, but a discussion can be found in
section 4.2 of~\cite{HoTTBook2013}. Roughly, we can motivate this by noticing
that it is similar to the definition of $\qinv$ (where the homotopies $\alpha$
and $\beta$ were unnamed) with an additional coherence condition relating how
these homotopies interact with $f$.
\end{enumerate}


\bibliographystyle{plain}
\bibliography{hott_references}

\end{document}