# HoTT/book

no change

1 parent 8ed8a38 commit 9f958ac3f7b03d6bc2f63ba1788fb40e5a9b6970 petera02 committed Dec 5, 2012
Showing with 287 additions and 6 deletions.
1. +269 −0 basics.tex
2. +6 −3 categories.tex
3. +6 −3 macros.tex
4. +6 −0 references.bib
 @@ -1,6 +1,275 @@ \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:
 @@ -141,10 +141,11 @@ \section{Categories and precategories} We call this a \textbf{(partial) order} or a \textbf{poset}. \end{eg} -\begin{eg}\label{ct:rigid} +\begin{eg}\label{ct:gaunt} If $A$ is a category, then $A_0$ is a set if and only if for any $a,b:A_0$, the type $a\cong b$ is a mere proposition. - This is equivalent to saying that every isomorphism in $A$ is an identity; thus it is rather stronger than the classical notion of skeletal'' category; one might call a category of this sort \textbf{rigid}. - There is not really any notion of skeletality'' in our theory, unless one considers \autoref{ct:category} itself to be such. + This is equivalent to saying that every isomorphism in $A$ is an identity; thus it is rather stronger than the classical notion of skeletal'' category. + Categories of this sort are sometimes called \textbf{gaunt}. + There is not really any notion of skeletality'' for our categories, unless one considers \autoref{ct:category} itself to be such. \end{eg} \begin{eg}\label{ct:discrete} @@ -798,6 +799,8 @@ \section*{Notes} The usefulness of a definition of categories of this sort, where the type of objects contains all the categorical isomorphisms, was first strongly emphasized (in the context of set-based definitions of higher categories) by Charles Rezk~\cite{rezk01css}. +The term gaunt'' (\autoref{ct:gaunt}) was introduced by Barwick and Schommer-Pries~\cite{bsp12infncats}. + \section*{Exercises} \label{sec:ct:exercises}
 @@ -21,11 +21,12 @@ \let\rev\opp %%% Transport %%% -\newcommand{\trans}[2]{\ensuremath{{#1}_{\#}\left({#2}\right)}\xspace} +\newcommand{\trans}[2]{\ensuremath{{#1}_{\#}\!\left({#2}\right)}\xspace} +\newcommand{\transf}[1]{\ensuremath{{#1}_{\#}}\xspace} %%% Map on paths %%% -\newcommand{\map}[2]{\ensuremath{{#1}_{*}\left({#2}\right)}\xspace} -\newcommand{\mapdep}[2]{\ensuremath{{#1}_{**}\left({#2}\right)}\xspace} +\newcommand{\map}[2]{\ensuremath{{#1}_{*}\!\left({#2}\right)}\xspace} +\newcommand{\mapdep}[2]{\ensuremath{{#1}_{**}\!\left({#2}\right)}\xspace} %%% Identity functions %%% \newcommand{\idfunc}[1][]{\ensuremath{\mathsf{id}_{#1}}\xspace} @@ -38,6 +39,8 @@ \newcommand{\set}{\ensuremath{\mathsf{Set}}\xspace} \newcommand{\prop}{\ensuremath{\mathsf{Prop}}\xspace} +%%% Projections out of dependent sums %%% +\newcommand{\proj}[1]{\ensuremath{\mathsf{pr}_{#1}}\xspace} %%%% THEOREM ENVIRONMENTS %%%%
 @@ -23,3 +23,9 @@ @ARTICLE{rezk01css fjournal = {Transactions of the American Mathematical Society}, issn = {0002-9947} } + +@Unpublished{bsp12infncats, + author = {Clark Barwick and Christopher Schommer-Pries}, + title = {On the Unicity of the Homotopy Theory of Higher Categories}, + note = {arXiv:1112.0040}} +