diff --git a/doc/cubical.tex b/doc/cubical.tex index 097a996..c9c6ece 100644 --- a/doc/cubical.tex +++ b/doc/cubical.tex @@ -210,7 +210,7 @@ Then comes the set of homotopical sets: \end{equation} % I won't give an example of a set at this point. It turns out that proving e.g. -$\isProp\ \bN$ is not so straight-forward (see \S3.1.4 in \ref{hott-2013}). +$\isProp\ \bN$ is not so straight-forward (see \cite[\S3.1.4]{hott-2013}). There will be examples of sets later in this report. At this point it should be noted that the term ``set'' is somewhat conflated; there is the notion of sets from set-theory, in Agda types are denoted \texttt{Set}. I will use it diff --git a/doc/macros.tex b/doc/macros.tex index bbc917d..f43fa0c 100644 --- a/doc/macros.tex +++ b/doc/macros.tex @@ -31,60 +31,62 @@ \resizebox{\@tempdima}{\height}{=}% } \makeatother -\newcommand{\var}[1]{\ensuremath{\mathit{#1}}\index{#1}} -\newcommand{\Hom}{\var{Hom}} -\newcommand{\fmap}{\var{fmap}} -\newcommand{\bind}{\var{bind}} -\newcommand{\join}{\var{join}} -\newcommand{\omap}{\var{omap}} -\newcommand{\pure}{\var{pure}} -\newcommand{\idFun}{\var{id}} -\newcommand{\Sets}{\var{Sets}} -\newcommand{\Set}{\var{Set}} -\newcommand{\hSet}{\var{hSet}} -\newcommand{\id}{\var{id}} -\newcommand{\isEquiv}{\var{isEquiv}} -\newcommand{\idToIso}{\var{idToIso}} -\newcommand{\idIso}{\var{idIso}} -\newcommand{\isSet}{\var{isSet}} -\newcommand{\isContr}{\var{isContr}} -\newcommand{\isGroupoid}{\var{isGroupoid}} -\newcommand{\pathJ}{\var{pathJ}} -\newcommand\Object{\var{Object}} -\newcommand\Functor{\var{Functor}} -\newcommand\isProp{\var{isProp}} -\newcommand\propPi{\var{propPi}} -\newcommand\propSig{\var{propSig}} -\newcommand\PreCategory{\var{PreCategory}} -\newcommand\IsPreCategory{\var{IsPreCategory}} -\newcommand\isIdentity{\var{isIdentity}} -\newcommand\propIsIdentity{\var{propIsIdentity}} -\newcommand\IsCategory{\var{IsCategory}} -\newcommand\Gl{\var{\lambda}} -\newcommand\lemPropF{\var{lemPropF}} -\newcommand\isPreCategory{\var{isPreCategory}} -\newcommand\congruence{\var{cong}} -\newcommand\identity{\var{identity}} -\newcommand\isequiv{\var{isequiv}} -\newcommand\qinv{\var{qinv}} -\newcommand\fiber{\var{fiber}} -\newcommand\shuffle{\var{shuffle}} -\newcommand\Univalent{\var{Univalent}} -\newcommand\refl{\var{refl}} -\newcommand\isoToId{\var{isoToId}} -\newcommand\Isomorphism{\var{Isomorphism}} +\newcommand{\var}[1]{\ensuremath{\mathit{#1}}} +\newcommand{\varindex}[1]{\ensuremath{\mathit{#1}}\index{#1}} + +\newcommand{\Hom}{\varindex{Hom}} +\newcommand{\fmap}{\varindex{fmap}} +\newcommand{\bind}{\varindex{bind}} +\newcommand{\join}{\varindex{join}} +\newcommand{\omap}{\varindex{omap}} +\newcommand{\pure}{\varindex{pure}} +\newcommand{\idFun}{\varindex{id}} +\newcommand{\Sets}{\varindex{Sets}} +\newcommand{\Set}{\varindex{Set}} +\newcommand{\hSet}{\varindex{hSet}} +\newcommand{\id}{\varindex{id}} +\newcommand{\isEquiv}{\varindex{isEquiv}} +\newcommand{\idToIso}{\varindex{idToIso}} +\newcommand{\idIso}{\varindex{idIso}} +\newcommand{\isSet}{\varindex{isSet}} +\newcommand{\isContr}{\varindex{isContr}} +\newcommand{\isGroupoid}{\varindex{isGroupoid}} +\newcommand{\pathJ}{\varindex{pathJ}} +\newcommand\Object{\varindex{Object}} +\newcommand\Functor{\varindex{Functor}} +\newcommand\isProp{\varindex{isProp}} +\newcommand\propPi{\varindex{propPi}} +\newcommand\propSig{\varindex{propSig}} +\newcommand\PreCategory{\varindex{PreCategory}} +\newcommand\IsPreCategory{\varindex{IsPreCategory}} +\newcommand\isIdentity{\varindex{isIdentity}} +\newcommand\propIsIdentity{\varindex{propIsIdentity}} +\newcommand\IsCategory{\varindex{IsCategory}} +\newcommand\Gl{\varindex{\lambda}} +\newcommand\lemPropF{\varindex{lemPropF}} +\newcommand\isPreCategory{\varindex{isPreCategory}} +\newcommand\congruence{\varindex{cong}} +\newcommand\identity{\varindex{identity}} +\newcommand\isequiv{\varindex{isequiv}} +\newcommand\qinv{\varindex{qinv}} +\newcommand\fiber{\varindex{fiber}} +\newcommand\shuffle{\varindex{shuffle}} +\newcommand\Univalent{\varindex{Univalent}} +\newcommand\refl{\varindex{refl}} +\newcommand\isoToId{\varindex{isoToId}} +\newcommand\Isomorphism{\varindex{Isomorphism}} \newcommand\rrr{\ggg} \newcommand\fish{\mathrel{\wideoverbar{\rrr}}} -\newcommand\fst{\var{fst}} -\newcommand\snd{\var{snd}} -\newcommand\Path{\var{Path}} -\newcommand\Category{\var{Category}} +\newcommand\fst{\varindex{fst}} +\newcommand\snd{\varindex{snd}} +\newcommand\Path{\varindex{Path}} +\newcommand\Category{\varindex{Category}} \newcommand\TODO[1]{TODO: \emph{#1}} \newcommand*{\QED}{\hfill\ensuremath{\square}}% \newcommand\uexists{\exists!} -\newcommand\Arrow{\var{Arrow}} -\newcommand\NTsym{\var{NT}} +\newcommand\Arrow{\varindex{Arrow}} +\newcommand\NTsym{\varindex{NT}} \newcommand\NT[2]{\NTsym\ #1\ #2} -\newcommand\Endo[1]{\var{Endo}\ #1} +\newcommand\Endo[1]{\varindex{Endo}\ #1} \newcommand\EndoR{\mathcal{R}} -\newcommand\funExt{\var{funExt}} +\newcommand\funExt{\varindex{funExt}}