notes_week12.tex

\documentclass[11pt]{article}

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

\newcommand{\U}{\mathbb{U}}
\renewcommand{\SS}{\mathbb{S}}
\renewcommand{\refl}{\mathsf{refl}}
\newcommand {\sbase}{\mathsf{base}}
\newcommand {\sloop}{\mathsf{loop}}
\newcommand{\lolli}{\multimap}
\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{\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{\merid}{\mathsf{merid}}

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

\newcommand{\susp}[1]{\mathsf{Susp}(#1)}
\newcommand{\Susp}[1]{\susp{#1}}

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

\title{15-819 Homotopy Type Theory\\Lecture Notes}
\author{Matthew Maurer and Stefan Muller}
\begin{document}
\maketitle
\section{Contents}
\section{Recap}
Recall from last week the construction of the suspension of a type. Note that
we are using different notation from the book, namely $\susp{A}$ as opposed
to $\sum A$. The suspension $\susp{A}$ of $A$ contains two 0-cells:
$$N : \susp{A}$$
$$S : \susp{A}$$
and paths $\merid(a)$ between $N$ and $S$, where $a: A$.
$$\merid : \Pi x : A . N =_{\susp{A}} S$$
$$x : \susp{A} \vdash B(X) : \universe$$

We also defined recursion and induction on $\susp{A}$:
$$
\infer{z: \susp{A} \vdash \rec[B](n; s; x. m): B}
{n: B & s: B & x: A \vdash m(x): n =_B s}
$$

$$
\infer{z: \susp{A} \vdash \ind[B](n; s; x.m): B(z)}
{z: \Susp{A} \vdash B(z): \universe &
n : B(N) & s : B(S) &
x : A \vdash m(x) : n =_{\merid(x)}^{z.B} s}
$$
\section{Equivalence of $\susp{2}$ and $\SS^1$}
\begin{proposition}
$$\susp{2} \simeq \SS^1$$
\end{proposition}
\begin{proof}
$$f : \susp{2} \rightarrow \SS^1$$
defined by 
$$N \mapsto \sbase$$
$$S \mapsto \sbase$$
On the higher order part of the suspension, we define what the behavior of the one-cells should be, e.g. how $\ap$ would act.
$$\merid(tt) \mapsto \sloop$$
$$\merid(ff) \mapsto \refl(\sbase)$$
To show equivalence, we now define a quasinverse of $f$
$$g : \susp{2} \rightarrow \SS^1$$
where we send $\sbase$ is arbitrary but must be consistent
$$\sbase \mapsto N$$
$$\sloop \mapsto \merid(tt) \cdot \merid(ff)^{-1}$$
Now need to prove these are inverses
$$\alpha : \Pi x : \susp{2} . g(f(x)) = x$$
By induction
\[
\begin{array}{r l}
(x = N)& \refl(N) : N = N \\
(x = S)& \merid(ff) : N = S\\
\merid(y) & ? : \refl(N) =_{\merid(y)}^{z.f(g(z) = z} \merid(ff)
\end{array}
\]
We can case out on this,
$$\ap_g (\ap_f (\merid(tt))^{-1} \cdot \refl(N) \cdot \merid(tt)) = \merid(ff)$$
$$\ap_g (\ap_f (\merid(ff))^{-1} \cdot \refl(N) \cdot \merid(ff)) = \merid(ff)$$
stepping evaluation,
$$\ap_g (\sloop)^{-1} \cdot \merid(tt) = \merid(ff)$$
$$(\merid(tt) \cdot \merid(ff)^{-1})^{-1} \cdot \merid(ff) = \merid(ff)^{-1-1} \cdot \merid(tt)^{-1} \cdot \merid(tt) = \merid(ff)$$

Our other proof of inversion
$$\beta : \Pi x : \SS^1 . f(g(x)) = x$$
proceeds by induction on $\SS^1$
\[
\begin{array}{r l}
(x = \sbase) & \refl(\sbase) : f(g(\sbase)) = \sbase\\
(x = \sloop) & \ap_f(\ap_g(\sloop))^{-1} \cdot \refl(\sbase) = \refl(\sbase)
\end{array}
\]
\end{proof}
\section{Pointed Type}
A pointed type is one with an example inhabitant. If A is a pointed type, then, in our notation, we have $a_0 : A$.

For example, $\Omega(A, a_0) = (a_0 =_A a_0)$, ``the loop space'', is pointed by $\refl(a_0)$. $\susp{A}$ pointed by $N$ (or $S$) is another example of a pointed type.

Pointed maps, also known as strict maps, are maps between two pointed types which map the well-known point of one to the well known point of the other, as in
$$(X, x_0) \lolli (Y, y_0) := \Sigma f : X \to Y . f(x_0) = y_0$$
We set out to prove
\begin{proposition}
$$\susp{A} \lolli B \simeq (A \lolli \Omega B)$$
\end{proposition}
\begin{proof}
Given $f : \susp{A} \lolli B$, define $g : A \lolli \Omega B$ as
$$g(a) = p_0^{-1} \cdot \ap_f(\merid(a) \cdot \merid(a_0)^{-1}) \cdot p_0$$
where $f_0$ is the raw map, and $p_0$ is a proof of distinguished point preservation, e.g. $p_0 : f_0(N) = b_0$, and $f = \langle f_0, p_0\rangle$
$$q = \refl(b_0)$$

On the other side, given $g : A \lolli \Omega B$, define $f : \susp{A} \lolli B$

$$f_0(N) = b_0$$
$$f_0(S) = b_0$$
We again define the behavior of the one-cell in the HIT
$$\ap_f(\merid(a)) = g_0(a)$$

where $g_0$ is the raw map, and $q_0$ is a proof of distinguished point preservation, e.g. $q_0 : g_0(N) = b_0$ and $f = \langle g_0, q_0\rangle$
\end{proof}

\section{Pushouts}
We temporarily return to conventional set math to define a pushout, which is
dual to a pullback, which is an equationally constrained subset of a product.
On the other hand, a pushout is essentially a disjoint union of two sets 
with some of the elements ``glued'' together. Specifically, assume we have
sets $A$, $B$ and $C$ with maps $f$ and $g$ from $C$ to $A$ and $B$ 
respectively. The pushout 
$A \sqcup^C B$ is the disjoint union of $A$ and $B$ with the images $f(C)$ and
$g(C)$ merged by merging $f(c)$ and $g(c)$ together for all $c \in C$. In the
notation of type theory, we denote the disjoint union of $A$ and $B$ as 
$A + B$ and use the maps $\inl: A \to A + B$ and $\inr: B \to A + B$. We
can then define the pushout as

$$A \sqcup^C B = (A + B) / R$$
where $R$ is the least equivalence relation containing 
$\forall c \in C. R(\inl(f(c)), \inr(g(c)))$

$A \sqcup^C B$ is the ``least such'' object in the sense that it has a unique
map to any other object $D$ with the same properties:

\begin{equation*}
\begin{tikzcd}
C \arrow{r}{g} \arrow{d}{f} & B \arrow[dashed]{d}{f'} \arrow[bend left]{ddr}{f''}\\
A \arrow[dashed]{r}{g'} \arrow[bend right]{drr}{g''} & A \sqcup^C B \arrow[dashed]{dr}{!}\\
{} & {} & D\\
\end{tikzcd}
\end{equation*}
where f' and g' are identified by f and g.

\subsection{Pushouts of $A \xleftarrow{f} C \xrightarrow{g} B$}
\newcommand{\glue}{\mathsf{glue}}
Moving back to HoTT, we can define pushouts as a higher inductive type,
whose elements are those of the disjoint sum $A + B$, generated by mapping
$A$ and $B$ to the pushout $A \sqcup^C B$ by $\inl$ and $\inr$, respectively

$$\inl : A \rightarrow A \sqcup^C B$$
$$\inr : B \rightarrow A \sqcup^C B$$

and whose 1-cells connect $\inl(f(c))$ and $\inr(g(c))$ for every element $c$
of $C$.

$$\glue : \Pi c : C. \Id{A \sqcup^C B} (\inl(f(c)), \inr(g(c)))$$

As usual, we can define a recursor $\rec[D](\cdots): A \sqcup^C B \to D$ (the
map implied by the diagram above.) Note that for every element $u$ of $C$, the
recursor requires that there exist a path witnessing the equality of
$[f(u)/x]l$ and $[g(u)/y]r$, representing the action of the recursor on
$\glue$ and ensuring that the images of elements ``glued together'' in the
pushout are also glued together in $D$.

\[
\infer{z : A \sqcup^C B \vdash \rec[D](x.l; y.r; u.q)(z) : D}
{x : A \vdash l : D &
y : B \vdash r : D &
u : C \vdash q : [f(u)/x]l =_D [g(u)/y]r}
\]

We have the usual $\beta$ rules.

$$rec(x.l; y.r; u.q)(\inl(a)) \equiv [a/x]l$$
$$rec(x.l; y.r; u.q)(\inr(b)) \equiv [b/y]r$$
$$\ap_{rec(x.l; y.r; u.q)}(glue(c)) = [c/u]q$$

The idea of gluing together elements of a higher inductive type with a path
for each element of a given type seems very reminiscent of suspensions. In
fact, suspensions can be defined as pushouts $A \sqcup^C B$ with the types
$A$ and $B$ and the maps $f$ and $g$ trivial:

$$\susp A = 1 \sqcup^A 1$$

\begin{equation*}
\begin{tikzcd}
{} & A \arrow{dr}{!} \arrow{dl}{!} & {}\\
1 \arrow{dr}{\inl} & {} & 1 \arrow{dl}{\inr} \\
{} & \susp{A} & {}\\
\end{tikzcd}
\end{equation*}

This immediately implies the following:
\begin{cor}The pushout of two sets needn't be a set.\end{cor}
This is true since $\SS^1 = \susp{2}$, but $\SS^1$ is known not to be a set.


\section{Quotients as HITs}
\newcommand{\trunc}{\mathsf{trunc}}
The set definition of pushouts is in terms of a quotient, so we might
consider defining quotients of sets by props uing HITs.

Consider the type-theoretic representation of $A/R$, a type $A$ quotiented
by the relation $R$. We define this type to have the normal properties of the
quotient. We must be able to project an element of $A$ into $A/R$, e.g. by
computing its representative
$$q : A \to A/R$$
If we have two elements $a$ and $b$ of $A$ that are related by $R$, that is,
$R(a, b)$, then we must have a proof of equality
$$\mathsf{wd}: \Pi a,b: A. R(a,b) \to q(a) = q(b)$$
The above are the expected properties. However, we also wish for
$A/R$ to be a set. This requires that all proofs of equality in $A/R$ must
themselves be equal. We truncate $A/R$ to a set by adding the required proofs
of equality for all paths $p, q$ between elements $x$ and $y$.
$$\trunc : \Pi x,y: A/R. \Pi p, q : x =_{A/R} y. p = q$$

Saying there is a function from $A/R$ to some type $B$ is the same as saying there is a function from A to B that respects $R$ by mapping related elements
to elements that are (propositionally) equal in $B$.

\begin{proposition}
$$(A/R) \rightarrow B \simeq \sum_{f : A \rightarrow B} \Pi_{a, b : A} . R(a, b) \rightarrow f(a) =_B f(b)$$
\end{proposition}

A proof appears in the textbook.

\newcommand{\N}{\mathbb{N}}
\newcommand{\Z}{\mathbb{Z}}
\subsection{Example: $\Z$}
We can represent integers as pairs of natural numbers $(a, b)$ (representing
the integer $a - b$). Since (infinitely) many pairs correspond to each
integer, we quotient out by an appropriate relation.
$$\Z = (\N \times \N) / R$$
where $R((a_1, b_1), (a_2, b_2))$ iff $a_1 + b_2 = a_2 + b_1$. This
representation will be important in the proof that $\pi_1(\SS^1) \simeq \Z$
in Section~\ref{sec:fundgroup}.

\section{Truncations as HITs}
\newcommand{\ntrunc}[2]{||#1||_{#2}}
\newcommand{\propt}[1]{\ntrunc{#1}{-1}}
\newcommand{\vntrunc}[2]{|#1|_{#2}}
\newcommand{\vpropt}[1]{\vntrunc{#1}{-1}}
\newcommand{\ssquash}{\mathsf{squash}}

We have previously seen the propositional truncation $\ntrunc{A}{}$, which
truncates the type $A$ to a proposition by forcing proofs of equality for all
values. We now redefine the propositional truncation as a higher inductive
type. Since we will generalize this to truncations for all h-levels $n$, we
now write propositional truncation as $\propt{A}$.

The higher inductive type $\propt{A}$ has a simple constructor
$$\vpropt{-} : A \rightarrow \propt{A}$$
To add the 1-cells, $\ssquash$ produces a proof of equality for any two
values of $A$.
$$\ssquash : \Pi_{a, b : \propt{A}} . a =_{\propt{A}} b$$

The induction principle is as follows:
$$
\inferrule
{z : \propt{A} \vdash P(z) : \universe \qquad
x : A \vdash p : P(\vpropt{x}) \\
x, y : \propt{A}, u : P(x), v : P(y) \vdash q : u =_{\ssquash(x, y)}^{z.P} v}
{z : \propt{A} \vdash \ind[z.P](x. p; x, y, u, v. q)(z) : P(z)}
$$

We can now use the same methodology to define set truncation as a HIT:
\newcommand{\sett}[1]{\ntrunc{#1}{0}}
\newcommand{\vsett}[1]{\vntrunc{#1}{0}}
$$\vsett{-} : A \rightarrow \sett{A}$$
As in the definition of quotients, the set truncation provides proofs of
equality for all paths.
$$x, y : \sett{A}, p, q : x =_{\sett{A}} y \vdash \ssquash(x, y, p, q) : p =_{x = y} q$$

And we state an induction principle:
$$
\inferrule
{z : \sett{A} \vdash P : U \qquad
x : A \vdash g : P(\vsett{A}) \\
x, y : \sett{A}, z : P(x), w : P(y), p, q : x = y, r : z=_p^{z.P} w, s : z =_q^{z.P} w \vdash ip : p =_{\ssquash(x,y,p,q)}^{z.P} q}
{z : \sett{A} \vdash \ind[z.P](x. g; x, y, z, w, p, q, r, s. ip)(z): P(z)}
$$

\begin{proposition}\label{prop:sett}
If $A$ is a set, it is equivalent to its own set truncation, i.e.

\[\mathsf{isSet}(A) \to \sett{A} \simeq A\]
\end{proposition}

\section{Fundamental group of $\SS^1$}\label{sec:fundgroup}
Recall $\SS^1$ is a HIT defined by

$$\sbase : \SS^1$$
$$\sloop : \sbase =_{\SS^1} \sbase$$

Recall $\Omega(A, a_0) := (a_0 =_A a_0)$

The fundamental group of $A$ at $a_0$, $\pi_1(A, a_0)$,
is defined to be $\sett{\Omega(A, a_0)}$.

\begin{thm}
We want to show that
$$\pi_1(\SS^1) \simeq Z$$
\begin{proof}
Show $\Omega(\SS^1, \sbase) \simeq \Z$ (this suffices by Proposition~\ref{prop:sett}.)

We define a map
$$\sloop^{(-)} : \Z \rightarrow \Omega(\SS^1)$$
as follows:
$$\sloop^{(0)} = \refl(\sbase)$$
$$\sloop^{(-n)} = \sloop^{(-n + 1)} \cdot \sloop^{-1}$$
$$\sloop^{(+n)} = \sloop^{(n - 1)} \cdot \sloop$$
This could be, for example, defined by the $\Z$ recursor

$$winding : \Omega(\SS^{1}) \rightarrow \Z$$
We take that $succ : \Z \simeq \Z$, and $pred = succ^{-1}$, defined by shifting all the numbers up/down by one

So, we have
$$ua(succ) : \Z =_\universe \Z$$

By the recursion principle (not induction)
$$code : \SS^1 \rightarrow \universe$$
$$code(\sbase) = \Z$$
$$code(\sloop) = ua(succ)$$

$$\ap_{code} : \Omega(\SS^1) \rightarrow (\Z = \Z)$$
$$winding(p) = tr[x.x](\ap_{code}(p))(0)$$
\begin{proposition}
$$\Pi_{n : Z} . winding(\sloop^{(n)}) =_Z n$$
\end{proposition}
\begin{proof}
Straightforward by induction
\end{proof}

\begin{proposition}
$$\Pi_{l : \Omega(\SS^1)} \sloop^{winding(l)} =_{\Omega(\SS^1)} l$$
\end{proposition}

We can't proceed by path induction on l, as the path is not free

$$encode : \Pi_{x : \SS^1} (\sbase = x) \rightarrow code(x)$$
$$decode : \Pi_{x : \SS^1} code(x) \rightarrow \sbase = x$$

$$encode(x,p) \defeq tr[code](p)(o)$$
$$decode(x) \defeq \rec_{\SS^1}[z.code(z) \rightarrow \sbase = z](\lambda z . \refl(\sbase), \lambda n . \sloop^{(n)})(x)$$

To complete the proof, you will need a path induction and a circle induction.
%\end{prop}
\end{proof}
\end{thm}

\end{document}