# HoTT/book

Switch branches/tags
Nothing to show
Fetching contributors…
Cannot retrieve contributors at this time
817 lines (683 sloc) 31.3 KB
 %%%% MACROS FOR NOTATION %%%% % Use these for any notation where there are multiple options. %%% Notes and exercise sections \makeatletter \newcommand{\sectionNotes}{\phantomsection\section*{Notes}\addcontentsline{toc}{section}{Notes}\markright{\textsc{\@chapapp{} \thechapter{} Notes}}} \newcommand{\sectionExercises}[1]{\phantomsection\section*{Exercises}\addcontentsline{toc}{section}{Exercises}\markright{\textsc{\@chapapp{} \thechapter{} Exercises}}} \makeatother %%% Definitional equality (used infix) %%% \newcommand{\jdeq}{\equiv} % An equality judgment \let\judgeq\jdeq %\newcommand{\defeq}{\coloneqq} % An equality currently being defined \newcommand{\defeq}{\vcentcolon\equiv} % A judgmental equality currently being defined %%% Term being defined \newcommand{\define}[1]{\textbf{#1}} %%% Vec (for example) \newcommand{\Vect}{\ensuremath{\mathsf{Vec}}} \newcommand{\Fin}{\ensuremath{\mathsf{Fin}}} \newcommand{\fmax}{\ensuremath{\mathsf{fmax}}} \newcommand{\seq}[1]{\langle #1\rangle} %%% Dependent products %%% \def\prdsym{\textstyle\prod} %% Call the macro like \prd{x,y:A}{p:x=y} with any number of %% arguments. Make sure that whatever comes *after* the call doesn't %% begin with an open-brace, or it will be parsed as another argument. \makeatletter % Currently the macro is configured to produce % {\textstyle\prod}(x:A) \; {\textstyle\prod}(y:B),{\ } % in display-math mode, and % \prod_{(x:A)} \prod_{y:B} % in text-math mode. % \def\prd#1{\@ifnextchar\bgroup{\prd@parens{#1}}{% % \@ifnextchar\sm{\prd@parens{#1}\@eatsm}{% % \prd@noparens{#1}}}} \def\prd#1{\@ifnextchar\bgroup{\prd@parens{#1}}{% \@ifnextchar\sm{\prd@parens{#1}\@eatsm}{% \@ifnextchar\prd{\prd@parens{#1}\@eatprd}{% \@ifnextchar\;{\prd@parens{#1}\@eatsemicolonspace}{% \@ifnextchar\\{\prd@parens{#1}\@eatlinebreak}{% \@ifnextchar\narrowbreak{\prd@parens{#1}\@eatnarrowbreak}{% \prd@noparens{#1}}}}}}}} \def\prd@parens#1{\@ifnextchar\bgroup% {\mathchoice{\@dprd{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}\prd@parens}% {\@ifnextchar\sm% {\mathchoice{\@dprd{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}\@eatsm}% {\mathchoice{\@dprd{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}}}} \def\@eatsm\sm{\sm@parens} \def\prd@noparens#1{\mathchoice{\@dprd@noparens{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}} % Helper macros for three styles \def\lprd#1{\@ifnextchar\bgroup{\@lprd{#1}\lprd}{\@@lprd{#1}}} \def\@lprd#1{\mathchoice{{\textstyle\prod}}{\prod}{\prod}{\prod}({\textstyle #1})\;} \def\@@lprd#1{\mathchoice{{\textstyle\prod}}{\prod}{\prod}{\prod}({\textstyle #1}),\ } \def\tprd#1{\@tprd{#1}\@ifnextchar\bgroup{\tprd}{}} \def\@tprd#1{\mathchoice{{\textstyle\prod_{(#1)}}}{\prod_{(#1)}}{\prod_{(#1)}}{\prod_{(#1)}}} \def\dprd#1{\@dprd{#1}\@ifnextchar\bgroup{\dprd}{}} \def\@dprd#1{\prod_{(#1)}\,} \def\@dprd@noparens#1{\prod_{#1}\,} % Look through spaces and linebreaks \def\@eatnarrowbreak\narrowbreak{% \@ifnextchar\prd{\narrowbreak\@eatprd}{% \@ifnextchar\sm{\narrowbreak\@eatsm}{% \narrowbreak}}} \def\@eatlinebreak\\{% \@ifnextchar\prd{\\\@eatprd}{% \@ifnextchar\sm{\\\@eatsm}{% \\}}} \def\@eatsemicolonspace\;{% \@ifnextchar\prd{\;\@eatprd}{% \@ifnextchar\sm{\;\@eatsm}{% \;}}} %%% Lambda abstractions. % Each variable being abstracted over is a separate argument. If % there is more than one such argument, they *must* be enclosed in % braces. Arguments can be untyped, as in \lam{x}{y}, or typed with a % colon, as in \lam{x:A}{y:B}. In the latter case, the colons are % automatically noticed and (with current implementation) the space % around the colon is reduced. You can even give more than one variable % the same type, as in \lam{x,y:A}. \def\lam#1{{\lambda}\@lamarg#1:\@endlamarg\@ifnextchar\bgroup{.\,\lam}{.\,}} \def\@lamarg#1:#2\@endlamarg{\if\relax\detokenize{#2}\relax #1\else\@lamvar{\@lameatcolon#2},#1\@endlamvar\fi} \def\@lamvar#1,#2\@endlamvar{(#2\,{:}\,#1)} % \def\@lamvar#1,#2{{#2}^{#1}\@ifnextchar,{.\,{\lambda}\@lamvar{#1}}{\let\@endlamvar\relax}} \def\@lameatcolon#1:{#1} \let\lamt\lam % This version silently eats any typing annotation. \def\lamu#1{{\lambda}\@lamuarg#1:\@endlamuarg\@ifnextchar\bgroup{.\,\lamu}{.\,}} \def\@lamuarg#1:#2\@endlamuarg{#1} %%% Dependent products written with \forall, in the same style \def\fall#1{\forall (#1)\@ifnextchar\bgroup{.\,\fall}{.\,}} %%% Existential quantifier %%% \def\exis#1{\exists (#1)\@ifnextchar\bgroup{.\,\exis}{.\,}} %%% Dependent sums %%% \def\smsym{\textstyle\sum} % Use in the same way as \prd \def\sm#1{\@ifnextchar\bgroup{\sm@parens{#1}}{% \@ifnextchar\prd{\sm@parens{#1}\@eatprd}{% \@ifnextchar\sm{\sm@parens{#1}\@eatsm}{% \@ifnextchar\;{\sm@parens{#1}\@eatsemicolonspace}{% \@ifnextchar\\{\sm@parens{#1}\@eatlinebreak}{% \@ifnextchar\narrowbreak{\sm@parens{#1}\@eatnarrowbreak}{% \sm@noparens{#1}}}}}}}} \def\sm@parens#1{\@ifnextchar\bgroup% {\mathchoice{\@dsm{#1}}{\@tsm{#1}}{\@tsm{#1}}{\@tsm{#1}}\sm@parens}% {\@ifnextchar\prd% {\mathchoice{\@dsm{#1}}{\@tsm{#1}}{\@tsm{#1}}{\@tsm{#1}}\@eatprd}% {\mathchoice{\@dsm{#1}}{\@tsm{#1}}{\@tsm{#1}}{\@tsm{#1}}}}} \def\@eatprd\prd{\prd@parens} \def\sm@noparens#1{\mathchoice{\@dsm@noparens{#1}}{\@tsm{#1}}{\@tsm{#1}}{\@tsm{#1}}} \def\lsm#1{\@ifnextchar\bgroup{\@lsm{#1}\lsm}{\@@lsm{#1}}} \def\@lsm#1{\mathchoice{{\textstyle\sum}}{\sum}{\sum}{\sum}({\textstyle #1})\;} \def\@@lsm#1{\mathchoice{{\textstyle\sum}}{\sum}{\sum}{\sum}({\textstyle #1}),\ } \def\tsm#1{\@tsm{#1}\@ifnextchar\bgroup{\tsm}{}} \def\@tsm#1{\mathchoice{{\textstyle\sum_{(#1)}}}{\sum_{(#1)}}{\sum_{(#1)}}{\sum_{(#1)}}} \def\dsm#1{\@dsm{#1}\@ifnextchar\bgroup{\dsm}{}} \def\@dsm#1{\sum_{(#1)}\,} \def\@dsm@noparens#1{\sum_{#1}\,} %%% W-types \def\wtypesym{{\mathsf{W}}} \def\wtype#1{\@ifnextchar\bgroup% {\mathchoice{\@twtype{#1}}{\@twtype{#1}}{\@twtype{#1}}{\@twtype{#1}}\wtype}% {\mathchoice{\@twtype{#1}}{\@twtype{#1}}{\@twtype{#1}}{\@twtype{#1}}}} \def\lwtype#1{\@ifnextchar\bgroup{\@lwtype{#1}\lwtype}{\@@lwtype{#1}}} \def\@lwtype#1{\mathchoice{{\textstyle\mathsf{W}}}{\mathsf{W}}{\mathsf{W}}{\mathsf{W}}({\textstyle #1})\;} \def\@@lwtype#1{\mathchoice{{\textstyle\mathsf{W}}}{\mathsf{W}}{\mathsf{W}}{\mathsf{W}}({\textstyle #1}),\ } \def\twtype#1{\@twtype{#1}\@ifnextchar\bgroup{\twtype}{}} \def\@twtype#1{\mathchoice{{\textstyle\mathsf{W}_{(#1)}}}{\mathsf{W}_{(#1)}}{\mathsf{W}_{(#1)}}{\mathsf{W}_{(#1)}}} \def\dwtype#1{\@dwtype{#1}\@ifnextchar\bgroup{\dwtype}{}} \def\@dwtype#1{\mathsf{W}_{(#1)}\,} \newcommand{\suppsym}{{\mathsf{sup}}} \newcommand{\supp}{\ensuremath\suppsym\xspace} \def\wtypeh#1{\@ifnextchar\bgroup% {\mathchoice{\@lwtypeh{#1}}{\@twtypeh{#1}}{\@twtypeh{#1}}{\@twtypeh{#1}}\wtypeh}% {\mathchoice{\@@lwtypeh{#1}}{\@twtypeh{#1}}{\@twtypeh{#1}}{\@twtypeh{#1}}}} \def\lwtypeh#1{\@ifnextchar\bgroup{\@lwtypeh{#1}\lwtypeh}{\@@lwtypeh{#1}}} \def\@lwtypeh#1{\mathchoice{{\textstyle\mathsf{W}^h}}{\mathsf{W}^h}{\mathsf{W}^h}{\mathsf{W}^h}({\textstyle #1})\;} \def\@@lwtypeh#1{\mathchoice{{\textstyle\mathsf{W}^h}}{\mathsf{W}^h}{\mathsf{W}^h}{\mathsf{W}^h}({\textstyle #1}),\ } \def\twtypeh#1{\@twtypeh{#1}\@ifnextchar\bgroup{\twtypeh}{}} \def\@twtypeh#1{\mathchoice{{\textstyle\mathsf{W}^h_{(#1)}}}{\mathsf{W}^h_{(#1)}}{\mathsf{W}^h_{(#1)}}{\mathsf{W}^h_{(#1)}}} \def\dwtypeh#1{\@dwtypeh{#1}\@ifnextchar\bgroup{\dwtypeh}{}} \def\@dwtypeh#1{\mathsf{W}^h_{(#1)}\,} \makeatother % Other notations related to dependent sums \let\setof\Set % from package 'braket', write \setof{ x:A | P(x) }. \newcommand{\pair}{\ensuremath{\mathsf{pair}}\xspace} \newcommand{\tup}[2]{(#1,#2)} \newcommand{\proj}[1]{\ensuremath{\mathsf{pr}_{#1}}\xspace} \newcommand{\fst}{\ensuremath{\proj1}\xspace} \newcommand{\snd}{\ensuremath{\proj2}\xspace} \newcommand{\ac}{\ensuremath{\mathsf{ac}}\xspace} % not needed in symbol index %%% recursor and induction \newcommand{\rec}[1]{\mathsf{rec}_{#1}} \newcommand{\ind}[1]{\mathsf{ind}_{#1}} \newcommand{\indid}[1]{\ind{=_{#1}}} % (Martin-Lof) path induction principle for identity types \newcommand{\indidb}[1]{\ind{=_{#1}}'} % (Paulin-Mohring) based path induction principle for identity types %%% Uniqueness principles \newcommand{\uniq}[1]{\mathsf{uniq}_{#1}} % Paths in pairs \newcommand{\pairpath}{\ensuremath{\mathsf{pair}^{\mathord{=}}}\xspace} % \newcommand{\projpath}[1]{\proj{#1}^{\mathord{=}}} \newcommand{\projpath}[1]{\ensuremath{\apfunc{\proj{#1}}}\xspace} \newcommand{\pairct}{\ensuremath{\mathsf{pair}^{\mathord{\ct}}}\xspace} %%% For quotients %%% %\newcommand{\pairr}[1]{{\langle #1\rangle}} \newcommand{\pairr}[1]{{\mathopen{}(#1)\mathclose{}}} \newcommand{\Pairr}[1]{{\mathopen{}\left(#1\right)\mathclose{}}} % \newcommand{\type}{\ensuremath{\mathsf{Type}}} % this command is overridden below, so it's commented out \newcommand{\im}{\ensuremath{\mathsf{im}}} % the image %%% 2D path operations \newcommand{\leftwhisker}{\mathbin{{\ct}_{\mathsf{l}}}} % was \ell \newcommand{\rightwhisker}{\mathbin{{\ct}_{\mathsf{r}}}} % was r \newcommand{\hct}{\star} %%% modalities %%% \newcommand{\modal}{\ensuremath{\ocircle}} \let\reflect\modal \newcommand{\modaltype}{\ensuremath{\type_\modal}} % \newcommand{\ism}[1]{\ensuremath{\mathsf{is}_{#1}}} % \newcommand{\ismodal}{\ism{\modal}} % \newcommand{\existsmodal}{\ensuremath{{\exists}_{\modal}}} % \newcommand{\existsmodalunique}{\ensuremath{{\exists!}_{\modal}}} % \newcommand{\modalfunc}{\textsf{\modal-fun}} % \newcommand{\Ecirc}{\ensuremath{\mathsf{E}_\modal}} % \newcommand{\Mcirc}{\ensuremath{\mathsf{M}_\modal}} \newcommand{\mreturn}{\ensuremath{\eta}} \let\project\mreturn %\newcommand{\mbind}[1]{\ensuremath{\hat{#1}}} \newcommand{\ext}{\mathsf{ext}} %\newcommand{\mmap}[1]{\ensuremath{\bar{#1}}} %\newcommand{\mjoin}{\ensuremath{\mreturn^{-1}}} % Subuniverse \renewcommand{\P}{\ensuremath{\type_{P}}\xspace} %%% Localizations % \newcommand{\islocal}[1]{\ensuremath{\mathsf{islocal}_{#1}}\xspace} % \newcommand{\loc}[1]{\ensuremath{\mathcal{L}_{#1}}\xspace} %%% Identity types %%% \newcommand{\idsym}{{=}} \newcommand{\id}[3][]{\ensuremath{#2 =_{#1} #3}\xspace} \newcommand{\idtype}[3][]{\ensuremath{\mathsf{Id}_{#1}(#2,#3)}\xspace} \newcommand{\idtypevar}[1]{\ensuremath{\mathsf{Id}_{#1}}\xspace} % A propositional equality currently being defined \newcommand{\defid}{\coloneqq} %%% Dependent paths \newcommand{\dpath}[4]{#3 =^{#1}_{#2} #4} %%% singleton % \newcommand{\sgl}{\ensuremath{\mathsf{sgl}}\xspace} % \newcommand{\sctr}{\ensuremath{\mathsf{sctr}}\xspace} %%% Reflexivity terms %%% % \newcommand{\reflsym}{{\mathsf{refl}}} \newcommand{\refl}[1]{\ensuremath{\mathsf{refl}_{#1}}\xspace} %%% Path concatenation (used infix, in diagrammatic order) %%% \newcommand{\ct}{% \mathchoice{\mathbin{\raisebox{0.5ex}{$\displaystyle\centerdot$}}}% {\mathbin{\raisebox{0.5ex}{$\centerdot$}}}% {\mathbin{\raisebox{0.25ex}{$\scriptstyle\,\centerdot\,$}}}% {\mathbin{\raisebox{0.1ex}{$\scriptscriptstyle\,\centerdot\,$}}} } %%% Path reversal %%% \newcommand{\opp}[1]{\mathord{{#1}^{-1}}} \let\rev\opp %%% Coherence paths %%% \newcommand{\ctassoc}{\mathsf{assoc}} % associativity law %%% Transport (covariant) %%% \newcommand{\trans}[2]{\ensuremath{{#1}_{*}\mathopen{}\left({#2}\right)\mathclose{}}\xspace} \let\Trans\trans %\newcommand{\Trans}[2]{\ensuremath{{#1}_{*}\left({#2}\right)}\xspace} \newcommand{\transf}[1]{\ensuremath{{#1}_{*}}\xspace} % Without argument %\newcommand{\transport}[2]{\ensuremath{\mathsf{transport}_{*} \: {#2}\xspace}} \newcommand{\transfib}[3]{\ensuremath{\mathsf{transport}^{#1}(#2,#3)\xspace}} \newcommand{\Transfib}[3]{\ensuremath{\mathsf{transport}^{#1}\Big(#2,\, #3\Big)\xspace}} \newcommand{\transfibf}[1]{\ensuremath{\mathsf{transport}^{#1}\xspace}} %%% 2D transport \newcommand{\transtwo}[2]{\ensuremath{\mathsf{transport}^2\mathopen{}\left({#1},{#2}\right)\mathclose{}}\xspace} %%% Constant transport \newcommand{\transconst}[3]{\ensuremath{\mathsf{transportconst}}^{#1}_{#2}(#3)\xspace} \newcommand{\transconstf}{\ensuremath{\mathsf{transportconst}}\xspace} %%% Map on paths %%% \newcommand{\mapfunc}[1]{\ensuremath{\mathsf{ap}_{#1}}\xspace} % Without argument \newcommand{\map}[2]{\ensuremath{{#1}\mathopen{}\left({#2}\right)\mathclose{}}\xspace} \let\Ap\map %\newcommand{\Ap}[2]{\ensuremath{{#1}\left({#2}\right)}\xspace} \newcommand{\mapdepfunc}[1]{\ensuremath{\mathsf{apd}_{#1}}\xspace} % Without argument % \newcommand{\mapdep}[2]{\ensuremath{{#1}\llparenthesis{#2}\rrparenthesis}\xspace} \newcommand{\mapdep}[2]{\ensuremath{\mapdepfunc{#1}\mathopen{}\left(#2\right)\mathclose{}}\xspace} \let\apfunc\mapfunc \let\ap\map \let\apdfunc\mapdepfunc \let\apd\mapdep %%% 2D map on paths \newcommand{\aptwofunc}[1]{\ensuremath{\mathsf{ap}^2_{#1}}\xspace} \newcommand{\aptwo}[2]{\ensuremath{\aptwofunc{#1}\mathopen{}\left({#2}\right)\mathclose{}}\xspace} \newcommand{\apdtwofunc}[1]{\ensuremath{\mathsf{apd}^2_{#1}}\xspace} \newcommand{\apdtwo}[2]{\ensuremath{\apdtwofunc{#1}\mathopen{}\left(#2\right)\mathclose{}}\xspace} %%% Identity functions %%% \newcommand{\idfunc}[1][]{\ensuremath{\mathsf{id}_{#1}}\xspace} %%% Homotopies (written infix) %%% \newcommand{\htpy}{\sim} %%% Other meanings of \sim \newcommand{\bisim}{\sim} % bisimulation \newcommand{\eqr}{\sim} % an equivalence relation %%% Equivalence types %%% \newcommand{\eqv}[2]{\ensuremath{#1 \simeq #2}\xspace} \newcommand{\eqvspaced}[2]{\ensuremath{#1 \;\simeq\; #2}\xspace} \newcommand{\eqvsym}{\simeq} % infix symbol \newcommand{\texteqv}[2]{\ensuremath{\mathsf{Equiv}(#1,#2)}\xspace} \newcommand{\isequiv}{\ensuremath{\mathsf{isequiv}}} \newcommand{\qinv}{\ensuremath{\mathsf{qinv}}} \newcommand{\ishae}{\ensuremath{\mathsf{ishae}}} \newcommand{\linv}{\ensuremath{\mathsf{linv}}} \newcommand{\rinv}{\ensuremath{\mathsf{rinv}}} \newcommand{\biinv}{\ensuremath{\mathsf{biinv}}} \newcommand{\lcoh}[3]{\mathsf{lcoh}_{#1}(#2,#3)} \newcommand{\rcoh}[3]{\mathsf{rcoh}_{#1}(#2,#3)} \newcommand{\hfib}[2]{{\mathsf{fib}}_{#1}(#2)} %%% Map on total spaces %%% \newcommand{\total}[1]{\ensuremath{\mathsf{total}(#1)}} %%% Universe types %%% %\newcommand{\type}{\ensuremath{\mathsf{Type}}\xspace} \newcommand{\UU}{\ensuremath{\mathcal{U}}\xspace} \let\bbU\UU \let\type\UU % Universes of truncated types \newcommand{\typele}[1]{\ensuremath{{#1}\text-\mathsf{Type}}\xspace} \newcommand{\typeleU}[1]{\ensuremath{{#1}\text-\mathsf{Type}_\UU}\xspace} \newcommand{\typelep}[1]{\ensuremath{{(#1)}\text-\mathsf{Type}}\xspace} \newcommand{\typelepU}[1]{\ensuremath{{(#1)}\text-\mathsf{Type}_\UU}\xspace} \let\ntype\typele \let\ntypeU\typeleU \let\ntypep\typelep \let\ntypepU\typelepU \renewcommand{\set}{\ensuremath{\mathsf{Set}}\xspace} \newcommand{\setU}{\ensuremath{\mathsf{Set}_\UU}\xspace} \newcommand{\prop}{\ensuremath{\mathsf{Prop}}\xspace} \newcommand{\propU}{\ensuremath{\mathsf{Prop}_\UU}\xspace} %Pointed types \newcommand{\pointed}[1]{\ensuremath{#1_\bullet}} %%% Ordinals and cardinals \newcommand{\card}{\ensuremath{\mathsf{Card}}\xspace} \newcommand{\ord}{\ensuremath{\mathsf{Ord}}\xspace} \newcommand{\ordsl}[2]{{#1}_{/#2}} %%% Univalence \newcommand{\ua}{\ensuremath{\mathsf{ua}}\xspace} % the inverse of idtoeqv \newcommand{\idtoeqv}{\ensuremath{\mathsf{idtoeqv}}\xspace} \newcommand{\univalence}{\ensuremath{\mathsf{univalence}}\xspace} % the full axiom %%% Truncation levels \newcommand{\iscontr}{\ensuremath{\mathsf{isContr}}} \newcommand{\contr}{\ensuremath{\mathsf{contr}}} % The path to the center of contraction \newcommand{\isset}{\ensuremath{\mathsf{isSet}}} \newcommand{\isprop}{\ensuremath{\mathsf{isProp}}} % h-propositions % \newcommand{\anhprop}{a mere proposition\xspace} % \newcommand{\hprops}{mere propositions\xspace} %%% Homotopy fibers %%% %\newcommand{\hfiber}[2]{\ensuremath{\mathsf{hFiber}(#1,#2)}\xspace} \let\hfiber\hfib %%% Bracket/squash/truncation types %%% % \newcommand{\brck}[1]{\textsf{mere}(#1)} % \newcommand{\Brck}[1]{\textsf{mere}\Big(#1\Big)} % \newcommand{\trunc}[2]{\tau_{#1}(#2)} % \newcommand{\Trunc}[2]{\tau_{#1}\Big(#2\Big)} % \newcommand{\truncf}[1]{\tau_{#1}} %\newcommand{\trunc}[2]{\Vert #2\Vert_{#1}} \newcommand{\trunc}[2]{\mathopen{}\left\Vert #2\right\Vert_{#1}\mathclose{}} \newcommand{\ttrunc}[2]{\bigl\Vert #2\bigr\Vert_{#1}} \newcommand{\Trunc}[2]{\Bigl\Vert #2\Bigr\Vert_{#1}} \newcommand{\truncf}[1]{\Vert \blank \Vert_{#1}} \newcommand{\tproj}[3][]{\mathopen{}\left|#3\right|_{#2}^{#1}\mathclose{}} \newcommand{\tprojf}[2][]{|\blank|_{#2}^{#1}} \def\pizero{\trunc0} %\newcommand{\brck}[1]{\trunc{-1}{#1}} %\newcommand{\Brck}[1]{\Trunc{-1}{#1}} %\newcommand{\bproj}[1]{\tproj{-1}{#1}} %\newcommand{\bprojf}{\tprojf{-1}} \newcommand{\brck}[1]{\trunc{}{#1}} \newcommand{\bbrck}[1]{\ttrunc{}{#1}} \newcommand{\Brck}[1]{\Trunc{}{#1}} \newcommand{\bproj}[1]{\tproj{}{#1}} \newcommand{\bprojf}{\tprojf{}} % Big parentheses \newcommand{\Parens}[1]{\Bigl(#1\Bigr)} % Projection and extension for truncations \let\extendsmb\ext \newcommand{\extend}[1]{\extendsmb(#1)} % %%% The empty type \newcommand{\emptyt}{\ensuremath{\mathbf{0}}\xspace} %%% The unit type \newcommand{\unit}{\ensuremath{\mathbf{1}}\xspace} \newcommand{\ttt}{\ensuremath{\star}\xspace} %%% The two-element type \newcommand{\bool}{\ensuremath{\mathbf{2}}\xspace} \newcommand{\btrue}{{1_{\bool}}} \newcommand{\bfalse}{{0_{\bool}}} %%% Injections into binary sums and pushouts \newcommand{\inlsym}{{\mathsf{inl}}} \newcommand{\inrsym}{{\mathsf{inr}}} \newcommand{\inl}{\ensuremath\inlsym\xspace} \newcommand{\inr}{\ensuremath\inrsym\xspace} %%% The segment of the interval \newcommand{\seg}{\ensuremath{\mathsf{seg}}\xspace} %%% Free groups \newcommand{\freegroup}[1]{F(#1)} \newcommand{\freegroupx}[1]{F'(#1)} % the "other" free group %%% Glue of a pushout \newcommand{\glue}{\mathsf{glue}} %%% Colimits \newcommand{\colim}{\mathsf{colim}} \newcommand{\inc}{\mathsf{inc}} \newcommand{\cmp}{\mathsf{cmp}} %%% Circles and spheres \newcommand{\Sn}{\mathbb{S}} \newcommand{\base}{\ensuremath{\mathsf{base}}\xspace} \newcommand{\lloop}{\ensuremath{\mathsf{loop}}\xspace} \newcommand{\surf}{\ensuremath{\mathsf{surf}}\xspace} %%% Suspension \newcommand{\susp}{\Sigma} \newcommand{\north}{\mathsf{N}} \newcommand{\south}{\mathsf{S}} \newcommand{\merid}{\mathsf{merid}} %%% Blanks (shorthand for lambda abstractions) \newcommand{\blank}{\mathord{\hspace{1pt}\text{--}\hspace{1pt}}} %%% Nameless objects \newcommand{\nameless}{\mathord{\hspace{1pt}\underline{\hspace{1ex}}\hspace{1pt}}} %%% Some decorations %\newcommand{\bbU}{\ensuremath{\mathbb{U}}\xspace} % \newcommand{\bbB}{\ensuremath{\mathbb{B}}\xspace} \newcommand{\bbP}{\ensuremath{\mathbb{P}}\xspace} %%% Some categories \newcommand{\uset}{\ensuremath{\mathcal{S}et}\xspace} \newcommand{\ucat}{\ensuremath{{\mathcal{C}at}}\xspace} \newcommand{\urel}{\ensuremath{\mathcal{R}el}\xspace} \newcommand{\uhilb}{\ensuremath{\mathcal{H}ilb}\xspace} \newcommand{\utype}{\ensuremath{\mathcal{T}\!ype}\xspace} % Pullback corner \newbox\pbbox \setbox\pbbox=\hbox{\xy \POS(65,0)\ar@{-} (0,0) \ar@{-} (65,65)\endxy} \def\pb{\save[]+<3.5mm,-3.5mm>*{\copy\pbbox} \restore} % Macros for the categories chapter \newcommand{\inv}[1]{{#1}^{-1}} \newcommand{\idtoiso}{\ensuremath{\mathsf{idtoiso}}\xspace} \newcommand{\isotoid}{\ensuremath{\mathsf{isotoid}}\xspace} \newcommand{\op}{^{\mathrm{op}}} \newcommand{\y}{\ensuremath{\mathbf{y}}\xspace} \newcommand{\dgr}[1]{{#1}^{\dagger}} \newcommand{\unitaryiso}{\mathrel{\cong^\dagger}} \newcommand{\cteqv}[2]{\ensuremath{#1 \simeq #2}\xspace} \newcommand{\cteqvsym}{\simeq} % Symbol for equivalence of categories %%% Natural numbers \newcommand{\N}{\ensuremath{\mathbb{N}}\xspace} %\newcommand{\N}{\textbf{N}} \let\nat\N \newcommand{\natp}{\ensuremath{\nat'}\xspace} % alternative nat in induction chapter \newcommand{\zerop}{\ensuremath{0'}\xspace} % alternative zero in induction chapter \newcommand{\suc}{\mathsf{succ}} \newcommand{\sucp}{\ensuremath{\suc'}\xspace} % alternative suc in induction chapter \newcommand{\add}{\mathsf{add}} \newcommand{\ack}{\mathsf{ack}} \newcommand{\ite}{\mathsf{iter}} \newcommand{\assoc}{\mathsf{assoc}} \newcommand{\dbl}{\ensuremath{\mathsf{double}}} \newcommand{\dblp}{\ensuremath{\dbl'}\xspace} % alternative double in induction chapter %%% Lists \newcommand{\lst}[1]{\mathsf{List}(#1)} \newcommand{\nil}{\mathsf{nil}} \newcommand{\cons}{\mathsf{cons}} \newcommand{\lost}[1]{\mathsf{Lost}(#1)} %%% Vectors of given length, used in induction chapter \newcommand{\vect}[2]{\ensuremath{\mathsf{Vec}_{#1}(#2)}\xspace} %%% Integers \newcommand{\Z}{\ensuremath{\mathbb{Z}}\xspace} \newcommand{\Zsuc}{\mathsf{succ}} \newcommand{\Zpred}{\mathsf{pred}} %%% Rationals \newcommand{\Q}{\ensuremath{\mathbb{Q}}\xspace} %%% Function extensionality \newcommand{\funext}{\mathsf{funext}} \newcommand{\happly}{\mathsf{happly}} %%% A naturality lemma \newcommand{\com}[3]{\mathsf{swap}_{#1,#2}(#3)} %%% Code/encode/decode \newcommand{\code}{\ensuremath{\mathsf{code}}\xspace} \newcommand{\encode}{\ensuremath{\mathsf{encode}}\xspace} \newcommand{\decode}{\ensuremath{\mathsf{decode}}\xspace} % Function definition with domain and codomain \newcommand{\function}[4]{\left\{\begin{array}{rcl}#1 & \longrightarrow & #2 \\ #3 & \longmapsto & #4 \end{array}\right.} %%% Cones and cocones \newcommand{\cone}[2]{\mathsf{cone}_{#1}(#2)} \newcommand{\cocone}[2]{\mathsf{cocone}_{#1}(#2)} % Apply a function to a cocone \newcommand{\composecocone}[2]{#1\circ#2} \newcommand{\composecone}[2]{#2\circ#1} %%% Diagrams \newcommand{\Ddiag}{\mathscr{D}} %%% (pointed) mapping spaces \newcommand{\Map}{\mathsf{Map}} %%% The interval \newcommand{\interval}{\ensuremath{I}\xspace} \newcommand{\izero}{\ensuremath{0_{\interval}}\xspace} \newcommand{\ione}{\ensuremath{1_{\interval}}\xspace} %%% Arrows \newcommand{\epi}{\ensuremath{\twoheadrightarrow}} \newcommand{\mono}{\ensuremath{\rightarrowtail}} %%% Sets \newcommand{\bin}{\ensuremath{\mathrel{\widetilde{\in}}}} %%% Semigroup structure \newcommand{\semigroupstrsym}{\ensuremath{\mathsf{SemigroupStr}}} \newcommand{\semigroupstr}[1]{\ensuremath{\mathsf{SemigroupStr}}(#1)} \newcommand{\semigroup}[0]{\ensuremath{\mathsf{Semigroup}}} %%% Macros for the formal type theory \newcommand{\emptyctx}{\ensuremath{\cdot}} \newcommand{\production}{\vcentcolon\vcentcolon=} \newcommand{\conv}{\downarrow} \newcommand{\ctx}{\ensuremath{\mathsf{ctx}}} \newcommand{\wfctx}[1]{#1\ \ctx} \newcommand{\oftp}[3]{#1 \vdash #2 : #3} \newcommand{\jdeqtp}[4]{#1 \vdash #2 \jdeq #3 : #4} \newcommand{\judg}[2]{#1 \vdash #2} \newcommand{\tmtp}[2]{#1 \mathord{:} #2} % rule names \newcommand{\rform}{\textsc{form}} \newcommand{\rintro}{\textsc{intro}} \newcommand{\relim}{\textsc{elim}} \newcommand{\rcomp}{\textsc{comp}} \newcommand{\runiq}{\textsc{uniq}} \newcommand{\Weak}{\mathsf{Wkg}} \newcommand{\Vble}{\mathsf{Vble}} \newcommand{\Exch}{\mathsf{Exch}} \newcommand{\Subst}{\mathsf{Subst}} %%% Macros for HITs \newcommand{\cc}{\mathsf{c}} \newcommand{\pp}{\mathsf{p}} \newcommand{\cct}{\widetilde{\mathsf{c}}} \newcommand{\ppt}{\widetilde{\mathsf{p}}} \newcommand{\Wtil}{\ensuremath{\widetilde{W}}\xspace} %%% Macros for n-types \newcommand{\istype}[1]{\mathsf{is}\mbox{-}{#1}\mbox{-}\mathsf{type}} \newcommand{\nplusone}{\ensuremath{(n+1)}} \newcommand{\nminusone}{\ensuremath{(n-1)}} \newcommand{\fact}{\mathsf{fact}} %%% Macros for homotopy \newcommand{\kbar}{\overline{k}} % Used in van Kampen's theorem %%% Macros for induction \newcommand{\natw}{\ensuremath{\mathbf{N^w}}\xspace} \newcommand{\zerow}{\ensuremath{0^\mathbf{w}}\xspace} \newcommand{\sucw}{\ensuremath{\mathsf{succ}^{\mathbf{w}}}\xspace} \newcommand{\nalg}{\nat\mathsf{Alg}} \newcommand{\nhom}{\nat\mathsf{Hom}} \newcommand{\ishinitw}{\mathsf{isHinit}_{\mathsf{W}}} \newcommand{\ishinitn}{\mathsf{isHinit}_\nat} \newcommand{\w}{\mathsf{W}} \newcommand{\walg}{\w\mathsf{Alg}} \newcommand{\whom}{\w\mathsf{Hom}} %%% Macros for real numbers \newcommand{\RC}{\ensuremath{\mathbb{R}_\mathsf{c}}\xspace} % Cauchy \newcommand{\RD}{\ensuremath{\mathbb{R}_\mathsf{d}}\xspace} % Dedekind \newcommand{\R}{\ensuremath{\mathbb{R}}\xspace} % Either \newcommand{\barRD}{\ensuremath{\bar{\mathbb{R}}_\mathsf{d}}\xspace} % Dedekind completion of Dedekind \newcommand{\close}[1]{\sim_{#1}} % Relation of closeness \newcommand{\closesym}{\mathord\sim} \newcommand{\rclim}{\mathsf{lim}} % HIT constructor for Cauchy reals \newcommand{\rcrat}{\mathsf{rat}} % Embedding of rationals into Cauchy reals \newcommand{\rceq}{\mathsf{eq}_{\RC}} % HIT path constructor \newcommand{\CAP}{\mathcal{C}} % The type of Cauchy approximations \newcommand{\Qp}{\Q_{+}} \newcommand{\apart}{\mathrel{\#}} % apartness \newcommand{\dcut}{\mathsf{isCut}} % Dedekind cut \newcommand{\cover}{\triangleleft} % inductive cover \newcommand{\intfam}[3]{(#2, \lam{#1} #3)} % family of rational intervals % Macros for the Cauchy reals construction \newcommand{\bsim}{\frown} \newcommand{\bbsim}{\smile} \newcommand{\hapx}{\diamondsuit\approx} \newcommand{\hapname}{\diamondsuit} \newcommand{\hapxb}{\heartsuit\approx} \newcommand{\hapbname}{\heartsuit} \newcommand{\tap}[1]{\bullet\approx_{#1}\triangle} \newcommand{\tapname}{\triangle} \newcommand{\tapb}[1]{\bullet\approx_{#1}\square} \newcommand{\tapbname}{\square} %%% Macros for surreals \newcommand{\NO}{\ensuremath{\mathsf{No}}\xspace} \newcommand{\surr}[2]{\{\,#1\,\big|\,#2\,\}} \newcommand{\LL}{\mathcal{L}} \newcommand{\RR}{\mathcal{R}} \newcommand{\noeq}{\mathsf{eq}_{\NO}} % HIT path constructor \newcommand{\ble}{\trianglelefteqslant} \newcommand{\blt}{\vartriangleleft} \newcommand{\bble}{\sqsubseteq} \newcommand{\bblt}{\sqsubset} \newcommand{\hle}{\diamondsuit\preceq} \newcommand{\hlt}{\diamondsuit\prec} \newcommand{\hlname}{\diamondsuit} \newcommand{\hleb}{\heartsuit\preceq} \newcommand{\hltb}{\heartsuit\prec} \newcommand{\hlbname}{\heartsuit} % \newcommand{\tle}{(\bullet\preceq\triangle)} % \newcommand{\tlt}{(\bullet\prec\triangle)} \newcommand{\tle}{\triangle\preceq} \newcommand{\tlt}{\triangle\prec} \newcommand{\tlname}{\triangle} % \newcommand{\tleb}{(\bullet\preceq\square)} % \newcommand{\tltb}{(\bullet\prec\square)} \newcommand{\tleb}{\square\preceq} \newcommand{\tltb}{\square\prec} \newcommand{\tlbname}{\square} %%% Macros for set theory \newcommand{\vset}{\mathsf{set}} % point constructor for cummulative hierarchy V \def\cd{\tproj0} \newcommand{\inj}{\ensuremath{\mathsf{inj}}} % type of injections \newcommand{\acc}{\ensuremath{\mathsf{acc}}} % accessibility \newcommand{\atMostOne}{\mathsf{atMostOne}} \newcommand{\power}[1]{\mathcal{P}(#1)} % power set \newcommand{\powerp}[1]{\mathcal{P}_+(#1)} % inhabited power set %%%% THEOREM ENVIRONMENTS %%%% % The cleveref package provides \cref{...} which is like \ref{...} % except that it automatically inserts the type of the thing you're % referring to, e.g. it produces "Theorem 3.8" instead of just "3.8" % (and hyperref makes the whole thing a hyperlink). This saves a slight amount % of typing, but more importantly it means that if you decide later on % that 3.8 should be a Lemma or a Definition instead of a Theorem, you % don't have to change the name in all the places you referred to it. % The following hack improves on this by using the same counter for % all theorem-type environments, so that after Theorem 1.1 comes % Corollary 1.2 rather than Corollary 1.1. This makes it much easier % for the reader to find a particular theorem when flipping through % the document. \makeatletter \def\defthm#1#2#3{% %% Ensure all theorem types are numbered with the same counter \newaliascnt{#1}{thm} \newtheorem{#1}[#1]{#2} \aliascntresetthe{#1} %% This command tells cleveref's \cref what to call things \crefname{#1}{#2}{#3}% following brace must be on separate line to support poorman cleveref sed file } % Now define a bunch of theorem-type environments. \newtheorem{thm}{Theorem}[section] \crefname{thm}{Theorem}{Theorems} %\defthm{prop}{Proposition} % Probably we shouldn't use "Proposition" in this way \defthm{cor}{Corollary}{Corollaries} \defthm{lem}{Lemma}{Lemmas} \defthm{axiom}{Axiom}{Axioms} % Since definitions and theorems in type theory are synonymous, should % we actually use the same theoremstyle for them? \theoremstyle{definition} \defthm{defn}{Definition}{Definitions} \theoremstyle{remark} \defthm{rmk}{Remark}{Remarks} \defthm{eg}{Example}{Examples} \defthm{egs}{Examples}{Examples} \defthm{notes}{Notes}{Notes} % Number exercises within chapters, with their own counter. \newtheorem{ex}{Exercise}[chapter] \crefname{ex}{Exercise}{Exercises} % Display format for sections \crefformat{section}{\S#2#1#3} \Crefformat{section}{Section~#2#1#3} \crefrangeformat{section}{\S\S#3#1#4--#5#2#6} \Crefrangeformat{section}{Sections~#3#1#4--#5#2#6} \crefmultiformat{section}{\S\S#2#1#3}{ and~#2#1#3}{, #2#1#3}{ and~#2#1#3} \Crefmultiformat{section}{Sections~#2#1#3}{ and~#2#1#3}{, #2#1#3}{ and~#2#1#3} \crefrangemultiformat{section}{\S\S#3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}{, #3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6} \Crefrangemultiformat{section}{Sections~#3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}{, #3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6} % Display format for appendices \crefformat{appendix}{Appendix~#2#1#3} \Crefformat{appendix}{Appendix~#2#1#3} \crefrangeformat{appendix}{Appendices~#3#1#4--#5#2#6} \Crefrangeformat{appendix}{Appendices~#3#1#4--#5#2#6} \crefmultiformat{appendix}{Appendices~#2#1#3}{ and~#2#1#3}{, #2#1#3}{ and~#2#1#3} \Crefmultiformat{appendix}{Appendices~#2#1#3}{ and~#2#1#3}{, #2#1#3}{ and~#2#1#3} \crefrangemultiformat{appendix}{Appendices~#3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}{, #3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6} \Crefrangemultiformat{appendix}{Appendices~#3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6}{, #3#1#4--#5#2#6}{ and~#3#1#4--#5#2#6} \crefname{part}{Part}{Parts} % Number subsubsections \setcounter{secnumdepth}{5} % Display format for figures \crefname{figure}{Figure}{Figures} %%%% EQUATION NUMBERING %%%% % The following hack uses the single theorem counter to number % equations as well, so that we don't have both Theorem 1.1 and % equation (1.1). \let\c@equation\c@thm \numberwithin{equation}{section} %%%% ENUMERATE NUMBERING %%%% % Number the first level of enumerates as (i), (ii), ... \renewcommand{\theenumi}{(\roman{enumi})} \renewcommand{\labelenumi}{\theenumi} %%%% MARGINS %%%% % This is a matter of personal preference, but I think the left % margins on enumerates and itemizes are too wide. \setitemize[1]{leftmargin=2em} \setenumerate[1]{leftmargin=*} % Likewise that they are too spaced out. \setitemize[1]{itemsep=-0.2em} \setenumerate[1]{itemsep=-0.2em} %%% Notes %%% \def\noteson{% \gdef\note##1{\mbox{}\marginpar{\color{blue}\textasteriskcentered\ ##1}}} \gdef\notesoff{\gdef\note##1{\null}} \noteson \newcommand{\Coq}{\textsc{Coq}\xspace} \newcommand{\Agda}{\textsc{Agda}\xspace} \newcommand{\NuPRL}{\textsc{NuPRL}\xspace} %%%% CITATIONS %%%% % \let \cite \citep %%%% INDEX %%%% \newcommand{\footstyle}[1]{{\hyperpage{#1}}n} % If you index something that is in a footnote \newcommand{\defstyle}[1]{\textbf{\hyperpage{#1}}} % Style for pageref to a definition \newcommand{\indexdef}[1]{\index{#1|defstyle}} % Index a definition \newcommand{\indexfoot}[1]{\index{#1|footstyle}} % Index a term in a footnote \newcommand{\indexsee}[2]{\index{#1|see{#2}}} % Index "see also" %%%% Standard phrasing or spelling of common phrases %%%% \newcommand{\ZF}{Zermelo--Fraenkel} \newcommand{\CZF}{Constructive \ZF{} Set Theory} \newcommand{\LEM}[1]{\ensuremath{\mathsf{LEM}_{#1}}\xspace} \newcommand{\choice}[1]{\ensuremath{\mathsf{AC}_{#1}}\xspace} %%%% MISC %%%% \newcommand{\mentalpause}{\medskip} % Use for "mental" pause, instead of \smallskip or \medskip %% Use \symlabel instead of \label to mark a pageref that you need in the index of symbols \newcounter{symindex} \newcommand{\symlabel}[1]{\refstepcounter{symindex}\label{#1}} % Local Variables: % mode: latex % TeX-master: "hott-online" % End: