diff --git a/Notes/macros.tex b/Notes/macros.tex
new file mode 100644
index 0000000..9085053
--- /dev/null
+++ b/Notes/macros.tex
@@ -0,0 +1,781 @@
+%%%% 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@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}\,}
+
+%%% 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}{\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
+\newcommand{\un}{\ensuremath{\mathsf{upun}}\xspace} % not needed in symbol index, uniqueness principle for unit type
+
+%%% 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 
+
+%%% the uniqueness principle for product types, formerly called surjective pairing and named \spr:
+\newcommand{\uppt}{\ensuremath{\mathsf{uppt}}\xspace}
+
+% Paths in pairs
+\newcommand{\pairpath}{\ensuremath{\mathsf{pair}^{\mathord{=}}}\xspace}
+% \newcommand{\projpath}[1]{\proj{#1}^{\mathord{=}}}
+\newcommand{\projpath}[1]{\ensuremath{\apfunc{\proj{#1}}}\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}_{\ell}}}
+\newcommand{\rightwhisker}{\mathbin{{\ct}_{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
+
+%%% 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}}
+
+%%% 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}}
+
+%%% 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{\form}{\textsc{form}}
+\newcommand{\intro}{\textsc{intro}}
+\newcommand{\elim}{\textsc{elim}}
+\newcommand{\comp}{\textsc{comp}}
+\newcommand{\uniq}{\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{\mathbf{s^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 %%%%
+
+% Hyperref includes the command \autoref{...} 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 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}}
+
+% 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}
+
+% Use cleveref instead of hyperref's \autoref
+\let\autoref\cref
+
+
+%%%% 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:
diff --git a/Notes/notes.tex b/Notes/notes.tex
new file mode 100644
index 0000000..4b1ed1e
--- /dev/null
+++ b/Notes/notes.tex
@@ -0,0 +1,640 @@
+\documentclass{article}
+
+\input{preamble-articles}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% We define a command \@ifnextcharamong accepting an arbitrary number of
+%%%% arguments. The first is what it should do if a match is found, the second
+%%%% contains what it should do when no match is found; all the other arguments
+%%%% are the things it tries to find as the next character.
+%%%%
+%%%% For example \@ifnextcharamong{#1}{#2}{*}{\bgroup} expands #1 if the next
+%%%% character is a * or a \bgroup and it expands #2 otherwise.
+
+\makeatletter
+\newcommand{\@ifnextcharamong}[2]
+  {\@ifnextchar\bgroup{\@@ifnextchar{#1}{\@@ifnextcharamong{#1}{#2}}}{#2}}
+\newcommand{\@@ifnextchar}[3]{\@ifnextchar{#3}{#1}{#2}}
+\newcommand{\@@ifnextcharamong}[3]{\@ifnextcharamong{#1}{#2}}
+\makeatother
+
+\newcommand{\ucomp}[1]{\hat{#1}}
+\newcommand{\finset}[1]{{[#1]}}
+
+\makeatletter
+\newcommand{\higherequifibsf}{\mathcal}
+\newcommand{\higherequifib}[2]{\higherequifibsf{#1}(#2)}
+\newcommand{\underlyinggraph}[1]{U(#1)}
+\newcommand{\theequifib}[1]{{\def\higherequifibsf{}#1}}
+\makeatother
+
+\newcommand{\loopspace}[2][]{\typefont{\Omega}^{#1}(#2)}
+\newcommand{\join}[2]{{#1}*{#2}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\title{Notes on algebraic topology}
+\date{\today}
+
+\begin{document}
+
+\maketitle
+
+\tableofcontents
+
+\part{Spectral sequences}
+\section{Background}
+\begin{defn}
+A graded $R$-module $M$ is an $R$-module which decomposes as a direct
+sum
+\begin{equation*}
+\bigoplus_{p\in\Z} F_p M
+\end{equation*}
+of $R$-modules. A graded $R$-homomorphism $h:M\to N$ is an $R$-homomorphism which
+decomposes into $h_p:F_pM\to F_pN$. 
+\end{defn}
+
+\begin{lem}
+Suppose $M$ and $N$ are graded $R$-modules. Then $M\otimes N$ is a graded
+$R$-module by
+\begin{equation*}
+(M\otimes_R N)_i\defeq \bigoplus_{p+q=i} F_pM\otimes_R F_qN.
+\end{equation*}
+\end{lem}
+
+\begin{defn}
+A graded algebra is a graded $R$-module $M$ for which there are linear mappings
+$\varphi_{p,q}:F_pM\otimes_R F_qM\to F_{p+q}M$, i.e.~a graded $R$-homomorphism
+$\varphi:M\otimes M\to M$, which is associative in the sense
+that the diagram
+\begin{equation*}
+\begin{tikzcd}
+M\otimes M\otimes M \arrow[r,"\varphi\otimes 1"] \arrow[d,swap,"1\otimes\varphi"] &
+M\otimes M \arrow[d,"\varphi"] \\ M\otimes M \arrow[r,swap,"\varphi"] & M
+\end{tikzcd}
+\end{equation*}
+commutes.
+\end{defn}
+
+\begin{eg}
+Polynomials with coefficients in $R$ forms a graded algebra. Moreover, in the
+polynomial ring $R[X]$, we find that $G_pR[X]\defeq F_pR[X]/F_{p-1}R[X]\cong R$.
+Since those are free modules, we have that $R[X]\cong \bigoplus_p G_pR[X]$. 
+\end{eg}
+
+\section{Spectral sequences}
+
+\subsection{Motivation from the long exact sequence of a pair}
+
+Recall that a pair of spaces $(X,A)$ induces a long exact sequence of homology
+groups
+\begin{equation*}
+\begin{tikzcd}
+\cdots \arrow[r,"\partial_{n+1}"]
+& H_n(A) \arrow[r,"i_n"]
+& H_n(X) \arrow[r,"j_n"]
+& H_n(X,A) \arrow[r,"\partial_n"]
+& H_{n-1}(A) \arrow[r,"i_{n-1}"]
+& \cdots
+\end{tikzcd}
+\end{equation*}
+from the short exact sequence
+\begin{equation*}
+\begin{tikzcd}
+0 \arrow[r] & C_\ast(A) \arrow[r] & C_\ast(X) \arrow[r] & C_\ast(X,A) \arrow[r] & 0
+\end{tikzcd}
+\end{equation*}
+of chain complexes, by means of the snake lemma. This long exact sequence helps
+us to compute $H_n(X)$ in terms of $H_n(A)$ and $H_n(X,A)$, which may be easier
+to determine. For instance, from the long exact sequence we obtain the short
+exact sequence
+\begin{equation*}
+\begin{tikzcd}
+0 \arrow[r] & \mathrm{coker}(\partial_{n+1}) \arrow[r] & H_n(X) \arrow[r] & \mathrm{ker}(\partial_n) \arrow[r] & 0
+\end{tikzcd}
+\end{equation*}
+and hence we have determined that $H_n(X)$ can be obtained as some element of the
+group $\mathrm{Ext}(\mathrm{coker}(\partial_{n+1}),\mathrm{ker}(\partial_n))$.
+In other words, $H_n(X)$ is a particular solution to an extension problem.
+
+Note also that the long exact sequence of relative homology groups can be
+presented as an exact triangle of graded $R$-homomorphisms:
+\begin{equation*}
+\begin{tikzcd}[column sep=0em]
+\bigoplus_n H_n(C_\ast(A)) 
+\arrow[rr,"i"] & & \bigoplus_n H_n(C_\ast(X)) \arrow[dl,"j"] \\
+& \bigoplus_n H_n(C_\ast(X,A)) \arrow[ul,"\partial"]
+\end{tikzcd}
+\end{equation*}
+
+The first idea of spectral sequences is to generalize the long exact sequence
+of homology obtained from a pair of spaces, to an algebraic gadget obtained from
+a filtration on a space, and mimic the derivation of determining the homology
+group as a solution to an extension problem.
+
+\begin{defn}
+A filtration of a space X consists of a sequence 
+\begin{equation*}
+\cdots\subseteq X_p\subseteq X_{p+1}\subseteq\cdots
+\end{equation*}
+such that $X=\bigcup_p X_p$ and $\bigcap_p X_p=\varnothing$. A filtration of $X$ is said to be bounded, if
+$X_p=\varnothing$ for $p$ sufficiently small, and $X_p=X$ for $X$ sufficiently
+large.
+\end{defn}
+
+An important class of filtered spaces is that of CW-complexes, where the filtration
+$X_p$ of $X$ is given by the $p$-skeleton of $X$. Another case is where
+$X_p\defeq\varnothing$ for $p<0$, $X_0\defeq A$ and $X_p\defeq X$ for $p>0$; here
+we recover the old theory of the topological pair.
+
+\begin{defn}
+Given a space $X$ with a filtration, we can form the staircase diagram
+\begin{footnotesize}
+\begin{equation*}
+\begin{tikzcd}
+& \vdots \arrow[d] & & \vdots \arrow[d] \\ 
+\cdots \arrow[r]
+& H_{n+1}(X_p) \arrow[r] \arrow[d]
+& H_{n+1}(X_p,X_{p-1}) \arrow[r]
+& H_n(X_{p-1}) \arrow[r] \arrow[d]
+& H_n(X_{p-1},X_{p-2}) \arrow[r]
+& \cdots \\
+\cdots \arrow[r]
+& H_{n+1}(X_{p+1}) \arrow[r] \arrow[d]
+& H_{n+1}(X_{p+1},X_{p}) \arrow[r]
+& H_n(X_{p}) \arrow[r] \arrow[d]
+& H_n(X_{p},X_{p-1}) \arrow[r]
+& \cdots \\
+& \vdots & & \vdots
+\end{tikzcd}
+\end{equation*}%
+\end{footnotesize}%
+in which the familiar long exact sequence of the pairs $(X_p,X_{p-1})$ run
+down like a staircase.
+\end{defn}
+
+\begin{defn}
+Let $X$ be a space with a filtration. Then we obtain the exact couple
+\begin{equation*}
+\begin{tikzcd}
+A \arrow[rr,"i"] & & A \arrow[dl,"j"] \\
+& E \arrow[ul,"\partial"]
+\end{tikzcd}
+\end{equation*}
+in which $A\defeq\bigoplus_{p,n} H_n(X_p)$, and $E\defeq\bigoplus_{p,n}H_n(X_p,X_{p-1})$. 
+\end{defn}
+
+We can come to such an exact couple from any filtered chain complex, which is
+what we turn our attention to before continuing.
+
+\subsection{The spectral sequence of a filtered complex}
+
+\begin{defn}
+A filtration of an $R$-module $M$ consists of a sequence
+\begin{equation*}
+\cdots\subseteq F_pM\subseteq F_{p+1}M\subseteq\cdots
+\end{equation*}
+of $R$-submodules of $M$, such that $M=\bigcup_p F_pM$ and $\bigcap_p F_pM=0$. 
+A filtration of $R$ is said to be bounded if $F_pM=0$ for $p$ sufficiently
+small and $F_pM=M$ for $p$ sufficiently large.
+\end{defn}
+
+\begin{defn}
+Let $\{M,F_pM\}$ be a graded $R$-module. The associated graded module is defined
+by $G_p M\defeq F_pM/F_{p-1}M$. We obtain a short exact sequence
+\begin{equation*}
+\begin{tikzcd}
+0 \arrow[r] & F_{p-1}M \arrow[r] & F_pM \arrow[r] & G_pM \arrow[r] & 0.
+\end{tikzcd}
+\end{equation*}
+\end{defn}
+
+\begin{rmk}
+It would be nice if $F_pM\cong F_{p-1}M\oplus G_pM$, so that we can write
+$M\cong\bigoplus_p G_pM$. Under what condition does this hold? This holds if
+each $G_pM$ is a projective $R$-module, so under what conditions is this true?
+\end{rmk}
+
+\begin{defn}
+A filtered chain complex is a chain complex $(C_\ast,\partial)$ together with a
+filtration $\{F_pC_i\}$ of each $C_i$, such that the differential preserves the
+filtration, i.e.~$\partial(F_pC_i)\subseteq F_p C_{i-1}$. 
+
+A filtration of a chain complex is said to be bounded if it is bounded in each
+dimension.
+\end{defn}
+
+Let $(F_pC_\ast,\partial)$ be a filtered chain complex. We have again our
+short exact sequence
+\begin{equation*}
+\begin{tikzcd}
+0 \arrow[r] & F_{p-1} C_\ast \arrow[r] & F_p C_\ast \arrow[r] & G_p C_\ast \arrow[r] & 0
+\end{tikzcd}
+\end{equation*}
+of chain complexes. This also gives us the long exact sequence on homology,
+which we may express conveniently as the exact couple
+\begin{equation*}
+\begin{tikzcd}[column sep=0em]
+\bigoplus_{p,q} H_{p+q}(F_pC_\ast) \arrow[rr,"i"] & & \bigoplus_{p,q} H_{p+q}(F_pC_\ast) \arrow[dl,"j"] \\
+& \bigoplus_{p,q} H_{p+q}(G_p C_\ast) \arrow[ul,"k"]
+\end{tikzcd}
+\end{equation*}
+consisting of graded $R$-homomorphisms (of which $k$ shifts in degree).
+
+\begin{defn}
+Consider an exact couple, i.e.~a commutative triangle
+\begin{equation*}
+\begin{tikzcd}
+A \arrow[rr,"i"] & & A \arrow[dl,"j"] \\ & E \arrow[ul,"k"]
+\end{tikzcd}
+\end{equation*}
+of $R$-modules, which is exact at every vertex. Taking $\partial^0\defeq j\circ k$,
+we see that $(\partial^0)^2=0$ by exactness. We may now form the derived exact couple
+\begin{equation*}
+\begin{tikzcd}[column sep=0]
+\mathrm{im}(i) \arrow[rr,"i'"] & & \mathrm{im}(i) \arrow[dl,"j'"] \\
+& \frac{\mathrm{ker}(\partial)}{\mathrm{im}(\partial)} \arrow[ul,"k'"]
+\end{tikzcd}
+\end{equation*}
+where
+\begin{align*}
+i'(i(a)) & \defeq i(i(a)) \\
+j'(i(a)) & \defeq [j(a)] \\
+k'([e]) & \defeq k(e)
+\end{align*}
+\end{defn}
+
+\begin{rmk}
+Since quotients commute with direct sums (both are colimits), it follows that
+\begin{equation*}
+E'\defeq \frac{\mathrm{ker}(\partial)}{\mathrm{im}(\partial)}
+  \cong
+\bigoplus_{p,q} \frac{\mathrm{ker}(\partial^0_{p,q})}{\mathrm{im}(\partial^0_{p,q+1})}
+\end{equation*}
+is a graded $R$-module. In other words, $E'$ is a direct sum of the homology
+groups of the $p$-indexed family of chain complexes
+\begin{equation*}
+\begin{tikzcd}
+\cdots \arrow[r] & E_{p,q}^0 \arrow[r,"{\partial^0_{p,q}}"] & E_{p,q-1}^0 \arrow[r] & \cdots
+\end{tikzcd}
+\end{equation*}
+It follows that $i'$, $j'$ and $k'$ are graded
+whenever $i$, $j$ and $k$ are, where $k'$ shifts down in dimension the same way 
+$k$ does.
+\end{rmk}
+
+\begin{comment}
+\begin{defn}
+We define
+\begin{equation*}
+E_{p,q}^0\defeq G_pC_{p+q}\defeq F_pC_{p+1}/F_{p-1}C_{p+q},
+\end{equation*}
+
+Since the differential preserves the filtration, we obtain from the differentials
+well-defined $R$-homomorphisms functioning as the boundary maps in the chain complex
+
+\end{defn}
+
+\begin{defn}
+The homology groups 
+\begin{equation*}
+E^1_{p,q}\defeq \mathrm{ker}(\partial^0_{p,q})/\mathrm{im}(\partial^0_{p,q+1})
+\end{equation*}
+form again a chain complex, with boundary maps $\partial^1_{p,q}:E^1_{p,q}\to
+E^1_{p,q-1}$. Thus, this process may be repeated indefinitely.
+\end{defn}
+\end{comment}
+
+\begin{comment}
+\begin{lem}
+Let $(C_\ast,\partial)$ be a filtered chain complex. Then there is a filtration
+on the homology of $C_\ast$, given by
+\begin{equation*}
+F_pH_i(C_\ast)\defeq\{\alpha\in H_i(C_\ast)\mid \exists_{(x\in F_p C_i)}\,\alpha=[x]\}.
+\end{equation*}
+\end{lem}
+\end{comment}
+
+\subsection{Convergent spectral sequences}
+
+\begin{defn}
+A spectral sequence consists of
+\begin{enumerate}
+\item An $R$-module $E^r_{p,q}$ for each $p,q\in\Z$ and each $r\geq 0$.
+\item Differentials $\partial_r:E^r_{p,q}\to E^r_{p-r,q+r-1}$ such that
+$\partial_r^2=0$ and $E^{r+1}$ is the homology of $(E^r,\partial_r)$ 
+\end{enumerate}
+\end{defn}
+
+\begin{defn}
+A spectral sequence $\{E^r,\partial_r\}$ of $R$-modules is said to converge 
+if for every $p,q\in\Z$, one has $\partial_r=0:E^r_{p,q}\to E^r_{p-r,q+r-1}$
+for $r$ sufficiently large.
+\end{defn}
+
+\begin{rmk}
+If a spectral sequence $\{E^r,\partial_r\}$ converges, then the $R$-module
+$E^r_{p,q}$ is independent of $r$ for sufficiently large $r$. 
+\end{rmk}
+
+\begin{thm}
+Let $(F_pC_\ast,\partial)$ be a filtered complex. Then we obtain a spectral
+sequence $(E^r_{p,q},\partial^r)$ defined for $r\geq 0$, with
+\begin{equation*}
+E^1_{p,q}\defeq H_{p+q}(G_pC_\ast).
+\end{equation*}
+This is the spectral sequence of filtered complexes.
+\end{thm}
+
+\begin{thm}
+If $(F_pC_\ast,\partial)$ is a bounded filtered complex, then the spectral
+sequence converges to
+\begin{equation*}
+E^\infty_{p,q}\defeq G_pH_{p+q}(C_\ast).
+\end{equation*}
+\end{thm}
+
+Let $X$ be a filtered space, and let our goal be to compute the $n$-th (co)homology
+group $H_n(X)$. In general, this might be a complicated task. However, it might
+be easier to compute the homologies of the subcomplex $C_\ast(X_p)$, and the quotient
+complex $C_\ast(X)/C_\ast(X_p)$. From this, we obtain a short exact sequence
+\begin{equation*}
+\begin{tikzcd}
+0 \arrow[r]
+& \mathrm{coker}(\delta) \arrow[r]
+& H_\ast(X) \arrow[r]
+& \mathrm{ker}(\delta) \arrow[r]
+& 0
+\end{tikzcd}
+\end{equation*}
+
+\subsection{The Serre spectral sequence}
+
+The Serre spectral sequence relates the homology of a Serre fibration to the
+homology of the fibers and the base. Thus, in some cases one can compute the
+homology of the fibration in terms of the homology of the fibers and the base.
+
+Let $\pi : X\to B$ be a fibration, with $B$ a path-connected CW-complex, and we
+filter $X$ by the subspaces $X_p\defeq \pi^{-1}(B_p)$, in which $B_p$ is the
+$p$-skeleton of $B$. 
+
+\begin{lem}
+The spectral sequence for homology with coefficients in $G$ associated to this
+filtration of $X$ converges to $H_\ast(X;G)$.
+\end{lem}
+
+\begin{thm}
+Let $F\to X\to B$ be a fibration with $B$ path-connected. If $\pi_1(B)$ acts
+trivially on $H_\ast(F;G)$, then there is a spectral sequence $\{E^r_{p,q},\partial_r\}$
+with:
+\begin{enumerate}
+%\item $\partial_r : E^r_{p,q}\to E^r_{p-r,q+r-1}$ and $E^{r+1}_{p,q}=\mathrm{ker}\,d_r/\mathrm{im}\,dr$. 
+\item the stable terms $E^\infty_{p,n-p}$ are isomorphic to $F^p_n/F^{p-1}_n$ in
+a filtration $0\subseteq F^0_n\subseteq\cdots\subseteq F^n_n=H_n(X;G)$ of ...
+\item $E^2_{p,q}\cong H_p(B;H_q(F;G))$. 
+\end{enumerate}
+\end{thm}
+
+\part{K-theory}
+
+\section{Vector bundles}
+
+\subsection{Basic spaces}
+\begin{defn}
+The \define{$n$-sphere} $\Sn^n$ is the subspace of $\R^{n+1}$ consisting of unit vectors.
+The \define{real projective $n$-space} $\R P^n$  is the space of lines in
+$\R^{n+1}$ through the origin. Equivalently, we may regard $\R P^n$ as the quotient
+space of $\Sn^n$ in which the antipodal pairs of points are identified. Notice
+that $\R P^1\approx \Sn^1$. 
+\end{defn}
+
+\begin{defn}
+For each $n$, we may include the $n$-sphere $\Sn^n$ into $\Sn^{n+1}$ by mapping
+it into the equator. These inclusions induce inclusions $\R P^n\to \R P^{n+1}$.
+We define $\R P^\infty$ to be the sequential colimit of $\R P^n$. 
+\end{defn}
+
+\subsection{Definition and basic properties}
+\begin{defn}
+An \define{$n$-dimensional vector bundle} is a map $p:E\to B$ together with a
+real vector space structure on $p^{-1}(b)$ for each $b\in B$, satisfying the
+\define{local triviality condition}, which says that there is an open cover 
+$\mathcal{C}$ of $B$, with homeomorphisms $h_U:p^{-1}(U)\to U\times\mathbb{R}^n$
+for each $U\in\mathcal{C}$, which maps $p^{-1}(b)$ to $\{b\}\times\mathbb{R}^n$
+for each $b\in U$. 
+
+The functions $h_U$ are also called \define{local trivializations}. Given a
+vector bundle $p:E\to B$, the space $B$ is called the \define{base space}, the
+space $E$ is called the \define{total space}, and the spaces $p^{-1}(b)$ are
+called the \define{fibers}. A $1$-dimensional
+vector bundle is also called a \define{line bundle}.
+\end{defn}
+
+\begin{defn}
+An \define{isomorphism of vector bundles} from $p:E\to B$ to $p':E'\to B$
+consists of a map $h:E\to E'$ satisfying $p'\circ h=p$, 
+which induces a linear isomorphism
+$p^{-1}(b)\to p'^{-1}(b)$ between each of the fibers.
+\end{defn}
+
+\begin{lem}
+If $h:E\to E'$ is an isomorphism of vector bundles, then the underlying map
+of type $E\to E'$ is a homeomorphism. 
+\end{lem}
+
+\begin{proof}
+Suppose $h:E\to E'$ induces isomorphisms $p^{-1}(b)\to p'^{-1}(b)$ for each
+$b\in B$. Then, for each $x\in E'$ we have an isomorphism from
+$p^{-1}(p'(x))$ to $p'^{-1}(p'(x))$. Since $x\in p'^{-1}(p'(x))$, we find
+an element $y\in p^{-1}(p'(x))\subseteq E$. Thus, $h$ is surjective. Now suppose
+that $x,x'\in E$ are two elements for which $h(x)=h(x')$. Since $p'\circ h=p$,
+it follows that $x'\in p^{-1}(x)$. Now, the fact that $h$ induces an isomorphism
+between fibers implies that $x=x'$. 
+
+Thus, $h$ has an inverse function $k:E'\to E$, and we need to show that this
+function is continuous. It suffices to show that $k|_U$ is continuous for each
+$U$ on which $p'$ is trivial. Let $x\in B$, and compose the map
+$h_U:p^{-1}(U)\to p'^{-1}(U)$ with its local trivializations. Thus, we obtain
+a map $g_U:U\times\R^n\to U\times \R^n$, mapping $(x,y)$ to $(x,A(y))$, where
+$A$ is a linear isomorphism. 
+\end{proof}
+
+In the following definition, we give a vector bundle by a gluing construction.
+
+\begin{defn}
+Consider a space $B$, and an open cover $\mathcal{C}$ which is closed under
+finite intersections. Then $\mathcal{C}$ may be considered a poset ordered by
+inclusion.
+
+A \define{collection of gluing functions} consists of a continuous choice of linear 
+isomorphisms $g_{U,V}:U\cap V\to GL_n(\R)$ satisfying the \define{cocycle
+condition} 
+\begin{equation*}
+g_{V,W}\circ g_{U,V}=g_{U,W}
+\end{equation*}
+on $U\cap V\cap W$, for every 
+$U,V,W\in\mathcal{C}$. Such a collection of gluing functions determines a functor
+$\mathcal{C}\to\mathbf{Top}$, which is given on points by $U\mapsto U\times\R^n$,
+and on morphisms by $(x,v)\mapsto(x,A(v))$, for each $U\subseteq V$ determining
+a linear isomorphism $A$. 
+
+The colimit of this functor is the total space of a vector bundle.
+\end{defn}
+
+\begin{eg}
+There are lots of examples of vector bundles:
+\begin{enumerate}
+\item The \define{$n$-dimensional trivial bundle} over $B$ is defined to be 
+$\proj1:B\times\mathbb{R}^n\to B$. So the trivial bundle is the one which is
+\emph{globally} trivial. We will write the $n$-dimensional trivial bundle over
+$B$ as $\epsilon^n\to B$. 
+\item The circle may be regarded as the quotient of $[0,1]$ modulo the end points.
+The \define{Mobius bundle} is the line bundle over $\Sn^1$ to have total space
+$E\defeq [0,1]\times\R$, with the identifications $(0,t)\sim(1,-t)$. 
+\item The \define{tangent bundle} of the unit sphere $\Sn^n$, viewed as a subspace of
+$\R^{n+1}$, is defined to be the subspace $E\defeq\{(x,v)\in\Sn^n\times\R^{n+1}
+\mid x\perp v\}$ of $\R^{2n+2}$, which projects onto $\Sn^n$. 
+
+The $n$-sphere is covered by $2n+2$ open hemispheres, centering at $\pm e_i$,
+where $e_i\in\R^{n+1}$ is a basis vector. 
+\item The \define{normal bundle} of the unit sphere $\Sn^n$ is the line bundle
+with $E$ consisting of pairs $(x,v)\in\Sn^n\times\R^{n+1}$ such that $v=tx$ for
+some $t\in\R$. \emph{The normal bundle on $\Sn^n$ is isomorphic to the trivial line 
+bundle $\Sn^n\times\R\to\Sn^n$.}
+\item The \define{canonical line bundle} $p:E\to \R P^n$ has as its total space
+the subspace $E\subseteq \R P^{n+1}\times\R ^{n+1}$ consisting of pairs
+$(l,v)$ with $v\in l$. \emph{The M\"obius line bundle is isomorphic to the
+canonical line bundle on $\Sn^1$.}
+\item The inclusions $\R P^n\subseteq \R P^{n+1}$ induce inclusions of the
+canonical line bundles. The sequential colimit of the canonical line bundles
+produces the canonical line bundle on $\R P^\infty$. 
+\end{enumerate}
+\end{eg}
+
+\begin{defn}
+Given two vector bundles $p:E\to B$ and $p':E'\to B$ over the same base space
+$B$, we obtain a vector bundle $p\oplus p': E\oplus E'\to B$, fitting in the
+pullback square
+\begin{equation*}
+\begin{tikzcd}
+E\oplus E' \arrow[r] \arrow[d] \arrow[dr,"{p\oplus p'}" description ] & E' \arrow[d,"{p'}"] \\
+E \arrow[r,swap,"p"] & B
+\end{tikzcd}
+\end{equation*}
+\end{defn}
+
+\begin{eg}
+\begin{enumerate}
+\item The direct sum of the tangent and normal bundles on $\Sn^n$ is the trivial
+bundle $\Sn^n\times\R^{n+1}$. 
+\end{enumerate}
+\end{eg}
+
+\begin{defn}
+Let $p:E\to B$ and $p':E'\to B$ be two vector bundles over the same space $B$,
+and choose an open cover $\mathcal{C}$ such that both $E$ and $E'$ are locally
+trivial with respect to $\mathcal{C}$. We define $E\otimes E'$ by gluing. 
+
+Then we can define, for each $U,V\in\mathcal{C}$ satisfying $U\subseteq V$, we
+have linear isomorphisms $g_{U,V}(x):\R^n\to\R^n$ and $g'_{U,V}(x):\R^m\to\R^m$,
+induced by the local trivializations of $E$ and $E'$ respectively. These give
+gluing functions $g_{U,V}(x)\otimes g'_{U,V}(x):\R^n\otimes\R^m\to\R^n\otimes\R^m$
+for each $x\in U$, and these gluing functions satisfy the cocycle condition.
+
+Thus, we obtain a vector bundle $E\otimes E'$ from these gluing functions.
+\end{defn}
+
+\begin{lem}
+The tensor product of vector bundles over a fixed base space is commutative,
+associative, it has an identity element (the trivial bundle), and it is
+distributive with respect to direct sum.
+\end{lem}
+
+Change of base $f:B'\to B$ turns a vector bundle $E$ over $B$ to a vector
+bundle $f^\ast(E)$ over $B'$.
+
+\begin{lem}
+For any two vector bundles $E$ and $E'$ over $B$, and any $f:B'\to B$, we have
+natural isomorphisms $f^\ast(E\oplus E')\approx f^\ast(E)\oplus f^\ast(E')$, and
+$f^\ast(E\otimes E')\approx f^\ast(E)\otimes f^\ast(E')$. Moreover, if $f$
+is homotopic to $g$, then $f^\ast=g^\ast$. 
+\end{lem}
+
+\subsection{K-theory}
+
+\begin{defn}
+Two vector bundles $E\to B$ and $E'\to B$ are callec \define{stably isomorphic},
+if there is an $n$ for which $E\oplus\epsilon^n\approx E'\oplus\epsilon^n$, and
+we write $E\approx_s E'$ if $E$ and $E'$ are stably isomorphic. Also,
+we will define the relation $E\sim E'$ if there are $m$ and $n$ such that
+$E\oplus\epsilon^m\approx E'\oplus^n$. 
+\end{defn}
+
+\begin{lem}
+The direct sum preserves both $\approx_s$ and $\sim$. Moreover, if $B$ is compact,
+then the set of ${\sim}$-equivalence classes of vector bundles forms an abelian
+group, called $\tilde{K}(B)$. If $B$ is pointed, then the tensor product turns 
+$\tilde{K}(B)$ into a ring.
+\end{lem}
+
+\begin{lem}
+The direct sum satisfies the cancellation property with respect to $\approx_s$,
+i.e.~we have that $E\oplus E'\approx_s E\oplus E''$ implies $E'\oplus E''$. 
+Thus, if we define two pairs $(E,F)$ and $(E',F')$ to be equivalent to each
+other whenever $E\oplus F'=E'\oplus F$, we obtain an abelian group $K(B)$ for
+any compact space $B$. The tensor product turns $K(B)$ into a ring.
+\end{lem}
+
+\begin{lem}
+We have a ring isomorphism
+\begin{equation*}
+K(B)\approx \tilde{K}(B)\oplus\Z.
+\end{equation*}
+\end{lem}
+
+Both $K$ and $\tilde{K}$ are contravariant functors.
+
+\begin{lem}
+If $X$ is compact Hausdorff and $A\subseteq X$ is a closed subspace, then the
+inclusion and quotient maps $A\stackrel{i}{\to}X\stackrel{q}{\to}X/A$ induces
+an sequence
+\begin{equation*}
+\begin{tikzcd}
+\tilde{K}(X/A) \arrow[r,"q^\ast"] & \tilde{K}(X) \arrow[r,"i^\ast"] & \tilde{K}(A)
+\end{tikzcd}
+\end{equation*}
+which is exact at $\tilde{K}(X)$.
+\end{lem}
+
+\begin{lem}
+If $A$ is contractible, the quotient map $q:X\to X/A$ induces a bijection
+$q^\ast:\mathrm{Vect}^n(X/A)\to\mathrm{Vect}^n(X)$.
+\end{lem}
+
+Apparently, this gives a long exact sequence of $\tilde{K}$-groups:
+\begin{equation*}
+\begin{tikzcd}[column sep=small]
+\cdots\arrow[r] & \tilde{K}(\Sn(X)) \arrow[r] & \tilde{K}(\Sn(A)) \arrow[r]
+& \tilde{K}(X/A) \arrow[r] & \tilde{K}(X) \arrow[r] & \tilde{K}(A).
+\end{tikzcd}
+\end{equation*}
+Still considering pointed spaces, we may consider the long exact sequence of the pair $(X\times Y,
+X\vee Y)$. Recall that $(X\times Y)/(X\vee Y)$ is the smash product
+$X\wedge Y$, i.e.~the smash product is the pushout of $\unit\leftarrow
+X\vee Y\rightarrow X\times Y$. The long exact sequence of the pair
+$(X\times Y,X\vee Y)$ looks as follows:
+\begin{equation*}
+\begin{tikzcd}[column sep=.8em]
+\cdots\arrow[r] & \tilde{K}(\Sn(X\times Y)) \arrow[r] & \tilde{K}(\Sn(X\vee Y)) \arrow[r]
+& \tilde{K}(X\wedge Y) \arrow[r] & \tilde{K}(X\times Y) \arrow[r] & \tilde{K}(X\vee Y).
+\end{tikzcd}
+\end{equation*}  
+
+\subsection{Bott periodicity}
+
+\begin{defn}
+We define an \define{external product} $\mu:K(X)\otimes K(Y)\to K(X\times Y)$,
+by $\mu(a\otimes b)\defeq \proj1^\ast(a)\cdot\proj2^\ast(b)$. 
+\end{defn}
+
+
+\end{document}
diff --git a/Notes/preamble-articles.tex b/Notes/preamble-articles.tex
new file mode 100644
index 0000000..f5d0adc
--- /dev/null
+++ b/Notes/preamble-articles.tex
@@ -0,0 +1,508 @@
+% for type setting urls
+\usepackage[hyphens]{url} % This package has to be loaded *before* hyperref
+\usepackage[pagebackref,colorlinks,citecolor=darkgreen,linkcolor=darkgreen,unicode]{hyperref}
+\usepackage[english]{babel}
+
+%%% Because Germans have umlauts and Slavs have even stranger ways of mangling letters
+\usepackage[utf8]{inputenc}
+
+%%% Multi-Columns for long lists of names
+\usepackage{multicol}
+
+%%% Set the fonts
+\usepackage{mathpazo}
+\usepackage[scaled=0.95]{helvet}
+\usepackage{courier}
+\linespread{1.05} % Palatino looks better with this
+
+\usepackage{graphicx}
+\usepackage{comment}
+
+%\usepackage{wallpaper} % For the background image on the cover page
+%\usepackage{geometry} % For the cover page
+\usepackage{fancyhdr} % To set headers and footers
+
+\usepackage{ifthen}
+\usepackage{amssymb,amsmath,amsthm,stmaryrd,mathrsfs,wasysym}
+\usepackage{enumitem,mathtools,xspace,xcolor}
+\definecolor{darkgreen}{rgb}{0,0.45,0}
+\usepackage{aliascnt}
+\usepackage[capitalize]{cleveref}
+%\usepackage[all,2cell]{xy}
+%\UseAllTwocells
+% \usepackage{natbib}
+\usepackage{braket} % used for \setof{ ... } macro
+\usepackage{tikz-cd}
+\usepackage{tikz}
+\usetikzlibrary{decorations.pathmorphing}
+\usepackage[inference]{semantic}
+\usepackage{booktabs}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% To include references in TOC we should use this package rather than a hack.
+\usepackage{tocbibind}
+%\usepackage{etoolbox}           % get \apptocmd
+%\apptocmd{\thebibliography}{\addcontentsline{toc}{section}{References}}{}{} % tell bibliography to get itself into the table of contents
+
+
+\begin{comment}
+%%%% Header and footers
+\pagestyle{fancyplain}
+\setlength{\headheight}{15pt}
+\renewcommand{\chaptermark}[1]{\markboth{\textsc{Chapter \thechapter. #1}}{}}
+\renewcommand{\sectionmark}[1]{\markright{\textsc{\thesection\ #1}}}
+\end{comment}
+
+% TOC depth
+\setcounter{tocdepth}{2}
+
+\lhead[\fancyplain{}{{\thepage}}]%
+      {\fancyplain{}{\nouppercase{\rightmark}}}
+\rhead[\fancyplain{}{\nouppercase{\leftmark}}]%
+      {\fancyplain{}{\thepage}}
+\cfoot{\textsc{\footnotesize [Draft of \today]}}
+\lfoot[]{}
+\rfoot[]{}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% We mostly use the macros of the book, to keep notations
+%%%% and conventions the same. Recall that when the macros file
+%%%% is updated, we need to comment the lines containing the
+%%%% string `[chapter]` since our article is not a book.
+%%%%
+%%%% Instructions for updating the macros.tex file:
+%%%% - fetch the latest macros.tex file from the HoTT/book git repository.
+%%%% - comment all lines containing "[chapter]" because this is not a book.
+%%%% - comment the definition of pbcorner because the xypic package is not used.
+%%%%
+\input{macros}
+
+\newcommand{\idsymbin}{=}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% Our commands which are not part of the macros.tex file.
+%%%% We should keep these commands separate, because we will
+%%%% update the macros.tex following the updates of the book.
+
+%%%% First we redefine the \id, \eqv and \ct commands so that they accept an
+%%%% arbitrary number of arguments. This is useful when writing longer strings
+%%%% of equalities or equivalences.
+
+\makeatletter
+
+\renewcommand{\id}[3][]{
+  \@ifnextchar\bgroup
+    {#2 \mathbin{\idsym_{#1}} \id[#1]{#3}}
+    {#2 \mathbin{\idsym_{#1}} #3}
+  }
+
+\renewcommand{\eqv}[2]{
+  \@ifnextchar\bgroup
+    {#1 \eqvsym \eqv{#2}}
+    {#1 \eqvsym #2}
+  }
+
+\newcommand{\ctsym}{%
+  \mathchoice{\mathbin{\raisebox{0.5ex}{$\displaystyle\centerdot$}}}%
+             {\mathbin{\raisebox{0.5ex}{$\centerdot$}}}%
+             {\mathbin{\raisebox{0.25ex}{$\scriptstyle\,\centerdot\,$}}}%
+             {\mathbin{\raisebox{0.1ex}{$\scriptscriptstyle\,\centerdot\,$}}}
+  }
+
+\renewcommand{\ct}[3][]{
+  \@ifnextchar\bgroup
+    {#2 \mathbin{\ctsym_{#1}} \ct[#1]{#3}}
+    {#2 \mathbin{\ctsym_{#1}} #3}
+  }
+
+\makeatother
+
+%%%% We always use textstyle products and sums...
+%\renewcommand{\prd}{\tprd}
+%\renewcommand{\sm}{\tsm}
+\makeatletter
+\renewcommand{\@dprd}{\@tprd}
+\renewcommand{\@dsm}{\@tsm}
+\renewcommand{\@dprd@noparens}{\@tprd}
+\renewcommand{\@dsm@noparens}{\@tsm}
+
+%%%% ...with a bit more spacing
+\renewcommand{\@tprd}[1]{\mathchoice{{\textstyle\prod_{(#1)}\,}}{\prod_{(#1)}\,}{\prod_{(#1)}\,}{\prod_{(#1)}\,}}
+\renewcommand{\@tsm}[1]{\mathchoice{{\textstyle\sum_{(#1)}\,}}{\sum_{(#1)}\,}{\sum_{(#1)}\,}{\sum_{(#1)}\,}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% We adjust the \prd command so that implicit arguments become possible.
+%%%%
+%%%% First, we have the following switch. Set it to true if implicit arguments
+%%%% are desired, or to false if not. Note turning off implicit arguments
+%%%% might render some parts of the text harder to comprehend, since in the
+%%%% text might appear $f(x)$ where we would have $f(i,x)$ without implicit
+%%%% arguments.
+
+\newcommand{\implicitargumentson}{\boolean{true}}
+
+%%%% If one wants to use implicit arguments in the notation for product types,
+%%%% a * has to be put before the argument that has to be implicit.
+%%%% For example: in $\prd{x:A}*{y:B}{u:P(y)}Q(x,y,u)$, the argument y is
+%%%% implicit. Any of the arguments can be made implicit this way.
+
+%%%% First of all, we should make the command \prd search not only for a
+%%%% brace, but also for a star. We introduce an auxiliary command that
+%%%% determines whether the next character is a star or brace.
+\newcommand{\@ifnextchar@starorbrace}[2]
+%  {\@ifnextcharamong{#1}{#2}{*}{\bgroup};}
+  {\@ifnextchar*{#1}{\@ifnextchar\bgroup{#1}{#2}}}
+  
+%%%% When encountering the \prd command, latex should determine whether it
+%%%% should print implicit argument brackets or not. So the first branching
+%%%% happens right here.
+\renewcommand{\prd}{\@ifnextchar*{\@iprd}{\@prd}}
+
+\newcommand{\@prd}[1]
+  {\@ifnextchar@starorbrace
+    {\prd@parens{#1}}
+    {\@ifnextchar\sm{\prd@parens{#1}\@eatsm}{\prd@noparens{#1}}}}
+\newcommand{\@prd@parens}{\@ifnextchar*{\@iprd}{\prd@parens}}
+\renewcommand{\prd@parens}[1]
+  {\@ifnextchar@starorbrace
+    {\@theprd{#1}\@prd@parens}
+    {\@ifnextchar\sm{\@theprd{#1}\@eatsm}{\@theprd{#1}}}}
+\newcommand{\@theprd}[1]
+  {\mathchoice{\@dprd{#1}}{\@tprd{#1}}{\@tprd{#1}}{\@tprd{#1}}}
+\renewcommand{\dprd}[1]{\@dprd{#1}\@ifnextchar@starorbrace{\dprd}{}}
+\renewcommand{\tprd}[1]{\@tprd{#1}\@ifnextchar@starorbrace{\tprd}{}}
+
+%%%% Here we tell the actual symbols to be printed.
+\newcommand{\@theiprd}[1]{\mathchoice{\@diprd{#1}}{\@tiprd{#1}}{\@tiprd{#1}}{\@tiprd{#1}}}
+\newcommand{\@iprd}[2]{\@ifnextchar@starorbrace%
+  {\@theiprd{#2}\@prd@parens}%
+  {\@ifnextchar\sm%
+    {\@theiprd{#2}\@eatsm}%
+    {\@theiprd{#2}}}}
+\def\@tiprd#1{
+  \ifthenelse{\implicitargumentson}
+    {\@@tiprd{#1}\@ifnextchar\bgroup{\@tiprd}{}}
+    {\@tprd{#1}}}
+\def\@@tiprd#1{\mathchoice{{\textstyle\prod_{\{#1\}}\,}}{\prod_{\{#1\}}\,}{\prod_{\{#1\}}\,}{\prod_{\{#1\}}\,}}
+\def\@diprd{
+  \ifthenelse{\implicitargumentson}
+    {\@tiprd}
+    {\@tprd}}
+    
+
+%%%% And finally we need to redefine \@eatprd so that implicit arguments also
+%%%% works in the scope of a dependent sum.    
+\def\@eatprd\prd{\@prd@parens}
+
+\makeatother
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% Redefining the quantifiers, so that some of the longer 
+%%%% formulas appear one a single line without problems
+
+%%% Dependent products written with \forall, in the same style
+\makeatletter
+\def\tfall#1{\forall_{(#1)}\@ifnextchar\bgroup{\,\tfall}{\,}}
+\renewcommand{\fall}{\tfall}
+
+%%% Existential quantifier %%%
+\def\texis#1{\exists_{(#1)}\@ifnextchar\bgroup{\,\texis}{\,}}
+\renewcommand{\exis}{\texis}
+
+%%% Unique existence %%%
+\def\uexis#1{\exists!_{(#1)}\@ifnextchar\bgroup{\,\uexis}{\,}}
+\makeatother
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+%%%% Introducing logical usage of fonts.
+\newcommand{\modelfont}{\mathit} % use 'mf' in command to indicate model font
+\newcommand{\typefont}{\mathsf} % use 'tf' in command to indicate type font
+\newcommand{\catfont}{\mathrm} % use 'cf' in command to indicate cat font
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% Some macros of the book are redefined.
+
+\renewcommand{\UU}{\typefont{U}}
+\renewcommand{\isequiv}{\typefont{isEquiv}}
+\renewcommand{\happly}{\typefont{hApply}}
+\renewcommand{\pairr}[1]{{\mathopen{}\langle #1\rangle\mathclose{}}}
+\renewcommand{\type}{\typefont{Type}}
+\renewcommand{\op}[1]{{{#1}^\typefont{op}}}
+\renewcommand{\susp}{\typefont{\Sigma}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% The following is a big unorganized list of new macros that we use in the
+%%%% notes. 
+
+\newcommand{\mfM}{\modelfont{M}}
+\newcommand{\mfN}{\modelfont{N}}
+\newcommand{\tfctx}{\typefont{ctx}}
+\newcommand{\mftypfunc}[1]{{\modelfont{typ}^{#1}}}
+\newcommand{\mftyp}[2]{{\mftypfunc{#1}(#2)}}
+\newcommand{\tftypfunc}[1]{{\typefont{typ}^{#1}}}
+\newcommand{\tftyp}[2]{{\tftypfunc{#1}(#2)}}
+\newcommand{\hfibfunc}[1]{\typefont{fib}_{#1}}
+\newcommand{\mappingcone}[1]{\mathcal{C}_{#1}}
+\newcommand{\equifib}{\typefont{equiFib}}
+\newcommand{\tfcolim}{\typefont{colim}}
+\newcommand{\tflim}{\typefont{lim}}
+\newcommand{\tfdiag}{\typefont{diag}}
+\newcommand{\tfGraph}{\typefont{Graph}}
+\newcommand{\mfGraph}{\modelfont{Graph}}
+\newcommand{\unitGraph}{\unit^\mfGraph}
+\newcommand{\UUGraph}{\UU^\mfGraph}
+\newcommand{\tfrGraph}{\typefont{rGraph}}
+\newcommand{\mfrGraph}{\modelfont{rGraph}}
+\newcommand{\isfunction}{\typefont{isFunction}}
+\newcommand{\tfconst}{\typefont{const}}
+\newcommand{\conemap}{\typefont{coneMap}}
+\newcommand{\coconemap}{\typefont{coconeMap}}
+\newcommand{\tflimits}{\typefont{limits}}
+\newcommand{\tfcolimits}{\typefont{colimits}}
+\newcommand{\islimiting}{\typefont{isLimiting}}
+\newcommand{\iscolimiting}{\typefont{isColimiting}}
+\newcommand{\islimit}{\typefont{isLimit}}
+\newcommand{\iscolimit}{\typefont{iscolimit}}
+\newcommand{\pbcone}{\typefont{cone_{pb}}}
+\newcommand{\tfinj}{\typefont{inj}}
+\newcommand{\tfsurj}{\typefont{surj}}
+\newcommand{\tfepi}{\typefont{epi}}
+\newcommand{\tftop}{\typefont{top}}
+\newcommand{\sbrck}[1]{\Vert #1\Vert}
+\newcommand{\strunc}[2]{\Vert #2\Vert_{#1}}
+\newcommand{\gobjclass}{{\typefont{U}^\mfGraph}}
+\newcommand{\gcharmap}{\typefont{fib}}
+\newcommand{\diagclass}{\typefont{T}}
+\newcommand{\opdiagclass}{\op{\diagclass}}
+\newcommand{\equifibclass}{\diagclass^{\eqv{}{}}}
+\newcommand{\universe}{\typefont{U}}
+\newcommand{\catid}[1]{{\catfont{id}_{#1}}}
+\newcommand{\isleftfib}{\typefont{isLeftFib}}
+\newcommand{\isrightfib}{\typefont{isRightFib}}
+\newcommand{\leftLiftings}{\typefont{leftLiftings}}
+\newcommand{\rightLiftings}{\typefont{rightLiftings}}
+\newcommand{\psh}{\typefont{Psh}}
+\newcommand{\rgclass}{\typefont{\Omega^{RG}}}
+\newcommand{\terms}[2][]{\lfloor #2 \rfloor^{#1}}
+\newcommand{\grconstr}[2]
+             {\mathchoice % max size is textstyle size.
+             {{\textstyle \int_{#1}}#2}% 
+             {\int_{#1}#2}%
+             {\int_{#1}#2}%
+             {\int_{#1}#2}}
+\newcommand{\ctxhom}[3][]{\typefont{hom}_{#1}(#2,#3)}
+\newcommand{\graphcharmapfunc}[1]{\gcharmap_{#1}}
+\newcommand{\graphcharmap}[2][]{\graphcharmapfunc{#1}(#2)}
+\newcommand{\tfexp}[1]{\typefont{exp}_{#1}}
+\newcommand{\tffamfunc}{\typefont{fam}}
+\newcommand{\tffam}[1]{\tffamfunc(#1)}
+\newcommand{\tfev}{\typefont{ev}}
+\newcommand{\tfcomp}{\typefont{comp}}
+\newcommand{\isDec}[1]{\typefont{isDecidable}(#1)}
+\newcommand{\smal}{\mathcal{S}}
+\renewcommand{\modal}{{\ensuremath{\ocircle}}}
+\newcommand{\eqrel}{\typefont{EqRel}}
+\newcommand{\piw}{\ensuremath{\Pi\typefont{W}}} %% to be used in conjunction with -pretopos.
+\renewcommand{\sslash}{/\!\!/}
+\newcommand{\mprd}[2]{\Pi(#1,#2)}
+\newcommand{\msm}[2]{\Sigma(#1,#2)}
+\newcommand{\midt}[1]{\idvartype_#1}
+\newcommand{\reflf}[1]{\typefont{refl}^{#1}}
+\newcommand{\tfJ}{\typefont{J}}
+\newcommand{\tftrans}{\typefont{trans}}
+
+\newcommand{\tfT}{\typefont{T}}
+\newcommand{\reflsym}{{\mathsf{refl}}}
+\newcommand{\strans}[2]{\ensuremath{{#1}_{*}({#2})}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% JUDGMENTS
+%%%%
+%%%% Below we define several commands for the judgments of type theory. There
+%%%% are commands
+%%%% * \jctx for the judgment that something is a context.
+%%%% * \jctxeq for the judgment that two contexts are the same
+%%%% * \jtype for the judgment that something is a type in a context
+%%%% * \jtypeeq for the judgment that two types in the same context are the same
+%%%% * \jterm for the judgment that something is a term of a type in a context
+%%%% * \jtermeq for the judgment that two terms of the same type are the same
+
+\makeatletter
+\newcommand{\jctx}{\@ifnextchar*{\@jctxAlignTrue}{\@jctxAlignFalse}}
+\newcommand{\@jctxAlignTrue}[2]{& \vdash #2~ctx}
+\newcommand{\@jctxAlignFalse}[1]{\vdash #1~ctx}
+
+\newcommand{\jtype}{\@ifnextchar*{\@jtypeAlignTrue}{\@jtypeAlignFalse}}
+\newcommand{\@jtypeAlignFalse}[2]{#1\vdash #2~type}
+\newcommand{\@jtypeAlignTrue}[3]{#2 & \vdash #3~type}
+
+\newcommand{\jtermc}{\@ifnextchar*{\@jtermcAlignTrue}{\@jtermcAlignFalse}}
+\newcommand{\@jtermcAlignTrue}[3]{ & \vdash #3:#2}
+\newcommand{\@jtermcAlignFalse}[2]{\vdash #2:#1}
+
+\newcommand{\jtermt}{\@ifnextchar*{\@jtermtAlignTrue}{\@jtermtAlignFalse}}
+\newcommand{\@jtermtAlignTrue}[4]{#2 & \vdash #4:#3}
+\newcommand{\@jtermtAlignFalse}[3]{#1 \vdash #3:#2}
+
+\newcommand{\jctxeq}{\@ifnextchar*{\@jctxeqAlignTrue}{\@jctxeqAlignFalse}}
+\newcommand{\@jctxeqAlignTrue}[3]{& \vdash #2\jdeq #3~ctx}
+\newcommand{\@jctxeqAlignFalse}[2]{\vdash #1\jdeq #2~ctx}
+
+\newcommand{\jtypeeq}{\@ifnextchar*{\@jtypeeqAlignTrue}{\@jtypeeqAlignFalse}}
+\newcommand{\@jtypeeqAlignTrue}[4]{#2 & \vdash #3\jdeq #4~type}
+\newcommand{\@jtypeeqAlignFalse}[3]{#1\vdash #2\jdeq #3~type}
+
+\newcommand{\jtermceq}{\@ifnextchar*{\@jtermceqAlignTrue}{\@jtermceqAlignFalse}}
+\newcommand{\@jtermceqAlignTrue}[4]{& \vdash #3\jdeq #4:#2}
+\newcommand{\@jtermceqAlignFalse}[3]{\vdash #2\jdeq #3:#1}
+
+\newcommand{\jtermteq}{\@ifnextchar*{\@jtermteqAlignTrue}{\@jtermteqAlignFalse}}
+\newcommand{\@jtermteqAlignTrue}[5]{#2 & \vdash #4\jdeq #5:#3}
+\newcommand{\@jtermteqAlignFalse}[4]{#1\vdash #3\jdeq #4:#2}
+\makeatother
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% Often we shall need to display lists of inference rules. This environment
+%%%% adjusts the array environment so that there is enough vertical space
+%%%% between two inference rules
+%%%%
+%%%% bug: there's two much space above the array.
+
+\newenvironment{infarray}[1]{\begingroup\renewcommand*{\arraystretch}{3}
+\begin{equation*}
+\begin{array}{#1}}{
+\end{array}
+\end{equation*}
+\endgroup}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% CONTEXT EXTENSION 
+%%%%
+%%%% explicit context extension notation which we will use only rarely
+
+\newcommand{\tfext}{\typefont{ext}}
+
+%%%% The context extension command.
+%%%%
+%%%% To get a feeling of how the command works, here are a few examples.
+%%%% \ctxext{A}{B} will print A.B
+%%%% \ctxext{{A}{B}}{C} will print (A.B).C
+%%%% \ctxext{{{A}{B}}{C}}{{D}{E}} will print ((A.B).C).(D.E)
+
+\makeatletter
+\newcommand{\ctxext}[2]{\@ctxext@ctx #1.\@ctxext@type #2}
+\newcommand{\@ctxext}{\@ifnextchar\bgroup{\@@ctxext}{}}
+\newcommand{\@ctxext@ctx}{\@ifnextchar\ctxext{\@ctxext@nested}{\@ifnextchar\ctxwk{\@ctxwk@nested}{\@ctxext}}}
+\newcommand{\@ctxext@type}{\@ifnextchar\ctxext{\@ctxext@nested}{\@ifnextchar\subst{\@subst@nested}{\@ctxext}}}
+\newcommand{\@@ctxext}[1]{\@ifnextchar\bgroup{\@ctxext@parens{#1}}{#1}}
+\newcommand{\@ctxext@parens}[2]{(\ctxext{#1}{#2})}
+\newcommand{\@ctxext@nested}[3]{\@ctxext@parens{#2}{#3}}
+\makeatother
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% SUBSTITUTION
+
+\newcommand{\tfsubst}{\typefont{subst}}
+
+%%%% The substitution command will act the following way
+%%%%
+%%%% \subst{x}{P} will print P[x]
+%%%% \subst{x}{{f}{Q}} will print Q[f][x]
+%%%% \subst{{x}{f}}{{x}{Q}} will print Q[x][f[x]]
+
+\makeatletter
+\newcommand{\subst}[2]{\@subst@type #2[\@subst@term #1]}
+\newcommand{\@subst}{\@ifnextchar\bgroup{\@@subst}{}}
+\newcommand{\@@subst}[1]{\@ifnextchar\bgroup{\subst{#1}}{#1}}
+\newcommand{\@subst@term}{\@subst}
+\newcommand{\@subst@type}{\@ifnextchar\ctxext{\@ctxext@nested}{\@ifnextchar\ctxwk{\@ctxwk@nested}{\@subst}}}
+\newcommand{\@subst@nested}[3]{\@subst@parens{#2}{#3}}
+\newcommand{\@subst@parens}[2]{(\subst{#1}{#2})}
+\makeatother
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% WEAKENING
+
+\newcommand{\tfwk}{\typefont{wk}}
+
+%%%% The weakening command is very much like the substitution command.
+
+\makeatletter
+\newcommand{\ctxwk}[2]{\langle\@ctxwk@act #1\rangle\@ctxwk@pass #2}
+\newcommand{\@ctxwk}{\@ifnextchar\bgroup{\@@ctxwk}{}}
+\newcommand{\@@ctxwk}[1]{\@ifnextchar\bgroup{\ctxwk{#1}}{#1}}
+\newcommand{\@ctxwk@act}{\@ctxwk}
+\newcommand{\@ctxwk@pass}{\@ifnextchar\ctxext{\@ctxext@nested}{\@ifnextchar\subst{\@subst@nested}{\@ctxwk}}}
+\newcommand{\@ctxwk@parens}[2]{(\ctxwk{#1}{#2})}
+\newcommand{\@ctxwk@nested}[3]{\@ctxwk@parens{#2}{#3}}
+\makeatother
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% When investigation pointed structures we use the \pt macro.
+
+\makeatletter
+\newcommand{\pt}[1][]{*_{
+  \@ifnextchar\undergraph{\@undergraph@nested}
+    {\@ifnextchar\underovergraph{\@underovergraph@nested}{}}#1}}
+\makeatother
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% OPERATIONS ON GRAPHS
+%%%%
+%%%% First of all, each graph has a type of vertices and a type of edges. The
+%%%% type of vertices of a graph $\Gamma$ is denoted by $\pts{\Gamma}$;
+%%%% and likewise for the type of edges.
+
+\makeatletter
+\newcommand{\pts}[1]{{\@graphop@nested{#1}}_{0}}
+\newcommand{\edg}[1]{{\@graphop@nested{#1}}_{1}}
+\newcommand{\@graphop@nested}[1]
+  {\@ifnextchar\ctxext{\@ctxext@nested}
+      {\@ifnextchar\undergraph{\@undergraph@nested}
+         {\@ifnextchar\underovergraph{\@underovergraph@nested}{}}}
+    #1}
+\makeatother
+
+%%%% The following operations of \undergraph and \underovergraph are used to
+%%%% define the free category and the free groupoid of a graph, respectively
+
+\makeatletter
+\newcommand{\@undergraphtest}[2]{\@ifnextchar({#1}{#2}}
+\newcommand{\undergraph}[2]{\@undergraphtest{\@undergraph@parens{#1}{#2}}{\@undergraph{#1}{#2}}}
+\newcommand{\@undergraph}[2]{{#2/#1}}
+\newcommand{\@undergraph@nested}[3]{\@undergraph@parens{#2}{#3}}
+\newcommand{\@undergraph@parens}[2]{(\@undergraph{#1}{#2})}
+\makeatother
+
+\makeatletter
+\newcommand{\underovergraph}[2]{\@underovergraphtest{\@underovergraph@parens{#1}{#2}}{\@underovergraph{#1}{#2}}}
+\newcommand{\@underovergraph}[2]{{#2}\,{\parallel}\,{#1}}
+\newcommand{\@underovergraphtest}{\@undergraphtest}
+\newcommand{\@underovergraph@parens}[2]{(\@underovergraph{#1}{#2})}
+\newcommand{\@underovergraph@nested}[3]{\@underovergraph@parens{#2}{#3}}
+\makeatother
+
+\newcommand{\graphid}[1]{\mathrm{id}_{#1}}
+\newcommand{\freecat}[1]{\mathcal{C}(#1)}
+\newcommand{\freegrpd}[1]{\mathcal{G}(#1)}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%% Some tikz macros to typeset diagrams uniformly.
+
+\tikzset{patharrow/.style={double,double equal sign distance,-,font=\scriptsize}}
+\tikzset{description/.style={fill=white,inner sep=2pt}}
+
+%% Used for extra wide diagrams, e.g. when the label is too large otherwise.
+\tikzset{commutative diagrams/column sep/Huge/.initial=18ex}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% New theorem environment for conjectures.
+
+\defthm{conj}{Conjecture}{Conjectures}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%%%% The following environment for desiderata should not be there. It is better
+%%%% to use the issue tracker for desiderata.
+
+\newenvironment{desiderata}{\begingroup\color{blue}\textbf{Desiderata.}}
+{\endgroup}