diff --git a/basics.tex b/basics.tex index e51a62856..b2a1a3315 100644 --- a/basics.tex +++ b/basics.tex @@ -159,7 +159,7 @@ \chapter{Homotopy type theory} %% (Obviously, the %% notation ``$\id[A]{x}{y}$'' has its limitations here. The style %% $\idtype[A]{x}{y}$ is only slightly better in iterations: -%% $\idtype[{\idtype[{\idtype[A]{x}{y}}]{p}{q}}]{r}{s}$.) +%% $\idtype[{\idtype[{\idtype[A]{x}{y}}]{p}{q}}]{r}{s}$). An important difference between homotopy type theory and classical homotopy theory is that homotopy type theory provides a \emph{synthetic} \index{synthetic mathematics}% @@ -203,7 +203,7 @@ \chapter{Homotopy type theory} The ``conversion rule''~\eqref{eq:Jconv} is less familiar in the context of proof by induction on natural numbers, but there is an analogous notion in the related concept of definition by recursion. If a sequence\index{sequence} $(a_n)_{n\in \mathbb{N}}$ is defined by giving $a_0$ and specifying $a_{n+1}$ in terms of $a_n$, then in fact the $0^{\mathrm{th}}$ term of the resulting sequence \emph{is} the given one, and the given recurrence relation relating $a_{n+1}$ to $a_n$ holds for the resulting sequence. -(This may seem so obvious as to not be worth saying, but if we view a definition by recursion as an algorithm\index{algorithm} for calculating values of a sequence, then it is precisely the process of executing that algorithm.) +(This may seem so obvious as to not be worth saying, but if we view a definition by recursion as an algorithm\index{algorithm} for calculating values of a sequence, then it is precisely the process of executing that algorithm). The rule~\eqref{eq:Jconv} is analogous: it says that if we define an object $f(p)$ for all $p:x=y$ by specifying what the value should be when $p$ is $\refl{x}:x=x$, then the value we specified is in fact the value of $f(\refl{x})$. This induction principle endows each type with the structure of an $\infty$-groupoid\index{.infinity-groupoid@$\infty$-groupoid}, and each function between two types the structure of an $\infty$-functor\index{.infinity-functor@$\infty$-functor} between two such groupoids. This is interesting from a mathematical point of view, because it gives a new way to work with @@ -238,7 +238,7 @@ \section{Types are higher groupoids} \[ \prd{A:\UU}{x,y:A} (x= y)\to(y= x). \] The proof of \autoref{lem:opp} will consist of constructing an element of this type, i.e.\ deriving the judgment $f:\prd{A:\UU}{x,y:A} (x= y)\to(y= x)$ for some $f$. We then introduce the notation $\opp{(\blank)}$ for this element $f$, in which the arguments $A$, $x$, and $y$ are omitted and inferred from context. -(As remarked in \autoref{sec:types-vs-sets}, the secondary statement ``$\opp{\refl{x}}\jdeq\refl{x}$ for each $x:A$'' should be regarded as a separate judgment.) +(As remarked in \autoref{sec:types-vs-sets}, the secondary statement ``$\opp{\refl{x}}\jdeq\refl{x}$ for each $x:A$'' should be regarded as a separate judgment). \begin{proof}[First proof] Assume given $A:\UU$, and @@ -347,7 +347,7 @@ \section{Types are higher groupoids} The asymmetrical computation rules can sometimes be convenient when doing formalized mathematics, as they allow the computer to simplify more things automatically. However, in informal mathematics, and arguably even in the formalized case, it can be confusing to have a concatenation operation which behaves asymmetrically and to have to remember which side is the ``special'' one. Treating both sides symmetrically makes for more robust proofs; this is why we have given the proof that we did. -(However, this is admittedly a stylistic choice.) +(However, this is admittedly a stylistic choice). The table below summarizes the ``equality'', ``homotopical'', and ``higher-groupoid" points of view on what we have done so far. \begin{center} @@ -371,7 +371,7 @@ \section{Types are higher groupoids} a &= b & \text{(by $p$)}\\ &= c &\text{(by $q$)} \\ &= d &\text{(by $r$)}. \end{align*} In either case, the notation indicates construction of the element $(p\ct q)\ct r: (a=d)$. -(We choose left-associativity for concreteness, although in view of \autoref{thm:omg}\ref{item:omg4} below it makes little difference.) +(We choose left-associativity for concreteness, although in view of \autoref{thm:omg}\ref{item:omg4} below it makes little difference). If it should happen that $b$ and $c$, say, are judgmentally equal, then we may write \begin{align*} a &= b & \text{(by $p$)}\\ &\jdeq c \\ &= d &\text{(by $r$)} @@ -383,7 +383,7 @@ \section{Types are higher groupoids} Now, because of proof-relevance, we can't stop after proving ``symmetry'' and ``transitivity'' of equality: we need to know that these \emph{operations} on equalities are well-behaved. (This issue is invisible in set theory, where symmetry and transitivity are mere \emph{properties} of equality, rather than structure on -paths.) +paths). From the homotopy-theoretic point of view, concatenation and inversion are just the ``first level'' of higher groupoid structure --- we also need coherence\index{coherence} laws on these operations, and analogous operations at higher dimensions. For instance, we need to know that concatenation is \emph{associative}, and that inversion provides \emph{inverses} with respect to concatenation. @@ -613,7 +613,7 @@ \section{Types are higher groupoids} &\jdeq \opp{\refl{\refl{a}}} \ct \alpha \ct \refl{\refl{a}} \ct \opp{\refl{\refl a}} \ct \beta \ct \refl{\refl{a}}\\ &= \alpha \ct \beta. \end{align*} -(Recall that $\mathsf{ru}_{\refl{a}} \jdeq \mathsf{lu}_{\refl{a}} \jdeq \refl{\refl{a}}$, by the computation rule for path induction.) +(Recall that $\mathsf{ru}_{\refl{a}} \jdeq \mathsf{lu}_{\refl{a}} \jdeq \refl{\refl{a}}$, by the computation rule for path induction). On the other hand, we can define another horizontal composition analogously by \[ \alpha\hct'\beta\ \defeq\ (p\leftwhisker \beta)\ct (\alpha\rightwhisker s). @@ -1073,7 +1073,7 @@ \section{Homotopies and equivalences} \end{equation} is poorly behaved. For instance, for a single function $f:A\to B$ there may be multiple unequal inhabitants of~\eqref{eq:qinvtype}. -(This is closely related to the observation in higher category theory that often one needs to consider \emph{adjoint} equivalences\index{adjoint!equivalence} rather than plain equivalences.) +(This is closely related to the observation in higher category theory that often one needs to consider \emph{adjoint} equivalences\index{adjoint!equivalence} rather than plain equivalences). For this reason, we give~\eqref{eq:qinvtype} the following historically accurate, but slightly de\-rog\-a\-to\-ry-sounding name instead. \begin{defn}\label{defn:quasi-inverse} @@ -1678,7 +1678,7 @@ \section{Universes and the univalence axiom} \index{identity!function}% \index{function!identity}% Note that the identity function $\idfunc[\type]:\type\to\type$ may be regarded as a type family indexed by the universe \type; it assigns to each type $X:\type$ the type $X$ itself. - (When regarded as a fibration, its total space is the type $\sm{A:\type}A$ of ``pointed types''; see also \autoref{sec:object-classification}.) + (When regarded as a fibration, its total space is the type $\sm{A:\type}A$ of ``pointed types''; see also \autoref{sec:object-classification}). Thus, given a path $p:A =_\type B$, we have a transport\index{transport} function $\transf{p}:A \to B$. We claim that $\transf{p}$ is an equivalence. But by induction, it suffices to assume that $p$ is $\refl A$, in which case $\transf{p} \jdeq \idfunc[A]$, which is an equivalence by \autoref{eg:idequiv}. @@ -1896,12 +1896,12 @@ \section{Coproducts} We now consider our first example of a \emph{positive} type former. \index{type!positive}\index{positive!type}% Again informally, a positive type is one which is ``presented'' by certain constructors, with the universal property of a presentation\index{presentation!of a positive type by its constructors} being expressed by its elimination rule. -(Categorically speaking, a positive type has a ``mapping out'' universal property, while a negative type has a ``mapping in'' universal property.) +(Categorically speaking, a positive type has a ``mapping out'' universal property, while a negative type has a ``mapping in'' universal property). Because computing with presentations is, in general, an uncomputable problem, for positive types we cannot always expect a straightforward characterization of the identity type. However, in many particular cases, a characterization or partial characterization does exist, and can be obtained by the general method that we introduce with this example. (Technically, our chosen presentation of cartesian products and $\Sigma$-types is also positive. -However, because these types also admit a negative presentation which differs only slightly, their identity types have a direct characterization that does not require the method to be described here.) +However, because these types also admit a negative presentation which differs only slightly, their identity types have a direct characterization that does not require the method to be described here). Consider the coproduct type $A+B$, which is ``presented'' by the injections $\inl:A\to A+B$ and $\inr:B\to A+B$. Intuitively, we expect that $A+B$ contains exact copies of $A$ and $B$ disjointly, so that we should have @@ -2326,7 +2326,7 @@ \section{Universal properties} \begin{proof} We define the quasi-inverse by sending $(g,h)$ to $\lam{x}(g(x),h(x))$. (Technically, we have used the induction principle for the cartesian product $(X\to A)\times (X\to B)$, to reduce to the case of a pair. - From now on we will often apply this principle without explicit mention.) + From now on we will often apply this principle without explicit mention). Now given $f:X\to A\times B$, the round-trip composite yields the function \begin{equation} @@ -2394,7 +2394,7 @@ \section{Universal properties} \end{itemize} Thus, \autoref{thm:ttac} says that not only is the axiom of choice ``true'', its antecedent is actually equivalent to its conclusion. (On the other hand, the classical\index{mathematics!classical} mathematician may find that~\eqref{eq:sigma-ump-map} does not carry the usual meaning of the axiom of choice, since we have already specified the values of $g$, and there are no choices left to be made. -We will return to this point in \autoref{sec:axiom-choice}.) +We will return to this point in \autoref{sec:axiom-choice}). The above universal property for pair types is for ``mapping in'', which is familiar from the category-theoretic notion of products. However, pair types also have a universal property for ``mapping out'', which may look less familiar. @@ -2598,14 +2598,14 @@ \section{Universal properties} \begin{ex}\label{ex:equality-reflection} Suppose we add to type theory the \emph{equality reflection rule} which says that if there is an element $p:x=y$, then in fact $x\jdeq y$. Prove that for any $p:x=x$ we have $p\jdeq \refl{x}$. - (This implies that every type is a \emph{set} in the sense to be introduced in \autoref{sec:basics-sets}; see \autoref{sec:hedberg}.) + (This implies that every type is a \emph{set} in the sense to be introduced in \autoref{sec:basics-sets}; see \autoref{sec:hedberg}). \end{ex} \begin{ex} Show that \autoref{thm:transport-is-ap} can be strengthened to \[\transfib{B}{p}{{\blank}} =_{B(x)\to B(y)} \idtoeqv(\apfunc{B}(p))\] without using function extensionality. - (In this and other similar cases, the apparently weaker formulation has been chosen for readability and consistency.) + (In this and other similar cases, the apparently weaker formulation has been chosen for readability and consistency). \end{ex} \begin{ex}\label{ex:strong-from-weak-funext} diff --git a/categories.tex b/categories.tex index c4d9d24aa..9d98ecd40 100644 --- a/categories.tex +++ b/categories.tex @@ -230,7 +230,7 @@ \section{Categories and precategories} \indexdef{fundamental!pregroupoid}% \indexsee{pregroupoid, fundamental}{fundamental pregroupoid}% of $X$. - (In fact, we have met it already in \autoref{sec:van-kampen}; see also \autoref{ex:rezk-vankampen}.) + (In fact, we have met it already in \autoref{sec:van-kampen}; see also \autoref{ex:rezk-vankampen}). \end{eg} \begin{eg}\label{ct:hoprecat} @@ -446,7 +446,7 @@ \section{Functors and transformations} \end{proof} The equality in \autoref{ct:functor-assoc} is likewise not definitional. -(Composition of functions is definitionally associative, but the axioms that go into a functor must also be composed, and this breaks definitional associativity.) For this reason, we need also to know about \emph{coherence}\index{coherence} for associativity. +(Composition of functions is definitionally associative, but the axioms that go into a functor must also be composed, and this breaks definitional associativity). For this reason, we need also to know about \emph{coherence}\index{coherence} for associativity. \begin{lem}\label{ct:pentagon} \index{associativity!of functor composition!coherence of}% @@ -672,7 +672,7 @@ \section{Equivalences} This is an important advantage of our category theory over set-based approaches. With a purely set-based definition of category, the statement ``every fully faithful and essentially surjective functor is an equivalence of categories'' is equivalent to the axiom of choice \choice{}. Here we have it for free, as a category-theoretic version of the principle of unique choice (\autoref{sec:unique-choice}). -(In fact, this property characterizes categories among precategories; see \autoref{sec:rezk}.) +(In fact, this property characterizes categories among precategories; see \autoref{sec:rezk}). On the other hand, the following characterization of equivalences of categories is perhaps even more useful. @@ -773,7 +773,7 @@ \section{Equivalences} \circ g\\ &= g. \end{align*} - (There are lemmas needed here regarding the compatibility of \idtoiso and whiskering, which we leave it to the reader to state and prove.) + (There are lemmas needed here regarding the compatibility of \idtoiso and whiskering, which we leave it to the reader to state and prove). Thus, $F_{a,a'}$ is an equivalence, so $F$ is fully faithful; i.e.~\ref{item:ct:ipc1} holds. Now the composite~\ref{item:ct:ipc1}$\to$\ref{item:ct:ipc2}$\to$\ref{item:ct:ipc1} is equal to the identity since~\ref{item:ct:ipc1} is a mere proposition. @@ -841,7 +841,7 @@ \section{Equivalences} \item identities $\id{\trans {(P_{a,a})} {1_a}}{1_{\trans {P_0} a}}$ and \narrowequation{\id{\trans {(P_{a,c})} {gf}}{\trans {(P_{b,c})} g \circ \trans {(P_{a,b})} f}.} \end{itemize} - (Again, we use the fact that the identity types of hom-sets are mere propositions.) + (Again, we use the fact that the identity types of hom-sets are mere propositions). However, by univalence, this is equivalent to giving \begin{itemize} \item an equivalence of types $F_0:\eqv{A_0}{B_0}$, @@ -1099,7 +1099,7 @@ \section{Strict categories} \indexsee{monic}{monomorphism} \begin{itemize} \item Its objects consist of an object $y:A$ and a monomorphism $m:\hom_A(y,x)$. - (As usual, $m:\hom_A(y,x)$ is a \define{monomorphism} (or is \define{monic}) if $(m\circ f = m\circ g) \Rightarrow (f=g)$.) + (As usual, $m:\hom_A(y,x)$ is a \define{monomorphism} (or is \define{monic}) if $(m\circ f = m\circ g) \Rightarrow (f=g)$). \item Its morphisms from $(y,m)$ to $(z,n)$ are arbitrary morphisms from $y$ to $z$ in $A$ (not necessarily respecting $m$ and $n$). \end{itemize} An equality $(y,m)=(z,n)$ of objects in $\mathsf{mono}(A,x)$ consists of an equality $p:y=z$ and an equality $\trans{p}{m}=n$, which by \autoref{ct:idtoiso-trans} is equivalently an equality $m=n\circ \idtoiso(p)$. @@ -1565,7 +1565,7 @@ \section{The Rezk completion} This follows by path induction on $p$ and the third constructor. The type $\widehat A_0$ will be the type of objects of $\widehat A$; we now build all the rest of the structure. - (The following proof is of the sort that can benefit a lot from the help of a computer proof assistant:\index{proof!assistant} it is wide and shallow with many short cases to consider, and a large part of the work consists of writing down what needs to be checked.) + (The following proof is of the sort that can benefit a lot from the help of a computer proof assistant:\index{proof!assistant} it is wide and shallow with many short cases to consider, and a large part of the work consists of writing down what needs to be checked). \mentalpause @@ -1661,7 +1661,7 @@ \section{The Rezk completion} That is, for all $x:\widehat A$ we want there to merely exist an $a:A$ such that $Ia\cong x$. As always, we argue by induction on $x$, and since the goal is a mere proposition, all but the first constructor are trivial. But if $x$ is $ia$, then of course we have $a:A$ and $Ia\jdeq ia$, hence $Ia \cong ia$. - (Note that if we were trying to prove $I$ to be \emph{split} essentially surjective, we would be stuck, because we know nothing about equalities in $A_0$ and thus have no way to deal with any further constructors.) + (Note that if we were trying to prove $I$ to be \emph{split} essentially surjective, we would be stuck, because we know nothing about equalities in $A_0$ and thus have no way to deal with any further constructors). \end{proof} We call the construction $A\mapsto \widehat A$ the \define{Rezk completion}, diff --git a/equivalences.tex b/equivalences.tex index 62b5072e6..0cb47d123 100644 --- a/equivalences.tex +++ b/equivalences.tex @@ -497,7 +497,7 @@ \section{On the definition of equivalences} We have shown that all three definitions of equivalence satisfy the three desirable properties and are pairwise equivalent: \[ \iscontr(f) \eqvsym \ishae(f) \eqvsym \biinv(f). \] (There are yet more possible definitions of equivalence, but we will stop with these three. -See \autoref{ex:brck-qinv} and the exercises in this chapter for some more.) +See \autoref{ex:brck-qinv} and the exercises in this chapter for some more). Thus, we may choose any one of them as ``the'' definition of $\isequiv (f)$. For definiteness, we choose to define \[ \isequiv(f) \defeq \ishae(f).\] @@ -519,7 +519,7 @@ \section{Surjections and embeddings} or a \define{bijection}. \indexdef{bijection}% \indexsee{function!bijective}{bijection}% -(We avoid these words for types that are not sets, since in homotopy theory and higher category theory they often denote a stricter notion of ``sameness'' than homotopy equivalence.) +(We avoid these words for types that are not sets, since in homotopy theory and higher category theory they often denote a stricter notion of ``sameness'' than homotopy equivalence). In set theory, a function is a bijection just when it is both injective and surjective. The same is true in type theory, if we formulate these conditions appropriately. For clarity, when dealing with types that are not sets, we will speak of \emph{embeddings} instead of injections. @@ -1036,7 +1036,7 @@ \section{Univalence implies function extensionality} Give a characterization of this type analogous to \autoref{lem:qinv-autohtpy}. Can you give an example showing that this type is not generally a mere proposition? - (This will be easier after \autoref{cha:hits}.) + (This will be easier after \autoref{cha:hits}). \end{ex} \begin{ex}\label{ex:symmetric-equiv} diff --git a/errata.tex b/errata.tex index 9b9ec7cfb..cddf3f3a1 100644 --- a/errata.tex +++ b/errata.tex @@ -170,7 +170,7 @@ \autoref{sec:types-vs-sets} & 182-gb29ea2f & Change notation $a\jdeq_A b$ to $a\jdeq b : A$, to match that used in \autoref{cha:rules}. - (Neither are used anywhere else in the book.)\\ + (Neither are used anywhere else in the book).\\ % \autoref{sec:types-vs-sets} & 154-g42698c2 @@ -477,7 +477,7 @@ % \autoref{lem:quotient-when-canonical-representatives} & 514-g18ade45 - & Instead of ``is the set-quotient of $A$ by $\eqr$'', the statement should say ``satisfies the universal property of the set-quotient of $A$ by~$\eqr$, and hence is equivalent to it.'' + & Instead of ``is the set-quotient of $A$ by $\eqr$'', the statement should say ``satisfies the universal property of the set-quotient of $A$ by~$\eqr$, and hence is equivalent to it''. In the proof, the second displayed equation should be $e'(g, s) (x,p) \defeq g(x)$. The fourth displayed equation should be $e(e'(g, s)) \jdeq e(g \circ \proj{1}) \jdeq (g \circ \proj{1} \circ q, {\nameless})$, the fifth should be $g(\proj{1}(q(x))) \jdeq g(r(x)) = g(x)$, and the proof should conclude with ``$g$ respects $\eqr$ by the assumption $s$''.\\ % @@ -569,7 +569,7 @@ % \autoref{thm:ordord} & 140-g55de417 - & The second sentence of the proof should say ``By well-founded induction on $A$, suppose $\ordsl A b$ is accessible for all $b0$ that there exist types which are not $n$-types. In \autoref{cha:homotopy}, however, we will show that the $(n+1)$-sphere $\Sn^{n+1}$ is not an $n$-type. -(Kraus has also shown that the $n^{\mathrm{th}}$ nested univalent universe is also not an $n$-type, without using any higher inductive types.) +(Kraus has also shown that the $n^{\mathrm{th}}$ nested univalent universe is also not an $n$-type, without using any higher inductive types). Moreover, in \autoref{sec:whitehead} will give an example of a type that is not an $n$-type for \emph{any} (finite) number $n$. We begin the general theory of $n$-types by showing they are closed under certain operations and constructors. @@ -496,7 +496,7 @@ \section{Truncations} \end{proof} (This construction fails for $n=-2$, but in that case we can simply define $\trunc{-2}{A}\defeq \unit$ for all $A$. -From now on we assume $n\ge -1$.) +From now on we assume $n\ge -1$). \index{induction principle!for truncation}% To show the desired universal property of the $n$-truncation, we need the induction principle. @@ -534,7 +534,7 @@ \section{Truncations} Namely, if $E$ is an $n$-type and $g,g':\trunc nA\to{}E$ are such that $g(\tproj na)=g'(\tproj na)$ for every $a:A$, then $g(x)=g'(x)$ for all $x:\trunc nA$, since the type $g(x)=g'(x)$ is an $n$-type. Thus, $g=g'$. -(In fact, this uniqueness principle holds more generally when $E$ is an $\nplusone$-type.) +(In fact, this uniqueness principle holds more generally when $E$ is an $\nplusone$-type). This yields the following universal property. \begin{lem}[Universal property of truncations]\label{thm:trunc-reflective} @@ -552,7 +552,7 @@ \section{Truncations} In categorical language, this says that the $n$-types form a \emph{reflective subcategory} of the category of types. \index{reflective!subcategory}% -(To state this fully precisely, one ought to use the language of $(\infty,1)$-categories.) +(To state this fully precisely, one ought to use the language of $(\infty,1)$-categories). \index{.infinity1-category@$(\infty,1)$-category}% In particular, this implies that the $n$-truncation is functorial: given $f:A\to B$, applying the recursion principle to the composite $A\xrightarrow{f} B \to \trunc n B$ yields a map $\trunc n f: \trunc n A \to \trunc n B$. @@ -956,7 +956,7 @@ \section{Colimits of \texorpdfstring{$n$}{n}-types} {t \, j \, \beta \, g \, z} } \end{equation*} - (For brevity, we are omitting the parentheses around the arguments of functions.) + (For brevity, we are omitting the parentheses around the arguments of functions). On the other hand, for the left-bottom composite, the homotopy is $\apfunc{t}$ applied to~\eqref{eq:mapofspans-htpy}. Since $\apfunc{}$ respects path-concatenation, this is equal to \begin{equation*} @@ -1106,7 +1106,7 @@ \section{Connectedness} \begin{rmk}\label{rmk:connectedness-indexing} While our notion of $n$-connectedness for types agrees with the standard notion in homotopy theory, our notion of $n$-connectedness for \emph{functions} is off by one from a common indexing in classical homotopy theory. Whereas we say a function $f$ is $n$-connected if all its fibers are $n$-connected, some classical homotopy theorists would call such a function $(n+1)$-connected. - (This is due to a historical focus on \emph{cofibers} rather than fibers.) + (This is due to a historical focus on \emph{cofibers} rather than fibers). \end{rmk} We now observe a few closure properties of connected maps. @@ -1815,7 +1815,7 @@ \section{Modalities} Conditions~\ref{item:modal2} and~\ref{item:modal3} are very similar to \autoref{thm:modal-char}\ref{item:mchr2}, but phrased using $\modal B(z)$ rather than assuming $B$ to be valued in $\P$. This allows us to state the condition purely in terms of the operation $\modal$, rather than requiring the predicate $P:\type\to\prop$ to be given in advance. (It is not entirely satisfactory, since we still have to refer to $P$ not-so-subtly in clause~\ref{item:modal4}. -We do not know whether~\ref{item:modal4} follows from~\ref{item:modal1}--\ref{item:modal3}.) +We do not know whether~\ref{item:modal4} follows from~\ref{item:modal1}--\ref{item:modal3}). However, the stronger-looking property of \autoref{thm:modal-char}\ref{item:mchr2} follows from \autoref{defn:modality}\ref{item:modal2} and~\ref{item:modal3}, since for any $C:\modal A \to \modaltype$ we have $C(z) \eqvsym \modal C(z)$, and we can pass back across this equivalence. \index{universal!property!of a modality}% @@ -1854,7 +1854,7 @@ \section{Modalities} The name \emph{modality} comes, of course, from \emph{modal logic}\index{modal!logic}, which studies logic where we can form statements such as ``possibly $A$'' (usually written $\diamond A$) or ``necessarily $A$'' (usually written $\Box A$). The symbol $\modal$ is somewhat common for an arbitrary modal operator\index{modal!operator}. % (rather than a specific one such as $\diamond$ or $\Box$). Under the propositions-as-types principle, a modality in the sense of modal logic corresponds to an operation on \emph{types}, and \autoref{defn:modality} seems a reasonable candidate for how such an operation should be defined. -(More precisely, we should perhaps call these \emph{idempotent, monadic} modalities; see the Notes.) +(More precisely, we should perhaps call these \emph{idempotent, monadic} modalities; see the Notes). \index{idempotent!modality}% As mentioned in \autoref{subsec:when-trunc}, we may in general use adverbs\index{adverb} to speak informally about such modalities, such as ``merely''\index{merely} for the propositional truncation and ``purely''\index{purely} for the identity modality \index{identity!modality}% @@ -1915,7 +1915,7 @@ \section{Modalities} There exist ``purely functional'' programming languages, such as Haskell\index{Haskell}, in which it is technically only possible to write pure functions: side effects are represented by applying ``monads'' to output types. For instance, a function of type $\mathsf{Int}\to\mathsf{Int}$ is pure, while a function of type $\mathsf{Int}\to \mathsf{IO}(\mathsf{Int})$ may perform input and output along the way to computing its result; the operation $\mathsf{IO}$ is a monad. \index{purely}% -(This is the origin of our use of the adverb ``purely'' for the identity monad, since it corresponds computationally to pure functions with no side-effects.) +(This is the origin of our use of the adverb ``purely'' for the identity monad, since it corresponds computationally to pure functions with no side-effects). The modalities we have considered in this chapter are all idempotent, whereas those used in functional programming rarely are, but the ideas are still closely related. @@ -1983,11 +1983,11 @@ \section{Modalities} It is known that $\choice{\infty,-1}$ is consistent with univalence, since it holds in Voevodsky's simplicial model. \begin{enumerate} \item Without using univalence, show that $\LEM{n,\infty}$ implies $\choice{n,m}$ for all $m$. - (On the other hand, in \autoref{subsec:emacinsets} we will show that $\choice{}=\choice{0,-1}$ implies $\LEM{}=\LEM{-1,-1}$.) + (On the other hand, in \autoref{subsec:emacinsets} we will show that $\choice{}=\choice{0,-1}$ implies $\LEM{}=\LEM{-1,-1}$). \item Of course, $\choice{n,m}\Rightarrow \choice{k,m}$ if $k\le n$. Are there any other implications between the principles $\choice{n,m}$? Is $\choice{n,m}$ consistent with univalence for any $m\ge -1$? - (These are open questions.)\index{open!problem} + (These are open questions).\index{open!problem} \end{enumerate} \end{ex} @@ -2007,7 +2007,7 @@ \section{Modalities} \begin{enumerate} \item Prove that the $(-1)$-connected axiom of choice implies the $n$-con\-nect\-ed axiom of choice for all $n\ge -1$. \item Are there any other implications between the $n$-connected axioms of choice and the principles $\choice{n,m}$? - (This is an open question.)\index{open!problem} + (This is an open question).\index{open!problem} \end{enumerate} \end{ex} diff --git a/homotopy.tex b/homotopy.tex index 10cf64503..13e6435d2 100644 --- a/homotopy.tex +++ b/homotopy.tex @@ -339,7 +339,7 @@ \subsection{Getting started} Then we have $\apfunc{c} : (\base=\base) \to (\Z=\Z)$, and we can define $g(p)\defeq \transfib{X\mapsto X}{\apfunc{c}(p)}{0}$. With these definitions, we can even prove that $g(\lloop^n)=n$ for any $n:\Z$, using the induction principle \autoref{thm:sign-induction} for $n$. -(We will prove something more general a little later on.) +(We will prove something more general a little later on). However, the other equality $\lloop^{g(p)}=p$ is significantly harder. The obvious thing to try is path induction, but path induction does not apply to loops such as $p:(\base=\base)$ that have \emph{both} endpoints fixed! A new idea is required, one which can be explained both in terms of classical homotopy theory and in terms of type theory. @@ -397,7 +397,7 @@ \subsection{The classical proof} \index{covering space!universal}% Now a basic fact in classical homotopy theory is that a map $E_1\to E_2$ of fibrations over $B$ which is a homotopy equivalence between $E_1$ and $E_2$ induces a homotopy equivalence on all fibers. -(We have already seen the type-theoretic version of this as well in \autoref{thm:total-fiber-equiv}.) +(We have already seen the type-theoretic version of this as well in \autoref{thm:total-fiber-equiv}). Since $\mathbb{R}$ and $P_{\base} S^1$ are both contractible topological spaces, they are homotopy equivalent, and thus their fibers $\Z$ and $\Omega(\Sn ^1)$ over the basepoint are also homotopy equivalent. \index{classical!homotopy theory|)}% @@ -937,7 +937,7 @@ \section{Fiber sequences and the long exact sequence} \index{sequence!fiber|(}% If the codomain of a function $f:X\to Y$ is equipped with a basepoint $y_0:Y$, then we refer to the fiber $F\defeq \hfib f {y_0}$ of $f$ over $y_0$ as \define{the fiber of $f$}\index{fiber}. -(If $Y$ is connected, then $F$ is determined up to mere equivalence; see \autoref{ex:unique-fiber}.) +(If $Y$ is connected, then $F$ is determined up to mere equivalence; see \autoref{ex:unique-fiber}). We now show that if $X$ is also pointed and $f$ preserves basepoints, then there is a relation between the homotopy groups of $F$, $X$, and $Y$ in the form of a \emph{long exact sequence}. We derive this by way of the \emph{fiber sequence} associated to such an $f$. @@ -1756,7 +1756,7 @@ \section{The Freudenthal suspension theorem} Since this equality is a $(2n-1)$-type, we may assume $d$ is of the form $\tproj{2n}{(x_1,r)}$ for some $x_1:X$ and $r:\merid(x_1) \ct \opp{\merid(x_0)} = p$. Now by a further path induction, we may assume that $r$ is reflexivity, and $p$ is $\merid(x_1) \ct \opp{\merid(x_0)}$. - (This is why we generalized to arbitrary $p$ above.) + (This is why we generalized to arbitrary $p$ above). Thus, we have to prove that \begin{equation} \tproj{2n}{(x_1, \refl{\merid(x_1) \ct \opp{\merid(x_0)}})} @@ -2075,7 +2075,7 @@ \subsection{Naive van Kampen} \end{narrowmultline*} % i.e., the identity function. -(To be precise, there is an implicit inductive argument needed here.) +(To be precise, there is an implicit inductive argument needed here). The other three point cases are analogous, and the path cases are trivial since all the types are sets. \end{proof} @@ -2097,7 +2097,7 @@ \subsection{Naive van Kampen} Since \autoref{thm:naive-van-kampen} asserts only a bijection of families of sets, this isomorphism $\pi_1(S^1)\cong \Z$ is likewise only a bijection of sets. We could, however, define a concatenation operation on $\code$ (by concatenating sequences) and show that $\encode$ and $\decode$ form an isomorphism respecting this structure. -(In the language of \autoref{cha:category-theory}, these would be ``pregroupoids''.) +(In the language of \autoref{cha:category-theory}, these would be ``pregroupoids''). We leave the details to the reader. \index{fundamental!group|(}% @@ -2504,7 +2504,7 @@ \section{Whitehead's theorem and Whitehead's principle} \begin{eg} Suppose we have $B:\nat\to\type$ such that for each $n$, the type $B(n)$ contains an $n$-loop\index{loop!n-@$n$-} which is not equal to $n$-fold reflexivity, say $p_n:\Omega^n(B(n),b_n)$ with $p_n \neq \refl{b_n}^n$. - (For instance, we could define $B(n)\defeq \Sn^n$, with $p_n$ the image of $1:\Z$ under the isomorphism $\pi_n(\Sn^n)\cong \Z$.) + (For instance, we could define $B(n)\defeq \Sn^n$, with $p_n$ the image of $1:\Z$ under the isomorphism $\pi_n(\Sn^n)\cong \Z$). Consider $C\defeq \prd{n:\nat} B(n)$, with the point $c:C$ defined by $c(n)\defeq b_n$. Since loop spaces commute with products, for any $m$ we have \[\eqvspaced{\Omega^m (C,c)}{\prd{n:\nat}\Omega^m(B(n),b_n)}.\] @@ -2647,7 +2647,7 @@ \section{Additional Results} $k$ is in fact $2$, our calcluation of $\pi_4(\Sn ^3)$ is constructive,\index{mathematics!constructive} like all the rest of the proofs in this chapter. (More precisely, it doesn't use any additional axioms such as \LEM{} or \choice{}, making it as constructive as -univalence and higher inductive types are.) Thus, given a +univalence and higher inductive types are). Thus, given a computational interpretation of homotopy type theory, we could run the proof on a computer to verify that $k$ is $2$. This example is quite intriguing, because it is the first calculation of a homotopy group @@ -2807,7 +2807,7 @@ \section{Additional Results} \begin{ex} \index{decidable!equality}% Prove that if $A$ is a set with decidable equality (see \autoref{defn:decidable-equality}), then its suspension $\susp A$ is a 1-type. - (It is an open question\index{open!problem} whether this is provable without the assumption of decidable equality.) + (It is an open question\index{open!problem} whether this is provable without the assumption of decidable equality). \end{ex} \begin{ex} diff --git a/induction.tex b/induction.tex index 577fb9075..a2e7ebcf4 100644 --- a/induction.tex +++ b/induction.tex @@ -52,7 +52,7 @@ \section{Introduction to inductive types} \index{free!generation of an inductive type}% Intuitively, we should understand an inductive type as being \emph{freely generated by} its constructors. That is, the elements of an inductive type are exactly what can be obtained by starting from nothing and applying the constructors repeatedly. -(We will see in \autoref{sec:identity-systems,cha:hits} that this conception has to be modified slightly for more general kinds of inductive definitions, but for now it is sufficient.) +(We will see in \autoref{sec:identity-systems,cha:hits} that this conception has to be modified slightly for more general kinds of inductive definitions, but for now it is sufficient). For instance, in the case of \bool, we should expect that the only elements are $\bfalse$ and $\btrue$. Similarly, in the case of \nat, we should expect that every element is either $0$ or obtained by applying $\suc$ to some ``previously constructed'' natural number. @@ -224,7 +224,7 @@ \section{Uniqueness of inductive types} \end{itemize} This is not identical to the definition of \nat, and it does not give rise to an identical induction principle. The induction principle of $\lst\unit$ says that for any $E:\lst\unit\to\type$ together with recurrence data $e_\nil:E(\nil)$ and $e_\cons : \prd{u:\unit}{\ell:\lst\unit} E(\ell) \to E(\cons(u,\ell))$, there exists $f:\prd{\ell:\lst\unit} E(\ell)$ such that $f(\nil)\jdeq e_\nil$ and $f(\cons(u,\ell))\jdeq e_\cons(u,\ell,f(\ell))$. -(We will see how to derive the induction principle of an inductive definition in \autoref{sec:strictly-positive}.) +(We will see how to derive the induction principle of an inductive definition in \autoref{sec:strictly-positive}). Now suppose we define $0'' \defeq \nil: \lst\unit$, and $\suc'':\lst\unit\to\lst\unit$ by $\suc''(\ell) \defeq \cons(\ttt,\ell)$. Then for any $E:\lst\unit\to\type$ together with $e_0:E(0'')$ and $e_s:\prd{\ell:\lst\unit} E(\ell) \to E(\suc''(\ell))$, we can define @@ -232,7 +232,7 @@ \section{Uniqueness of inductive types} e_\nil &\defeq e_0\\ e_\cons(\ttt,\ell,x) &\defeq e_s(\ell,x). \end{align*} -(In the definition of $e_\cons$ we use the induction principle of \unit to assume that $u$ is $\ttt$.) +(In the definition of $e_\cons$ we use the induction principle of \unit to assume that $u$ is $\ttt$). Now we can apply the induction principle of $\lst\unit$, obtaining $f:\prd{\ell:\lst\unit} E(\ell)$ such that \begin{gather*} f(0'') \jdeq f(\nil) \jdeq e_\nil \jdeq e_0\\ @@ -780,7 +780,7 @@ \section{The general syntax of inductive definitions} However, what would the computation rule for the resulting function $f:C\to P$ be? Looking at other computation rules, we would expect something like ``$f(g(\alpha)) \jdeq h(\alpha,f(\alpha))$'' for $\alpha:C\to\nat$, but as we have seen, ``$f(\alpha)$'' does not make sense. The induction principle of $C$ is even more problematic; it's not even clear how to write down the hypotheses. -(See also \autoref{ex:loop,ex:loop2}.) +(See also \autoref{ex:loop,ex:loop2}). This example suggests one restriction on inductive definitions: the domains of all the constructors must be \emph{covariant functors}\index{functor!covariant}\index{covariant functor} of the type being defined, so that we can ``apply $f$ to them'' to get the result of the ``recursive call''. In other words, if we replace all occurrences of the type being defined with a variable @@ -839,7 +839,7 @@ \section{The general syntax of inductive definitions} \[ \theta(\gamma) \defeq \neg p(\gamma)(\gamma) \quad\text{for all $\gamma:D\to\prop$} \] then from $\theta = p(\delta)$ we deduce $p(\delta)(\delta) = \neg p(\delta)(\delta)$. This is a contradiction: no proposition can be equivalent to its negation. -(Supposing $P\Leftrightarrow \neg P$, if $P$, then $\neg P$, and so $\emptyt$; hence $\neg P$, but then $P$, and so $\emptyt$.) +(Supposing $P\Leftrightarrow \neg P$, if $P$, then $\neg P$, and so $\emptyt$; hence $\neg P$, but then $P$, and so $\emptyt$). \begin{rmk} There is a question of universe size to be addressed. @@ -856,7 +856,7 @@ \section{The general syntax of inductive definitions} \index{consistency}% This counterexample suggests that we should ban an inductive type from ever appearing on the left of an arrow in the domain of its constructors, even if that appearance is nested in other arrows so as to eventually become covariant. -(Similarly, we also forbid it from appearing in the domain of a dependent function type.) +(Similarly, we also forbid it from appearing in the domain of a dependent function type). This restriction is called \define{strict positivity} \indexdef{strict!positivity}% \indexsee{positivity, strict}{strict positivity}% @@ -879,7 +879,7 @@ \section{The general syntax of inductive definitions} This is simply because we have to write it down on the page. If we want an inductive type which behaves as if it has an infinite number of constructors, we can simply parametrize one constructor by some infinite type. For instance, a constructor such as $\nat \to W \to W$ can be thought of as equivalent to countably many constructors of the form $W\to W$. -(Of course, the infinity is now \emph{internal} to the type theory, but this is as it should be for any foundational system.) +(Of course, the infinity is now \emph{internal} to the type theory, but this is as it should be for any foundational system). Similarly, if we want a constructor that takes ``infinitely many arguments'', we can allow it to take a family of arguments parametrized by some infinite type, such as $(\nat\to W) \to W$ which takes an infinite sequence\index{sequence} of elements of $W$. \index{recursion principle!for an inductive type}% @@ -947,7 +947,7 @@ \section{Generalizations of inductive types} \index{type!inductive!generalizations}% The notion of inductive type has been studied in type theory for many years, and admits of many, many generalizations: inductive type families, mutual inductive types, inductive-inductive types, inductive-recursive types, etc. In this section we give an overview of some of these, a few of which will be used later in the book. -(In \autoref{cha:hits} we will study in more depth a very different generalization of inductive types, which is particular to \emph{homotopy} type theory.) +(In \autoref{cha:hits} we will study in more depth a very different generalization of inductive types, which is particular to \emph{homotopy} type theory). Most of these generalizations involve allowing ourselves to define more than one type by induction at the same time. One very simple example of this, which we have already seen, is the coproduct $A+B$. @@ -1107,7 +1107,7 @@ \section{Identity types and identity systems} If types are viewed as like \emph{sets}, as was traditionally the case in type theory, then there are no such operations, and hence we expect there to be no elements in an inductive type other than those resulting from its constructors. In homotopy type theory, we view types as like \emph{spaces} or $\infty$-groupoids,% \index{.infinity-groupoid@$\infty$-groupoid} -in which case there are many operations on the \emph{paths} (concatenation, inversion, etc.) --- this will be important in \autoref{cha:hits} --- but there are still no operations on the \emph{objects} (elements). +in which case there are many operations on the \emph{paths} (concatenation, inversion, etc). --- this will be important in \autoref{cha:hits} --- but there are still no operations on the \emph{objects} (elements). Thus, it is still true for us that, e.g., every element of \bool is either $\bfalse$ or $\btrue$, and every element of $\nat$ is either $0$ or a successor. However, as we saw in \autoref{cha:basics}, viewing types as $\infty$-groupoids entails also viewing functions as functors, and this includes type families $B:A\to\type$. @@ -1156,7 +1156,7 @@ \section{Identity types and identity systems} Note that the equivalences~\ref{item:identity-systems1}$\Leftrightarrow$\ref{item:identity-systems2}$\Leftrightarrow$\ref{item:identity-systems3} are a version of \autoref{lem:homotopy-induction-times-3} for identity types $a_0 =_A \blank$, regarded as inductive families varying over one element of $A$. Of course,~\ref{item:identity-systems2}--\ref{item:identity-systems4} are mere propositions, so that logical equivalence implies actual equivalence. -(Condition~\ref{item:identity-systems1} is also a mere proposition, but we will not prove this.) +(Condition~\ref{item:identity-systems1} is also a mere proposition, but we will not prove this). \begin{proof} First, assume~\ref{item:identity-systems1} and let $(S,s_0)$ be a pointed predicate. diff --git a/introduction.tex b/introduction.tex index 7c502542d..c1b7afc7d 100644 --- a/introduction.tex +++ b/introduction.tex @@ -71,11 +71,11 @@ \subsection*{Homotopy type theory} \[ a:A. \] This expression is traditionally thought of as akin to: \begin{center} -``$a$ is an element of the set $A$.'' +``$a$ is an element of the set $A$''. \end{center} However, in homotopy type theory we think of it instead as: \begin{center} -``$a$ is a point of the space $A$.'' +``$a$ is a point of the space $A$''. \end{center} \index{continuity of functions in type theory@``continuity'' of functions in type theory}% Similarly, every function $f : A\to B$ in type theory is regarded as a continuous map from the space $A$ to the space $B$. @@ -90,8 +90,8 @@ \subsection*{Homotopy type theory} (It is tempting to also use the phrase \emph{homotopy type} \index{homotopy!type}% -for these objects, suggesting the dual interpretation of ``a type (as in type theory) viewed homotopically'' and ``a space considered from the point of view of homotopy theory.'' -The latter is a bit different from the classical meaning of ``homotopy type'' as an \emph{equivalence class} of spaces modulo homotopy equivalence, although it does preserve the meaning of phrases such as ``these two spaces have the same homotopy type''.) +for these objects, suggesting the dual interpretation of ``a type (as in type theory) viewed homotopically'' and ``a space considered from the point of view of homotopy theory''. +The latter is a bit different from the classical meaning of ``homotopy type'' as an \emph{equivalence class} of spaces modulo homotopy equivalence, although it does preserve the meaning of phrases such as ``these two spaces have the same homotopy type''). The idea of interpreting types as structured objects, rather than sets, has a long pedigree, and is known to clarify various mysterious aspects of type theory. For instance, interpreting types as sheaves helps explain the intuitionistic nature of type-theoretic logic, while interpreting them as partial equivalence relations or ``domains'' helps explain its computational aspects. @@ -251,7 +251,7 @@ \subsection*{Informal type theory} Indeed, many of the proofs described in this book were actually \emph{first} done in a fully formalized form in a proof assistant, and are only now being ``unformalized'' for the first time --- a reversal of the usual relation between formal and informal mathematics. One can imagine a not-too-distant future when it will be possible for mathematicians to verify the correctness of their own papers by working within the system of univalent foundations, formalized in a proof assistant, and that doing so will become as natural as typesetting their own papers in \TeX. -%(Whether this proves to be the publishers' dream or their nightmare remains to be seen.) +%(Whether this proves to be the publishers' dream or their nightmare remains to be seen). In principle, this could be equally true for any other foundational system, but we believe it to be more practically attainable using univalent foundations, as witnessed by the present work and its formal counterpart. \index{type theory!formal|)}% @@ -269,7 +269,7 @@ \subsection*{Constructivity} Accordingly, we can regard a term $a : A$ as both an element of the type $A$ (or in homotopy type theory, a point of the space $A$), and at the same time, a proof of the proposition $A$. To take an example, suppose we have sets $A$ and $B$ (discrete spaces), \index{discrete!space}% -and consider the statement ``$A$ is isomorphic to $B$.'' +and consider the statement ``$A$ is isomorphic to $B$''. In type theory, this can be rendered as: \begin{narrowmultline*} \mathsf{Iso}(A,B) \defeq \narrowbreak @@ -309,15 +309,15 @@ \subsection*{Constructivity} The new insight that makes this possible is that the system of all types, just like spaces in classical homotopy theory, is ``stratified'' according to the dimensions in which their higher homotopy structure exists or collapses. In particular, Voevodsky has found a purely type-theoretic definition of \emph{homotopy $n$-types}, corresponding to spaces with no nontrivial homotopy information above dimension $n$. -(The $0$-types are the ``sets'' mentioned previously as satisfying Lawvere's axioms\index{Lawvere}.) +(The $0$-types are the ``sets'' mentioned previously as satisfying Lawvere's axioms\index{Lawvere}). Moreover, with higher inductive types, we can universally ``truncate'' a type into an $n$-type; in classical homotopy theory this would be its $n^{\mathrm{th}}$ Postnikov\index{Postnikov tower} section.\index{n-type@$n$-type}%% With these notions in hand, the homotopy $(-1)$-types, which we call \emph{(mere) propositions}, support a logic that is much more like traditional ``intuitionistic'' logic. -(Classically, every $(-1)$-type is empty or contractible; we interpret these possibilities as the truth values ``false'' and ``true'' respectively.) +(Classically, every $(-1)$-type is empty or contractible; we interpret these possibilities as the truth values ``false'' and ``true'' respectively). The ``$(-1)$-truncated axiom of choice'' is not automatically true, but is a strong assumption with the same sorts of consequences as its counterpart in classical\index{mathematics!classical} set theory. Similarly, the ``$(-1)$-truncated law of excluded middle'' may be assumed, with many of the same consequences as in classical mathematics. Thus, the homotopical perspective reveals that classical and constructive logic can coexist, as endpoints of a spectrum of different systems, with an infinite number of possibilities in between (the homotopy $n$-types for $-1 < n < \infty$). -We may speak of ``\LEM{n}'' and ``\choice{n}'', with $\choice{\infty}$ being provable and \LEM{\infty} inconsistent with univalence, while $\choice{-1}$ and $\LEM{-1}$ are the versions familiar to classical mathematicians (hence in most cases it is appropriate to assume the subscript $(-1)$ when none is given). Indeed, one can even have useful systems in which only \emph{certain} types satisfy such further ``classical'' principles, while types in general remain ``constructive.''\index{excluded middle}\index{axiom!of choice}%% +We may speak of ``\LEM{n}'' and ``\choice{n}'', with $\choice{\infty}$ being provable and \LEM{\infty} inconsistent with univalence, while $\choice{-1}$ and $\LEM{-1}$ are the versions familiar to classical mathematicians (hence in most cases it is appropriate to assume the subscript $(-1)$ when none is given). Indeed, one can even have useful systems in which only \emph{certain} types satisfy such further ``classical'' principles, while types in general remain ``constructive''.\index{excluded middle}\index{axiom!of choice}%% It is worth emphasizing that univalent foundations does not \emph{require} the use of constructive or intuitionistic logic.\index{logic!intuitionistic}\index{logic!constructive} % Most of classical mathematics which depends on the law of excluded middle and the axiom of choice can be performed in univalent foundations, simply by assuming that these two principles hold (in their proper, $(-1)$-truncated, form). @@ -480,7 +480,7 @@ \subsection*{How to read this book} In \autoref{cha:category-theory} (Category theory), we develop some basic (1-)category theory, adhering to the principle of the univalence axiom that \emph{equality is isomorphism}. This has the pleasant effect of ensuring that all definitions and constructions are automatically invariant under equivalence of categories: indeed, equivalent categories are equal just as equivalent types are equal. -(It also has connections to higher category theory and higher topos theory.) +(It also has connections to higher category theory and higher topos theory). \autoref{cha:set-math} (Set theory) studies sets in univalent foundations. The category of sets has its usual properties, hence provides a foundation for any mathematics that doesn't need homotopical or higher-categorical structures. diff --git a/logic.tex b/logic.tex index c5705b7ec..df1f7391f 100644 --- a/logic.tex +++ b/logic.tex @@ -145,7 +145,7 @@ \section{Sets and \texorpdfstring{$n$}{n}-types} In \autoref{cha:hits,cha:homotopy} we will show that for any $n$, there are types which are not $n$-types. Note that $A$ is a 1-type exactly when for any $x,y:A$, the identity type $\id[A]xy$ is a set. -(Thus, \autoref{thm:isset-is1type} could equivalently be read as saying that the identity types of a set are also sets.) +(Thus, \autoref{thm:isset-is1type} could equivalently be read as saying that the identity types of a set are also sets). This will be the basis of the recursive definition of $n$-types we will give in \autoref{cha:hlevels}. We can also extend this characterization ``downwards'' from sets. @@ -167,7 +167,7 @@ \section{Propositions as types?} For instance, in \autoref{thm:ttac} we saw that the statement \index{axiom!of choice!type-theoretic}% \begin{equation}\label{eq:english-ac} - \parbox{\textwidth-2cm}{``If for all $x:X$ there exists an $a:A(x)$ such that $P(x,a)$, then there exists a function $g:\prd{x:A} A(x)$ such that for all $x:X$ we have $P(x,g(x))$,''} + \parbox{\textwidth-2cm}{``If for all $x:X$ there exists an $a:A(x)$ such that $P(x,a)$, then there exists a function $g:\prd{x:A} A(x)$ such that for all $x:X$ we have $P(x,g(x))$'',} \end{equation} which looks like the classical\index{mathematics!classical} \emph{axiom of choice}, is always true under this reading. This is a noteworthy, and often useful, feature of the propositions-as-types logic, but it also illustrates how significantly it differs from the classical interpretation of logic, under which the axiom of choice is not a logical truth, but an additional ``axiom''. @@ -488,7 +488,7 @@ \section{Subsets and propositional resizing} \end{equation} % as an alternative notation for $\sm{x:A} P(x)$. -(There is no technical reason not to use this notation for arbitrary $P$ as well, but such usage could be confusing due to unintended connotations.) +(There is no technical reason not to use this notation for arbitrary $P$ as well, but such usage could be confusing due to unintended connotations). If $A$ is a set, we call \eqref{eq:subset} a \define{subset} \indexdef{subset}% \indexdef{type!subset}% @@ -592,7 +592,7 @@ \section{The logic of mere propositions} \index{quantifier!existential}% The same issue arises with the $\Sigma$-type $\sm{x:A} P(x)$. This is a purely constructive interpretation of ``there exists an $x:A$ such that $P(x)$'' which remembers the witness $x$, and hence is not generally a mere proposition even if each type $P(x)$ is. -(Recall that we observed in \autoref{subsec:prop-subsets} that $\sm{x:A} P(x)$ can also be regarded as ``the subset of those $x:A$ such that $P(x)$''.) +(Recall that we observed in \autoref{subsec:prop-subsets} that $\sm{x:A} P(x)$ can also be regarded as ``the subset of those $x:A$ such that $P(x)$''). \section{Propositional truncation} @@ -621,7 +621,7 @@ \section{Propositional truncation} \end{itemize} In other words, any mere proposition which follows from (the inhabitedness of) $A$ already follows from $\brck A$. Thus, $\brck A$, as a mere proposition, contains no more information than the inhabitedness of $A$. -(There is also an induction principle for $\brck A$, but it is not especially useful; see \autoref{ex:prop-trunc-ind}.) +(There is also an induction principle for $\brck A$, but it is not especially useful; see \autoref{ex:prop-trunc-ind}). In \autoref{ex:lem-brck,ex:impred-brck,sec:hittruncations} we will describe some ways to construct $\brck{A}$ in terms of more general things. For now, we simply assume it as an additional rule alongside those of \autoref{cha:typetheory}. @@ -748,7 +748,7 @@ \section{The axiom of choice} \end{equation} \end{lem} -This corresponds to a well-known equivalent form of the classical\index{mathematics!classical} axiom of choice, namely ``the cartesian product of a family of nonempty sets is nonempty.'' +This corresponds to a well-known equivalent form of the classical\index{mathematics!classical} axiom of choice, namely ``the cartesian product of a family of nonempty sets is nonempty''. \begin{proof} By \autoref{thm:ttac}, the codomain of~\eqref{eq:ac} is equivalent to @@ -860,7 +860,7 @@ \section{When are propositions truncated?} However, it may come as a surprise to realize that the practice of \emph{informal} mathematics is often more accurately described by the untruncated forms. \index{prime number}% -For example, consider a statement like ``every prime number is either $2$ or odd.'' +For example, consider a statement like ``every prime number is either $2$ or odd''. The working mathematician feels no compunction about using this fact not only to prove \emph{theorems} about prime numbers, but also to perform \emph{constructions} on prime numbers, perhaps doing one thing in the case of $2$ and another in the case of an odd prime. The end result of the construction is not merely the truth of some statement, but a piece of data which may depend on the parity of the prime number. Thus, from a type-theoretic perspective, such a construction is naturally phrased using the induction principle for the coproduct type ``$(p=2)+(p\text{ is odd})$'', not its propositional truncation. @@ -877,7 +877,7 @@ \section{When are propositions truncated?} We may attempt to apologize for them, expunge them from final drafts, or weasel out of them with vague words like ``canonical''. The problem is exacerbated by the fact that in formalized set theory, there is technically no way to ``construct'' objects at all --- we can only prove that an object with certain properties exists. Untruncated logic in type theory thus captures some common practices of informal mathematics that the set theoretic reconstruction obscures. -(This is similar to how the univalence axiom validates the common, but formally unjustified, practice of identifying isomorphic objects.) +(This is similar to how the univalence axiom validates the common, but formally unjustified, practice of identifying isomorphic objects). On the other hand, sometimes truncated logic is essential. We have seen this in the statements of \LEM{} and \choice{}; some other examples will appear later on in the book. @@ -925,7 +925,7 @@ \section{When are propositions truncated?} \item Many statements that classically are mere propositions are no longer so in homotopy type theory. Of course, foremost among these is equality. \item On the other hand, one of the most interesting observations of homotopy type theory is that a surprising number of types are \emph{automatically} mere propositions, or can be slightly modified to become so, without the need for any truncation. - (See \autoref{thm:isprop-isprop,cha:equivalences,cha:hlevels,cha:category-theory,cha:set-math}.) + (See \autoref{thm:isprop-isprop,cha:equivalences,cha:hlevels,cha:category-theory,cha:set-math}). Thus, although these types contain no data beyond a truth value, we can nevertheless use them to construct untruncated objects, since there is no need to use the induction principle of propositional truncation. This useful fact is more clumsy to express if propositional truncation is applied to all statements by default. \item Finally, truncations are not very useful for most of the mathematics we will be doing in this book, so it is simpler to notate them explicitly when they occur. @@ -1018,7 +1018,7 @@ \section{Contractibility} \index{function extensionality}% (In fact, the statement of \autoref{thm:contr-forall} is equivalent to the function extensionality axiom. -See~\autoref{sec:univalence-implies-funext}.) +See~\autoref{sec:univalence-implies-funext}). Of course, if $A$ is equivalent to $B$ and $A$ is contractible, then so is $B$. More generally, it suffices for $B$ to be a \emph{retract} of $A$. @@ -1190,13 +1190,13 @@ \section{Contractibility} \begin{ex} Show that it is not the case that for all $A:\type$ we have $\brck{A} \to A$. (However, there can be particular types for which $\brck{A}\to A$. - \autoref{ex:brck-qinv} implies that $\qinv(f)$ is such.) + \autoref{ex:brck-qinv} implies that $\qinv(f)$ is such). \end{ex} \begin{ex} \index{axiom!of choice}% Show that if \LEM{} holds, then for all $A:\type$ we have $\bbrck{(\brck A \to A)}$. - (This property is a very simple form of the axiom of choice, which can fail in the absence of \LEM{}; see~\cite{krausgeneralizations}.) + (This property is a very simple form of the axiom of choice, which can fail in the absence of \LEM{}; see~\cite{krausgeneralizations}). \end{ex} \begin{ex} diff --git a/main.tex b/main.tex index de412022d..90674e8a7 100644 --- a/main.tex +++ b/main.tex @@ -33,11 +33,11 @@ \renewcommand{\backref}[1]{} \renewcommand{\backrefalt}[4]{% \ifcase #1 % - (No citations.) + (No citations). \or - (Cited on page\ #2.) + (Cited on page\ #2). \else - (Cited on pages\ #2.) + (Cited on pages\ #2). \fi} % OTHER PACKAGES diff --git a/preliminaries.tex b/preliminaries.tex index f4c3be49e..08e6095b6 100644 --- a/preliminaries.tex +++ b/preliminaries.tex @@ -221,7 +221,7 @@ \section{Function types} Now we can compute $f(a)$ by replacing the variable $x$ in $\Phi$ with $a$. As an example, consider the function $f : \nat \to \nat$ which is -defined by $f(x) \defeq x+x$. (We will define $\nat$ and $+$ in \autoref{sec:inductive-types}.) +defined by $f(x) \defeq x+x$. (We will define $\nat$ and $+$ in \autoref{sec:inductive-types}). Then $f(2)$ is judgmentally equal to $2+2$. If we don't want to introduce a name for the function, we can use @@ -313,7 +313,7 @@ \section{Function types} }} to $\lamu{z:\nat} x + z$. It follows that $f(y)$ is judgmentally equal to $\lamu{z:\nat} y + z$, and that answers our question. (Instead of $z$, -any variable distinct from $y$ could have been used, yielding an equal result.) +any variable distinct from $y$ could have been used, yielding an equal result). Of course, this should all be familiar to any mathematician: it is the same phenomenon as the fact that if $f(x) \defeq \int_1^2 \frac{dt}{x-t}$, then $f(t)$ is not $\int_1^2 \frac{dt}{t-t}$ but rather $\int_1^2 \frac{ds}{t-s}$. A $\lambda$-abstraction binds a dummy variable in exactly the same way that an integral does. @@ -419,7 +419,7 @@ \section{Universes and families} \symlabel{fin}% An example of a type family is the family of finite sets $\Fin : \nat \to \UU$, where $\Fin(n)$ is a type with exactly $n$ elements. -(We cannot \emph{define} the family $\Fin$ yet --- indeed, we have not even introduced its domain $\nat$ yet --- but we will be able to soon; see \autoref{ex:fin}.) +(We cannot \emph{define} the family $\Fin$ yet --- indeed, we have not even introduced its domain $\nat$ yet --- but we will be able to soon; see \autoref{ex:fin}). We may denote the elements of $\Fin(n)$ by $0_n,1_n,\dots,(n-1)_n$, with subscripts to emphasize that the elements of $\Fin(n)$ are different from those of $\Fin(m)$ if $n$ is different from $m$, and all are different from the ordinary natural numbers (which we will introduce in \autoref{sec:inductive-types}). \index{finite!sets, family of}% @@ -517,7 +517,7 @@ \section{Dependent function types (\texorpdfstring{$\Pi$}{Π}-types)} given $A:\UU$ and type families $B : A \to \UU$ and $C : \prd{x:A}B(x) \to \UU$, we may construct the type $\prd{x:A}{y : B(x)} C(x,y)$ of functions with two arguments. -(Like $\lambda$-abstractions, $\Pi$s automatically scope\index{scope} over the rest of the expression unless delimited; thus $C : \prd{x:A}B(x) \to \UU$ means $C : \prd{x:A}(B(x) \to \UU)$.) +(Like $\lambda$-abstractions, $\Pi$s automatically scope\index{scope} over the rest of the expression unless delimited; thus $C : \prd{x:A}B(x) \to \UU$ means $C : \prd{x:A}(B(x) \to \UU)$). In the case when $B$ is constant and equal to $A$, we may condense the notation and write $\prd{x,y:A}$; for instance, the type of $\mathsf{swap}$ could also be written as \[ \mathsf{swap} : \prd{A,B,C:\UU} (A\to B\to C) \to (B\to A \to C). \] @@ -551,7 +551,7 @@ \section{Product types} \item how to form new types of this kind, via \define{formation rules}. \indexdef{formation rule}% \index{rule!formation}% -(For example, we can form the function type $A \to B$ when $A$ is a type and when $B$ is a type. We can form the dependent function type $\prd{x:A} B(x)$ when $A$ is a type and $B(x)$ is a type for $x:A$.) +(For example, we can form the function type $A \to B$ when $A$ is a type and when $B$ is a type. We can form the dependent function type $\prd{x:A} B(x)$ when $A$ is a type and $B(x)$ is a type for $x:A$). \item how to construct elements of that type. These are called the type's \define{constructors} or \define{introduction rules}. @@ -560,32 +560,32 @@ \section{Product types} \indexdef{introduction rule}% (For example, a function type has one constructor, $\lambda$-abstraction. Recall that a direct definition like $f(x)\defeq 2x$ can equivalently be phrased - as a $\lambda$-abstraction $f\defeq \lam{x} 2x$.) + as a $\lambda$-abstraction $f\defeq \lam{x} 2x$). \item how to use elements of that type. These are called the type's \define{eliminators} or \define{elimination rules}. \indexsee{rule!elimination}{eliminator}% \indexsee{elimination rule}{eliminator}% \indexdef{eliminator}% - (For example, the function type has one eliminator, namely function application.) + (For example, the function type has one eliminator, namely function application). \item a \define{computation rule}\indexdef{computation rule}\footnote{also referred to as \define{$\beta$-reduction}\index{beta-reduction@$\beta $-reduction|footstyle}}, which expresses how an eliminator acts on a constructor. -(For example, for functions, the computation rule states that $(\lamu{x:A}\Phi)(a)$ is judgmentally equal to the substitution of $a$ for $x$ in $\Phi$.) +(For example, for functions, the computation rule states that $(\lamu{x:A}\Phi)(a)$ is judgmentally equal to the substitution of $a$ for $x$ in $\Phi$). \item an optional \define{uniqueness principle}\indexdef{uniqueness!principle}\footnote{also referred to as \define{$\eta$-expansion}\index{eta-expansion@$\eta $-expansion|footstyle}}, which expresses uniqueness of maps into or out of that type. For some types, the uniqueness principle characterizes maps into the type, by stating that every element of the type is uniquely determined by the results of applying eliminators to it, and can be reconstructed from those results by applying a constructor---thus expressing how constructors act on eliminators, dually to the computation rule. -(For example, for functions, the uniqueness principle says that any function $f$ is judgmentally equal to the ``expanded'' function $\lamu{x} f(x)$, and thus is uniquely determined by its values.) -For other types, the uniqueness principle says that every map (function) \emph{from} that type is uniquely determined by some data. (An example is the coproduct type introduced in \cref{sec:coproduct-types}, whose uniqueness principle is mentioned in \cref{sec:universal-properties}.) +(For example, for functions, the uniqueness principle says that any function $f$ is judgmentally equal to the ``expanded'' function $\lamu{x} f(x)$, and thus is uniquely determined by its values). +For other types, the uniqueness principle says that every map (function) \emph{from} that type is uniquely determined by some data. (An example is the coproduct type introduced in \cref{sec:coproduct-types}, whose uniqueness principle is mentioned in \cref{sec:universal-properties}). When the uniqueness principle is not taken as a rule of judgmental equality, it is often nevertheless provable as a \emph{propositional} equality from the other rules for the type. In this case we call it a \define{propositional uniqueness principle}. \indexdef{uniqueness!principle, propositional}% \indexsee{propositional!uniqueness principle}{uniqueness principle, propositional}% - (In later chapters we will also occasionally encounter \emph{propositional computation rules}.) + (In later chapters we will also occasionally encounter \emph{propositional computation rules}). \indexdef{computation rule!propositional}% \end{enumerate} The inference rules in \autoref{sec:syntax-more-formally} are organized and named accordingly; see, for example, \autoref{sec:more-formal-pi}, where each possibility is realized. @@ -603,7 +603,7 @@ \section{Product types} Thus, we introduce a new rule (the elimination rule for products), which says that for any such $g$, we can define a function $f : A\times B \to C$ by \[ f(\tup{a}{b}) \defeq g(a)(b). \] We avoid writing $g(a,b)$ here, in order to emphasize that $g$ is not a function on a product. -(However, later on in the book we will often write $g(a,b)$ both for functions on a product and for curried functions of two variables.) +(However, later on in the book we will often write $g(a,b)$ both for functions on a product and for curried functions of two variables). This defining equation is the computation rule for product types\index{computation rule!for product types}. Note that in set theory, we would justify the above definition of $f$ by the fact that every element of $A\times B$ is a pair, so that it suffices to define $f$ on pairs. @@ -885,7 +885,7 @@ \section{Coproduct types} There are two ways to construct elements of $A+B$, either as $\inl(a) : A+B$ for $a:A$, or as $\inr(b):A+B$ for $b:B$. -(The names $\inl$ and $\inr$ are short for ``left injection'' and ``right injection''.) +(The names $\inl$ and $\inr$ are short for ``left injection'' and ``right injection''). There are no ways to construct elements of the empty type. \index{recursion principle!for coproduct} @@ -1021,7 +1021,7 @@ \section{The type of booleans} For this we need a type family $P:\bool\to\type$ such that $P(\bfalse)\jdeq A$ and $P(\btrue)\jdeq B$. Indeed, we can obtain such a family precisely by the recursion principle for $\bool$. \index{type!family of}% -(The ability to define \emph{type families} by induction and recursion, using the fact that the universe $\UU$ is itself a type, is a subtle and important aspect of type theory.) +(The ability to define \emph{type families} by induction and recursion, using the fact that the universe $\UU$ is itself a type, is a subtle and important aspect of type theory). Thus, we could have defined \index{type!coproduct}% \[ A + B \defeq \sm{x:\bool} \rec{\bool}(\UU,A,B,x). \] @@ -1031,7 +1031,7 @@ \section{The type of booleans} \inr(b) &\defeq \tup{\btrue}{b}. \end{align*} We leave it as an exercise to derive the induction principle of a coproduct type from this definition. -(See also \autoref{ex:sum-via-bool,sec:appetizer-univalence}.) +(See also \autoref{ex:sum-via-bool,sec:appetizer-univalence}). We can apply the same idea to products and $\Pi$-types: we could have defined \[ A \times B \defeq \prd{x:\bool}\rec{\bool}(\UU,A,B,x) \] @@ -1050,7 +1050,7 @@ \section{The type of booleans} However, note that unlike in classical\index{mathematics!classical} mathematics, we do not use elements of $\bool$ as truth values \index{value!truth}% or as propositions. -(Instead we identify propositions with types; see \autoref{sec:pat}.) +(Instead we identify propositions with types; see \autoref{sec:pat}). In particular, the type $A \to \bool$ is not generally the power set\index{power set} of $A$; it represents only the ``decidable'' subsets of $A$ (see \autoref{cha:logic}). \index{decidable!subset}% @@ -1136,7 +1136,7 @@ \section{The natural numbers} \add &\defeq \rec{\nat}\big(\nat \to \nat,\, \lamu{n:\nat} n,\, \lamu{n:\nat}{g:\nat \to \nat}{m :\nat} \suc(g(m))\big). \end{align} Of course, all functions definable only using the primitive recursion principle will be \emph{computable}. -(The presence of higher function types --- that is, functions with other functions as arguments --- does, however, mean we can define more than the usual primitive recursive functions; see e.g.~\autoref{ex:ackermann}.) +(The presence of higher function types --- that is, functions with other functions as arguments --- does, however, mean we can define more than the usual primitive recursive functions; see e.g.~\autoref{ex:ackermann}). This is appropriate in constructive mathematics; \index{mathematics!constructive}% in \autoref{sec:intuitionism,sec:axiom-choice} we will see how to augment type theory so that we can define more general mathematical functions. @@ -1164,7 +1164,7 @@ \section{The natural numbers} \index{associativity!of addition!of natural numbers} As an example, consider how we might represent an explicit proof that $+$ is associative. -(We will not actually write out proofs in this style, but it serves as a useful example for understanding how induction is represented formally in type theory.) +(We will not actually write out proofs in this style, but it serves as a useful example for understanding how induction is represented formally in type theory). To derive \[\assoc : \prd{i,j,k:\nat} \id{i + (j + k)}{(i + j) + k}, \] it is sufficient to supply @@ -1188,7 +1188,7 @@ \section{The natural numbers} \index{hypothesis!inductive}% \index{inductive!hypothesis}% yields $\id{i+(j+k)}{(i+j)+k}$, so it suffices to invoke the fact that if two natural numbers are equal, then so are their successors. -(We will prove this obvious fact in \autoref{lem:map}, using the induction principle of identity types.) +(We will prove this obvious fact in \autoref{lem:map}, using the induction principle of identity types). We call this latter fact $\apfunc{\suc} : %\prd{m,n:\nat} (\id[\nat]{m}{n}) \to (\id[\nat]{\suc(m)}{\suc(n)})$, so we can define @@ -1269,7 +1269,7 @@ \section{Propositions as types} \index{evidence, of the truth of a proposition}% \index{witness!to the truth of a proposition}% \index{proof|(} -We regard the elements of this type as \emph{evidence} or \emph{witnesses} that the proposition is true. (They are sometimes even called \emph{proofs}, but this terminology can be misleading, so we generally avoid it.) +We regard the elements of this type as \emph{evidence} or \emph{witnesses} that the proposition is true. (They are sometimes even called \emph{proofs}, but this terminology can be misleading, so we generally avoid it). In general, however, we will not construct witnesses explicitly; instead we present the proofs in ordinary mathematical prose, in such a way that they could be translated into an element of a type. This is no different from reasoning in classical set theory, where we don't expect to see an explicit derivation using the rules of predicate logic and the axioms of set theory. @@ -1368,7 +1368,7 @@ \section{Propositions as types} At this point our partial definition of an element of~\eqref{eq:tautology2} can be written as \[ f((x,y)) \defeq\; \Box\;:A+B\to\emptyt \] with a ``hole'' $\Box$ of type $A+B\to\emptyt$ indicating what remains to be done. -(We could equivalently write $f \defeq \rec{(A\to\emptyt)\times (B\to\emptyt)}(A+B\to\emptyt,\lam{x}{y} \Box)$, using the recursor instead of pattern matching.) +(We could equivalently write $f \defeq \rec{(A\to\emptyt)\times (B\to\emptyt)}(A+B\to\emptyt,\lam{x}{y} \Box)$, using the recursor instead of pattern matching). The next phrase ``also suppose $A$ or $B$; we will derive a contradiction'' indicates filling this hole by a function definition, introducing another unnamed hypothesis $z:A+B$, leading to the proof state: \[ f((x,y))(z) \defeq \;\Box\; :\emptyt \] Now saying ``there are two cases'' indicates a case split, i.e.\ an application of the recursion principle for the coproduct $A+B$. @@ -1382,7 +1382,7 @@ \section{Propositions as types} Note that in both cases we now have two ``holes'' of type $\emptyt$ to fill in, corresponding to the two cases where we have to derive a contradiction. Finally, the conclusion of a contradiction from $a:A$ and $x:A\to\emptyt$ is simply application of the function $x$ to $a$, and similarly in the other case. \index{application!of hypothesis or theorem}% -(Note the convenient coincidence of the phrase ``applying a function'' with that of ``applying a hypothesis'' or theorem.) +(Note the convenient coincidence of the phrase ``applying a function'' with that of ``applying a hypothesis'' or theorem). Thus our eventual definition is \begin{align*} f((x,y))(\inl(a)) &\defeq x(a)\\ @@ -1474,7 +1474,7 @@ \section{Propositions as types} \symlabel{leq-nat}% As a more concrete example, consider how to define inequalities of natural numbers. One natural definition is that $n\le m$ if there exists a $k:\nat$ such that $n+k=m$. -(This uses again the identity types that we will introduce in the next section, but we will not need very much about them.) +(This uses again the identity types that we will introduce in the next section, but we will not need very much about them). Under the propositions-as-types translation, this would yield: \[ (n\le m) \defeq \sm{k:\nat} (\id{n+k}{m}). \] The reader is invited to prove the familiar properties of $\le$ from this definition. @@ -1522,7 +1522,7 @@ \section{Propositions as types} Using these types, we will introduce a modification to the above-described logic that is sometimes appropriate, in which the additional information contained in disjunctions and existentials is discarded. Finally, we note that the propositions-as-types correspondence can be viewed in reverse, allowing us to regard any type $A$ as a proposition, which we prove by exhibiting an element of $A$. -Sometimes we will state this proposition as ``$A$ is \define{inhabited}.'' +Sometimes we will state this proposition as ``$A$ is \define{inhabited}''. \indexdef{inhabited type}% \indexsee{type!inhabited}{inhabited type}% That is, when we say that $A$ is inhabited, we mean that we have given a (particular) element of $A$, but that we are choosing not to give a name to that element. @@ -1572,7 +1572,7 @@ \section{Identity types} This is well-typed because $a\jdeq b$ means that also the type $\id[A]{a}{b}$ is judgmentally equal to $\id[A]{a}{a}$, which is the type of $\refl{a}$. The induction principle (i.e.\ the elimination rule) for the identity types is one of the most subtle parts of type theory, and crucial to the homotopy interpretation. -We begin by considering an important consequence of it, the principle that ``equals may be substituted for equals,'' as expressed by the following: +We begin by considering an important consequence of it, the principle that ``equals may be substituted for equals'', as expressed by the following: \index{indiscernability of identicals}% \index{equals may be substituted for equals}% \begin{description} @@ -1683,7 +1683,7 @@ \subsection{Path induction} \[ \indidb{A}(a,C,c,a,\refl{a}) \defeq c. \] %\[ g(x)(x,\refl{x}) \defeq d(x) \] -Below, we show that path induction and based path induction are equivalent. Because of this, we will sometimes be sloppy and also refer to based path induction simply as ``path induction,'' relying on the reader to infer which principle is meant from the form of the proof. +Below, we show that path induction and based path induction are equivalent. Because of this, we will sometimes be sloppy and also refer to based path induction simply as ``path induction'', relying on the reader to infer which principle is meant from the form of the proof. \begin{rmk} Intuitively, the induction principle for the natural numbers expresses the fact that the only natural numbers are $0$ and $\suc(n)$, so if we prove a property for these cases, then we have proved it for all natural numbers. Applying this same reading to path induction, we might loosely say that path induction expresses the fact that the only path is \refl{}, so if we prove a property for reflexivity, then we have proved it for all paths. However, this reading is quite confusing in the context of the homotopy interpretation of paths, where there may be many different ways in which two elements $a$ and $b$ can be identified, and therefore many different elements of the identity type! How can there be many different paths, but at the same time we have an induction principle asserting that the only path is reflexivity? @@ -1849,7 +1849,7 @@ \subsection{Disequality} the only proof of equality is reflexivity (up to judgmental equality). These additional requirements may be selectively imposed in the \Coq and \Agda\ systems. -%(In the terminology of \autoref{cha:hlevels} such a type theory is about $0$-truncated types.) +%(In the terminology of \autoref{cha:hlevels} such a type theory is about $0$-truncated types). Another point of variation among intensional theories is the strength of judgmental equality, particularly as regards objects of function type. Here we include the uniqueness principle\index{uniqueness!principle} ($\eta$-conversion) $f \jdeq \lam{x} f(x)$, as a principle of judgmental equality. This principle is used, for example, in \autoref{sec:univalence-implies-funext}, to show that univalence implies propositional function extensionality. Uniqueness principles are sometimes considered for other types. For instance, the uniqueness principle\index{uniqueness!principle!for product types} for cartesian products would be a judgmental version of the propositional equality $\uppt$ which we constructed in \autoref{sec:finite-product-types}, saying that $u \jdeq (\proj1(u),\proj2(u))$. @@ -1874,7 +1874,7 @@ \subsection{Disequality} Unlike the type theory of \Coq, we do not include a primitive type of propositions. Instead, as discussed in \autoref{sec:pat}, we embrace the \emph{propositions-as-types (PAT)} principle, identifying propositions with types. This was suggested originally by de Bruijn~\cite{deBruijn-1973}, Howard~\cite{howard:pat}, Tait~\cite{Tait-1968}, and Martin-L\"{o}f~\cite{Martin-Lof-1972}. -(Our decision is explained more fully in \autoref{subsec:pat?,subsec:hprops}.) +(Our decision is explained more fully in \autoref{subsec:pat?,subsec:hprops}). We do, however, include a full cumulative hierarchy of universes, so that the type formation and equality judgments become instances of the membership and equality judgments for a universe. As a convenience, we regard objects of a universe as types, rather than as codes for types; in the terminology of \cite{martin-lof:bibliopolis}, this means we use ``Russell-style universes'' rather than ``Tarski-style universes''. @@ -1917,7 +1917,7 @@ \subsection{Disequality} Derive the induction principle for products $\ind{A\times B}$, using only the projections and the propositional uniqueness principle $\uppt$. Verify that the definitional equalities are valid. Generalize $\uppt$ to $\Sigma$-types, and do the same for $\Sigma$-types. - \emph{(This requires concepts from \autoref{cha:basics}.)} + \emph{(This requires concepts from \autoref{cha:basics}).} \end{ex} \begin{ex}\label{ex:iterator} @@ -1941,12 +1941,12 @@ \subsection{Disequality} \begin{ex}\label{ex:prod-via-bool} \index{type!product}% Show that if we define $A \times B \defeq \prd{x:\bool}\rec{\bool}(\UU,A,B,x)$, then we can give a definition of $\ind{A\times B}$ for which the definitional equalities stated in \autoref{sec:finite-product-types} hold propositionally (i.e.\ using equality types). -\emph{(This requires the function extensionality axiom, which is introduced in \autoref{sec:compute-pi}.)} +\emph{(This requires the function extensionality axiom, which is introduced in \autoref{sec:compute-pi}).} \end{ex} \begin{ex}\label{ex:pm-to-ml} Give an alternative derivation of $\indidb{A}$ from $\indid{A}$ which avoids the use of universes. - \emph{(This is easiest using concepts from later chapters.)} + \emph{(This is easiest using concepts from later chapters).} \end{ex} \begin{ex}\label{ex:nat-semiring} diff --git a/reals.tex b/reals.tex index 3b4c7bf75..367b1904e 100644 --- a/reals.tex +++ b/reals.tex @@ -158,7 +158,7 @@ \section{Dedekind reals} \index{sigma-frame@$\sigma$-frame!initial|defstyle}% i.e., a lattice\index{lattice} with countable joins\index{join!in a lattice} in which binary meets distribute over countable joins. (The initial $\sigma$-frame cannot be the two-point lattice $\bool$ because - $\bool$ is not closed under countable joins, unless we assume excluded middle.) This + $\bool$ is not closed under countable joins, unless we assume excluded middle). This would lead to a construction of~$\Omega$ as a higher inductive-inductive type, but one experiment of this kind in \autoref{sec:cauchy-reals} is enough. \end{enumerate} @@ -596,7 +596,7 @@ \subsection{Dedekind reals are Dedekind complete} U_x(q) \defeq (x < q). \end{equation*} % - (We have just used the assumption that $F$ is admissible for $\Omega$.) + (We have just used the assumption that $F$ is admissible for $\Omega$). Then $(L_x, U_x)$ is a Dedekind cut.\index{cut!Dedekind} Indeed, the cuts are inhabited and rounded because $F$ is archimedean and $<$ is transitive, disjoint because $<$ is irreflexive, and located because $<$ is a weak linear order. Let $e : F \to \RD$ be the map $e(x) \defeq (L_x, @@ -702,7 +702,7 @@ \section{Cauchy reals} In general, the construction of a free gadget of any sort requires applying the gadget operations repeatedly many times to the generators. For instance, the elements of the free group on a set $X$ are not just binary products and inverses of elements of $X$, but words obtained by iterating the product and inverse constructions. Thus, we might naturally expect the same to be true for Cauchy completion, with the relevant ``operation'' being ``take the limit of a Cauchy sequence''. -(In this case, the iteration would have to take place transfinitely, since even after infinitely many steps there will be new Cauchy sequences to take the limit of.) +(In this case, the iteration would have to take place transfinitely, since even after infinitely many steps there will be new Cauchy sequences to take the limit of). The argument referred to above shows that if excluded middle or countable choice hold, then Cauchy completion is very special: when building the completion of a space, it suffices to stop applying the operation after \emph{one step}. This may be regarded as analogous to the fact that free monoids and free groups can be given explicit descriptions in terms of (reduced) words. @@ -932,7 +932,7 @@ \subsection{Induction and recursion on Cauchy reals} \end{proof} We can also show that although $\RC$ may not be a quotient of the set of Cauchy sequences of \emph{rationals}, it is nevertheless a quotient of the set of Cauchy sequences of \emph{reals}. -(Of course, this is not a valid \emph{definition} of $\RC$, but it is a useful property.) +(Of course, this is not a valid \emph{definition} of $\RC$, but it is a useful property). We define the type of Cauchy approximations to be % \symlabel{cauchy-approximations}% @@ -1225,7 +1225,7 @@ \subsection{Induction and recursion on Cauchy reals} It is at this point that we can give the definitions~\eqref{eq:RCappx1}--\eqref{eq:RCappx4}, as the first two clauses of each of the two inner recursions, corresponding to rational points and limits. In each case, we must verify that the relation is rounded and hence lies in $C$. In the rational-rational case~\eqref{eq:RCappx1} this is clear, while in the other cases it follows from an inductive hypothesis. - (In~\eqref{eq:RCappx2} the relevant inductive hypothesis is that $(\rcrat(q) \approx_{(\blank)} y_\delta) : C$, while in~\eqref{eq:RCappx3} and~\eqref{eq:RCappx4} it is that $(x_\delta \approx_{(\blank)} \blank) : A$.) + (In~\eqref{eq:RCappx2} the relevant inductive hypothesis is that $(\rcrat(q) \approx_{(\blank)} y_\delta) : C$, while in~\eqref{eq:RCappx3} and~\eqref{eq:RCappx4} it is that $(x_\delta \approx_{(\blank)} \blank) : A$). The remaining data of the sub-recursions consist of showing that \eqref{eq:RCappx1}--\eqref{eq:RCappx4} satisfy the triangle inequality on the right with respect to the constructors of $\closesym$. There are eight cases --- four in each sub-recursion --- corresponding to the eight possible ways that $u$, $v$, and $w$ in~\eqref{eq:RC-sim-rtri} can be chosen to be rational points or limits. @@ -1785,7 +1785,7 @@ \section{Comparison of Cauchy and Dedekind reals} $\sigma$-frame \index{initial!sigma-frame@$\sigma$-frame}% \index{sigma-frame@$\sigma$-frame!initial}% -it takes a simple induction, while in other cases it is immediate.) +it takes a simple induction, while in other cases it is immediate). Therefore, by \autoref{RD-final-field} there is an embedding of ordered fields % \begin{equation*} @@ -1793,7 +1793,7 @@ \section{Comparison of Cauchy and Dedekind reals} \end{equation*} % which fixes the rational numbers. -(We could also obtain this from \autoref{RC-initial-Cauchy-complete,RD-cauchy-complete}.) +(We could also obtain this from \autoref{RC-initial-Cauchy-complete,RD-cauchy-complete}). In general we do not expect $\RC$ and $\RD$ to coincide without further assumptions. @@ -2471,7 +2471,7 @@ \section{The surreal numbers} This obviously looks like an inductive definition, but there are three issues with regarding it as such. Firstly, the definition requires the relation of (strict) inequality between surreals, so that relation must be defined simultaneously with the type \NO of surreals. -(Conway avoids this issue by first defining \emph{games}\index{game!Conway}, which are like surreals but omit the compatibility condition on $L$ and $R$.) +(Conway avoids this issue by first defining \emph{games}\index{game!Conway}, which are like surreals but omit the compatibility condition on $L$ and $R$). As with the relation $\closesym$ for the Cauchy reals, this simultaneous definition could \emph{a priori} be either inductive-inductive or inductive-recursive. We will choose to make it inductive-inductive, for the same reasons we made that choice for $\closesym$. @@ -2485,14 +2485,14 @@ \section{The surreal numbers} In type theory, this means that \NO will be defined relative to a universe \UU, but will itself belong to the next higher universe $\UU'$, like the sets \ord and \card of ordinals and cardinals, the cumulative hierarchy $V$, or even the Dedekind reals in the absence of propositional resizing. \index{propositional!resizing}% We will then require the ``sets'' $L$ and $R$ of surreals to be \UU-small, and so it is natural to represent them by \emph{families} of surreals indexed by some \UU-small type. -(This is all exactly the same as what we did with the cumulative hierarchy in \autoref{sec:cumulative-hierarchy}.) +(This is all exactly the same as what we did with the cumulative hierarchy in \autoref{sec:cumulative-hierarchy}). That is, the constructor of surreals will have type \[ \prd{\LL,\RR:\UU} (\LL\to\NO) \to (\RR\to \NO) \to (\text{some condition}) \to \NO \] which is indeed strictly positive.\index{strict!positivity} Finally, after giving the mutual definitions of \NO and its ordering, Conway declares two surreal numbers $x$ and $y$ to be \emph{equal} if $x\le y$ and $y\le x$. This is naturally read as passing to a quotient of the set of ``pre-surreals'' by an equivalence relation. -%(In set-theoretic foundations, one has to us an additional trick to deal with large equivalence classes.) +%(In set-theoretic foundations, one has to us an additional trick to deal with large equivalence classes). However, in the absence of the axiom of choice, such a quotient presents the same problem as the quotient in the usual construction of Cauchy reals: it will no longer be the case that a pair of families \emph{of surreals} yield a new surreal $\surr L R$, since we cannot necessarily ``lift'' $L$ and $R$ to families of pre-surreals. Of course, we can solve this problem in the same way we did for Cauchy reals, by using a \emph{higher} inductive-inductive definition. @@ -2703,7 +2703,7 @@ \section{The surreal numbers} \begin{cor}\label{thm:NO-set} \NO is a 0-type. -% (As with $V$, it might be confusing to say that it is a ``set''.) +% (As with $V$, it might be confusing to say that it is a ``set''). \end{cor} \begin{proof} The mere relation $R(x,y)\defeq (x\le y) \land (y\le x)$ implies identity by the path constructor of $\NO$, and contains the diagonal by \autoref{thm:NO-refl-opt}\ref{item:NO-le-refl}. @@ -2725,7 +2725,7 @@ \section{The surreal numbers} Suppose $A$ is a type equipped with relations $\mathord\ble:A\to A\to\prop$ and $\mathord\blt:A\to A\to\prop$. Then we can define $f:\NO\to A$ by doing the following. \begin{enumerate} -\item For any $x$ defined by a cut, assuming $f(x^L)$ and $f(x^R)$ to be defined such that $f(x^L)\blt f(x^R)$ for all $L$ and $R$, we must define $f(x)$. (We call this the \emph{primary clause} of the recursion.)\label{item:NO-rec-primary} +\item For any $x$ defined by a cut, assuming $f(x^L)$ and $f(x^R)$ to be defined such that $f(x^L)\blt f(x^R)$ for all $L$ and $R$, we must define $f(x)$. (We call this the \emph{primary clause} of the recursion).\label{item:NO-rec-primary} \item Prove that $\ble$ is \emph{antisymmetric}\index{relation!antisymmetric}: if $a\ble b$ and $b\ble a$, then $a=b$. \item For $x,y$ defined by cuts such that $x^L