fredefox/cat
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Only index some things, change crossref to citation

Browse source
This commit is contained in:
Frederik Hanghøj Iversen 2018-05-09 18:29:44 +02:00
parent d8f1aabed5
commit bc8309c0cd
2 changed files with 53 additions and 51 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/cubical.tex
View file

@ -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

102
doc/macros.tex
View file

@ -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}}