notes_week10.tex

\documentclass[11pt]{article}
\usepackage[letterpaper]{geometry}

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

%\setlength{\inferLineSkip}{4pt}

\metadata{Muller and Cavallo}{2013/11/18 and 2013/11/20}

\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*{\z}{0}
\newcommand*{\s}{\mathsf{succ}}

\newcommand*{\dummy}{\_}
\newcommand*{\triv}{\langle \rangle}

\newcommand*{\comp}{\circ}

\newcommand*{\W}{\mathsf{W}}
\newcommand*{\wrec}{\mathsf{wrec}}
\newcommand*{\wind}{\mathsf{wind}}

\newtheorem{lemma}{Lemma}

\title{15-819 Homotopy Type Theory\\Lecture Notes}
\author{Evan Cavallo and Stefan Muller}
\date{November 18 and 20, 2013}

\begin{document}

\maketitle

\section{Reconsider $\Nat$ in simple types}

As a warmup to discussing inductive types, we first review several equivalent
presentations of the simple type $\Nat$ seen earlier in the course. The
introduction forms for $\Nat$ are $\z$ and $\s(M)$ for any $M: \Nat$.
The elimination form is the recursor $\rec$.

\subsection{Traditional Form}

\[
\begin{array}{c}

\infer[{\Nat}I_{z1}]{\ctx \entails \z : \Nat}{}

\qquad
\hfill

\infer[{\Nat}I_{s1}]{\ctx \entails \s(M) : \Nat}{\ctx \entails M: \Nat}

\\[4ex]

\infer[{\Nat}E_1]
{\ctx \entails \rec[A](M; M_0; x. M_1): A}
{\ctx \entails M : \Nat \qquad
\ctx \entails M_0 : A \qquad
\ctx, x: A \entails M_1 :A}

\end{array}
\]

We include the motive $A$ in the recursor to motivate the dependently-typed
presentation to come although it is not necessary in the simply-typed setting.
The dynamic behavior of $\rec$ is defined by the following $\beta$ rules.

\[\rec[A](\z; M_0; x. M_1) \jdeq M_0\]
\[\rec[A](\s(M); M_0; x. M_1) \jdeq [\rec[A](M; M_0; x. M_1)/x]M_1\]

The recursor on $\z$ returns the base case $M_0$. On $\s(M)$, it substitutes
the recursive result on $M$ for $x$ in $M_1$. The $\eta$ rule states that
any object that ``behaves like'' the recursor is definitionally equal to the
recursor on the appropriate arguments.

\[
\infer[\eta]
{\ctx, y: \Nat \entails N \jdeq \rec[A](y; M_0; x. M_1)}
{[0/y]N \jdeq M_0 \qquad
\ctx, z: \Nat \entails [\s(z)/y]N \jdeq [[z/y]N/x]M_1 : A}
\]

%\subsection{Alternate Form}
%The introduction and elimination rules can be presented in this alternate form:

%\[
%\begin{array}{c}
%\cdot \entails \z : \Nat ({\Nat}I_{z2})

%\qquad
%\hfill

%x: \Nat \entails \s(x) : \Nat ({\Nat}I_{s2})

%\\[4ex]

%M: \Nat, M_0: A, x: A, M_1
%\end{array}
%\]

%% TODO: Help!

\subsection{As elements of the exponential}
The introduction forms of $\Nat$ may be treated as exponentials in the absence
of a context.

\[\cdot \entails \z : 1 \to \Nat \qquad ({\Nat}I_{z3})\]
\[\cdot \entails \s : \Nat \to \Nat \qquad ({\Nat}I_{s3})\]

Note that the type $1 \to \Nat$ is equivalent to the type $\Nat$. There are
two ways to present the elimination form in this format. The first moves the
$\Nat$ on which the recursion is done to the argument position, implying that
$\rec$ has exponential type.

\[
\infer[{\Nat}E_{3a}]
{z: \Nat \entails \rec[A](M_0; x. M_1)(z): A}
{\cdot \entails M_0: A \qquad x: A \entails M_1: A}
\]

This can be presented in a more direct way by omitting the argument.

\[
\infer[{\Nat}E_{3b}]
{\cdot \entails \rec[A](M_0; x. M_1): \Nat \to A}
{\cdot \entails M_0: A \qquad x: A \entails M_1: A}
\]

We can derive rules $\Nat I_{z1}$, $\Nat I_{s1}$ and $\Nat E_1$.
For example,

\[
\begin{array}{c}
\infer{\ctx, M: \Nat \entails \s(M) : \Nat}
{\infer{\ctx, M: \Nat \entails M: \Nat}{\strut} \qquad
\infer[\Nat I_{s3}]{\ctx, M: \Nat \entails \s : \Nat \to \Nat}{\strut}}
\end{array}
\]

\section{$\Nat$-algebras}
We now motivate the idea of $\Nat$-algebras, which are maps of the form
$1 + A \to A$. From the name, one would expect there to be a $\Nat$-algebra
where $A$ is $\Nat$. Indeed, there is.

\[z: 1 + \Nat \entails \case(z; \dummy. \z; x. \s(x)) : \Nat\]

We can write $\case(z; \dummy. \z; x. \s(x))$
above as $\{\dummy. \z; x. \s(x)\}(z)$ or, somewhat abusively,
$\{\z, \s\}(z)$. This gives

\[\cdot \entails \{\z, \s\} : 1 + \Nat \to \Nat\]

as desired. More generally, we can write any $\Nat$-algebra as
$\alpha = \{\alpha_0, \alpha_1\}$ where $\alpha_0 : 1 \to \Nat$ (or,
equivalently, $\alpha_0 : \Nat$) and $\alpha_1: \Nat \to \Nat$. We call
$\alpha_0$ the {\em basis} or {\em pseudo-zero} and $\alpha_1$ the
{\em inductive step} or {\em pseudo-successor}.

In fact, $\{\z, \s\}$ holds a special position among $\Nat$-algebras.
The $\Nat$-algebras form a category and $\{\z, \s\}$ is the initial object
in this category. Recall that this means it has a unique morphism to any other
object in the category. This requires us to define morphisms between
$\Nat$-algebras, which we will call {\em $\Nat$-homomorphisms}. Given two
$\Nat$-algebras, $\alpha : 1 + A \to A$ and $\beta: 1 + B \to B$,
$h: A \to B$ is a $\Nat$-homomorphism if it makes the following diagram commute.

\[
\begin{tikzcd}
1+A \arrow{d}{\alpha} \arrow{r}{1+h} & 1+B \arrow{d}{\beta}\\
A \arrow{r}{h} & B
\end{tikzcd}
\]

The map $1 + h: 1 + A \to 1 + B$ is defined in the natural way:

\[1 + h \defeq \{\dummy. \inl\; \triv; a. \inr\; h(a)\}\]

To show that $\Nat$ is an initial algebra, we must show that for every
$\Nat$-algebra
$\alpha: 1 + A \to A$, there exists a unique $\Nat$-homomorphism $!: \Nat \to A$
such that the following diagram commutes (note that the order of
quantifications expressed in the previous sentence is not inherently clear in
the diagram, and must be considered to get a full understanding of the
diagram.)

\[
\begin{tikzcd}
1+\Nat \arrow{d}{\{\z, \s\}} \arrow[dashed]{r}{1+!} & 1+A \arrow{d}{\alpha}\\
\Nat \arrow[dashed]{r}{!} & A
\end{tikzcd}
\]

Let's consider the requirements on $!$ for the diagram to commute.

\[! \z = \alpha_0 \]
\[! \s(x) = \alpha_1(! x)\]

where the left sides correspond to following the path $! \comp \{\z, \s\}$
and the right sides correspond to following $\alpha \comp 1 + !$. Note that
these two equations match the $\beta$ rules for $\rec$, so we can define
$! \defeq \rec[A](\alpha_0; \alpha_1)$ or simply $! \defeq \rec[A](\alpha)$.
As we see above, the $\beta$ rules for $\rec$ imply
commutation of the diagram. Uniqueness of $!$ follows from the $\eta$ rule
for $\rec$.

It's worth noting that commuting diagrams hide exactly the type of equality
that is being discussed, which is quite
important in HoTT. For $\Nat$, for example, uniqueness of $!$ holds ``on
the nose,'' while, in general, uniqueness may be only up to higher homotopy.

\section{$F$-algebras}
The above discussion can be generalized to any functor $F$. A functor is
a mapping between categories $C$ and $D$. Functors act on objects in a
category and the morphisms between them, i.e. for all objects $X \in C$,
$F(X) \in D$, and for all morphisms $f: X \to Y$ between objects $X$ and $Y$
in $C$, $F(f): F(X) \to F(Y)$. 
Functors respect identity and composition:
  \begin{enumerate}
  \item For every object $X \in C$, $F(\id_X) = \id_{F(X)}$
  \item For all morphisms $f: X \to Y$ and $g: Y \to Z$, 
    $F(g\comp f) = F(g)\comp F(f)$
  \end{enumerate}
\cite{WikiFunctor}

For example, $F_{\Nat}(C) \defeq 1 + C$ is a functor. We check that $F_\Nat$
preserves identities and composition. Let $X$ be an object of $C$.
\[F_\Nat(\id_X) = 1 + \id_X = \{\triv, \id_X\}\]
which is indeed an identity
on $1 + X$. Let $f: X\to Y, g: Y \to Z$ be morphisms between objects of $C$.
\[F_\Nat(g \comp f) = 1 + g \comp f = \{\triv, g \comp f\} =
\{\triv, g\} \comp \{\triv, f\} = (1 + g) \comp (1 + f) = F(g) \comp F(f)\]

For any functor $F$, an $F$-algebra is a mapping $F(X) \to X$. Thus,
a $\Nat$-algebra is an $F_\Nat$-algebra. $F$-algebras form categories as
$\Nat$-algebras do. For a functor $F$, objects $A$ and $B$, two $F$-algebras
$\alpha: F(A) \to A$ and $\beta: F(B) \to B$, and a morphism $h: A \to B$,
the following diagram commutes.

\[
\begin{tikzcd}
F(A) \arrow{d}{\alpha} \arrow{r}{F(h)} & F(B) \arrow{d}{\beta}\\
A \arrow{r}{h} & B
\end{tikzcd}
\]

An {\em initial} $F$-algebra is an $F$-algebra $i: F(I) \to I$ such that
for all other $F$-algebras $\alpha: F(A) \to A$, there exists a unique map
$!: I \to A$ such that the following diagram commutes.

\[
\begin{tikzcd}
F(I) \arrow{d}{i} \arrow[dashed]{r}{F(!)} & F(A) \arrow{d}{\alpha}\\
I \arrow[dashed]{r}{!} & A
\end{tikzcd}
\]

There also exists the notion of an $F$-coalgebra, which, dual to the above,
is a map $\alpha: A \to F(A)$. A final $F$-coalgebra is a mapping 
$j: J \to F(J)$ such that for all other $F$-coalgebras $\alpha: A \to F(A)$,
there exists a unique map $!: A \to J$ making the following diagram commute.

\[
\begin{tikzcd}
A \arrow{d}{\alpha} \arrow[dashed]{r}{!} & J \arrow{d}{j}\\
F(A) \arrow[dashed]{r}{!} & F(J)
\end{tikzcd}
\]

\begin{lemma}[Lambek]
If $i: F(I) \to I$ is an initial $F$-algebra, then $i$ is an isomorphism.
That is, $F(I) \equiv I$.
\end{lemma}

\begin{proof}
To show that $i$ is an isomorphism, we must exhibit an inverse
$i^{-1}: I \to F(I)$
such that $i \comp i^{-1} = \id_I$ and $i^{-1} \comp i = \id_{F(I)}$.
Consider the $F$-algebra $F(i): F(F(I)) \to F(I)$. We now treat $i$ as
homomorphism between the $F$-algebras $F(i)$ and $i$ making this diagram
commute.

\[
\begin{tikzcd}
F(F(I)) \arrow{d}{F(i)} \arrow{r}{F(i)} & F(I) \arrow{d}{i}\\
F(I) \arrow{r}{i} & I
\end{tikzcd}
\]

Since $i$ is an initial $F$-algebra, however, we also have a unique mapping
$!: I \to F(I)$ making the top half of this diagram commute.
\[
\begin{tikzcd}
F(I) \arrow[dashed]{d}{F(!)} \arrow{r}{i} & I \arrow[dashed]{d}{!}\\
F(F(I)) \arrow{d}{F(i)} \arrow{r}{F(i)} & F(I) \arrow{d}{i}\\
F(I) \arrow{r}{i} & I
\end{tikzcd}
\]

There is also a unique mapping from $I$ to $I$, which must be the identity.
This indicates that the mapping $i \comp !$ along the right side of the
diagram must be equal to $\id_I$:

\[i \comp ! = \id_I\]

We also have
\[! \comp i = F(i) \comp F(!) = F(i \comp !) = F(\id_I) = \id_{F(I)}\]
where the first equality follows from the commutativity of the upper half of
the diagram, the second and fourth follow from the properties of functors
and the third follows from the result above.
\end{proof}

This shows that for any functor $F$, the initial $F$-algebra $I$ is a fixed
point of $F$. A dual result can be proven showing that, if $J$ is the final 
$F$-coalgebra of a functor $F$, then $F(J) \equiv J$.

\section{Internalizing $\Nat$-Algebras}

Inside type theory, we can define the notion of $\Nat$-algebra as
\[
\mathsf{NatAlg} \defeq \Sigma A{:}\universe.\, ((1 + A) \to A)
\]
We can define the type of $\Nat$-homomorphisms between two $\Nat$-algebras $(A,\alpha)$ and $(B,\beta)$ as
\[
\mathsf{NatHom}(\alpha,\beta) \defeq \Sigma h{:}A \to B.\, (\beta \circ (1 + h) = h \circ \alpha)
\]
The fact that $\nu \defeq \tuple{\Nat}{\{\z, \s\}}$ is initial in the category of $\Nat$-algebras is expressed by the fact that $\mathsf{NatHom}(\nu,\alpha)$ is contractible for all $\alpha$: this means that there exists a $\Nat$-homomorphism from $\nu$ to $\alpha$ which is unique up to higher homotopy.

\section{$\W$-types}
We'd like to be able to take a functor $F$ and define the initial $F$-algebra within HoTT (if one exists). For the class of \emph{polynomial functors}, we can do this using \emph{Brouwer ordinals}, also called \emph{$\W$-types}.

$\W$-types are inspired by the mathematical concept of well-founded induction. In classical mathematics, a partially ordered set $\left< A, < \right>$ is said to be well-founded if every subset of $A$ has a $<$-minimal element (equivalently, there are no infinite descending chains). Well-founded sets are useful because they admit an induction principle:
\begin{quote}
  \textbf{Proposition (Well-Founded Induction):} \\
  Let $\left<A , <\right>$ be a well-founded set and $P(x)$ be a proposition. If for any $a \in A$ we can prove $P(a)$ by assuming $P(b)$ for all $b < a$, then $P(a)$ holds for all $a \in A$.
\end{quote}
The set of natural numbers $\left< \mathbb{N}, <\right>$ together with its usual ordering is an example of a well-founded set, and the induction principle is the familiar mathematical induction.

Classically, the proof that induction holds goes by contradiction, so this definition is unsatisfactory for a constructive theory. We will instead characterize well-founded sets as those for which we have a (constructive) induction principle.

To better understand what we mean by this, we will define $\W$-types. To form a $\W$-type, we require a type $A$ and a type family $B$ over $A$:
\[
  \infer[\W F]
      {\ctx \vdash \W x{:}A. B : \universe}
      {\ctx \vdash A : \universe & \ctx, x{:}A \vdash B : \universe}
\]
$A$ is the type of \emph{node sorts}. Each node sort represents a different way of forming an element of $\W x{:}A. B$. For example, in the case of the natural numbers, the node sorts are $\z$ and $\s$. We can think of each element of the natural numbers as a tree built from these two sorts of nodes. For example, the numbers 0 through 2 can be represented as
\begin{center}
\begin{tikzcd}
\z & \s \arrow{d} & \s \arrow{d} \\
& \z & \s \arrow{d} \\
& & \z
\end{tikzcd}
\end{center}
Another natural example is the type of binary trees. This type can be defined by two node sorts $\mathsf{node}$ and $\mathsf{leaf}$, with the elements taking the form of trees such as this:
\begin{center}
\begin{tikzcd}
{}& \mathsf{node} \arrow{dl} \arrow{dr} & \\
\mathsf{leaf} & & \mathsf{leaf} 
\end{tikzcd}
\end{center}
In order to fully specify these two types, we need to have some notion of a node's arity. This is given by the type family $B$. For each node sort $a : A$, $B(a)$ describes the \emph{branching factor} of $a$, the index type to specify the predecessors of a node of sort $a$. For example, the branching factor of the sort $\z$ or $\mathsf{leaf}$ would be $0$, the branching factor of $\s$ would be $1$, and the branching factor of $\mathsf{node}$ would be $1 + 1$. Thus we can write $\Nat$ as $\W x{:}\Bool. \caseif(x;0;1)$, where $\ttsym$ represents $\z$ and $\ffsym$ represents $\s$.

Now that we have the purposes of $A$ and $B$ in hand, we can see how to define the introduction rule for $\W x{:}A. B$. 
\[
  \infer[\W I]
    {\ctx \vdash \sup[a](x.w) : \W x{:}A. B}
    {a : A & x{:}B(a) \vdash w : \W x{:}A. B}
\]
In other words, in order to construct a node of sort $a$, we must give an element $\W x{:}A. B$ for each predecessor as specified by the branching factor $B(a)$. Note that when $B(a)$ is $0$ we can construct a new node without any predecessor information. For example, we can construct elements of the naturals as follows:
\begin{align*}
  \overline{0} &\defeq \sup[\ttsym](x.\abort{\W x{:}\Bool. \caseif(x;0;1)}(x)) \\
  \overline{1} &\defeq \sup[\ffsym](\dummy.\overline{0}) \\
  \overline{2} &\defeq \sup[\ffsym](\dummy.\overline{1})
\end{align*}

The recursor for $\W x{:}A. B$ follows the idea of well-founded recursion: in order to define the result of a function $f$ on an element $w : \W x{:}A. B$, we can assume we've already computed $f$ for all of $w$'s predecessors.
\[
  \infer[\W R]
    {\ctx, z : \W x{:}A.B \vdash \wrec[C](a,r.M)(z) : C}
    {\ctx \vdash C : \universe & \ctx, a : A, r : B(a) \to C \vdash M : C}
\]
In the hypothesis, we assume that we are dealing with a node of type $a$ and that we have the value $r(b)$ for each $b : B(a)$ indexing a predecessor. We use this information to construct the value $M$ of the recursor at the current node. The recursor comes with the compuation rule
\[
  \wrec[C](a,r.M)(\sup[a](w)) \jdeq [a,\lambda z. \wrec[C](a,r.M)(w(z))/a,r]M
\]
which, as expected, gives the value of $\wrec[C](a,r.M)$ on $\sup[a](w)$ in terms of the value on each predecessor $w(z)$ for $z : B(a)$.

The dependent eliminator has a similar form, expressing the idea of well-founded induction.
\[
  \infer[\W E]
     {\ctx, z : \W x{:}A.B \vdash \wind[x.P](a,p,h.M) : P(z)}
     {\ctx, z : \W x{:}A.B \vdash P : \universe &
      \ctx, a{:}A, p : B(a) \to \W x{:}A.B, h : \prod_{b : B(a)} P(p(b))
       \vdash M : P(\sup[a](p))}
\]
Here, in order to formulate the hypothesis, we need to assume the additional data $p : B(a) \to \W x{:}A.B$ which gives us the predecessors of the element we are considering. The computation rule takes the form
\[
  \wind[x.P](a,p,h.M)(\sup[a](w)) = [a,w,\lambda z. \wind[x.P](a,p,h.M)(w(z))/a,p,h]M
\]
In general, we can only assert that this computation rule holds propositionally.

Each $\W$-type determines a functor, in particular a \emph{polynomial functor}. This is a functor of the form $F(X) = \Sigma a{:}A. (B(a) \to X)$ for some type $A$ and type family $B$. We can see that the $\W$-type $\W x{:}A.B$ defines an $F$-algebra where $F(X) \defeq \Sigma a{:}A. (B(a) \to X)$: we have $\lambda \tuple{a}{w}. \sup[a](w) : F(X) \to X$. The map $\lambda \tuple{a}{w}. \sup[a](w)$ is in fact an equivalence, and $\W x{:}A.B$ is a homotopy-initial $F$-algebra.

In the case of our $\W$-type definition of $\Nat$, observe that the functor determined by $\W x{:}\Bool. \caseif(x;0;1)$ is $F(X) = \Sigma b{:}\Bool. (\caseif(b;0;1) \to X)$. One can check that $\Sigma b{:}\Bool. (\caseif(b;0;1) \to X) \simeq 1 + X$. Thus, this type satisfies the equation $F(X) = 1 + X$, our original definition of a $\Nat$-algebra.

\bibliographystyle{plain}
\bibliography{hott_references}

\end{document}