_packages_and_newcommands.tex

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% PACKAGES & ENVIRONMENTS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% \usepackage[margin=0.75in]{geometry}   % Put this in each specific document to choose margin

\usepackage{amssymb,amsmath,amsthm}
\usepackage{makeidx}
%\usepackage{MnSymbol}
\usepackage{latexsym}
\usepackage{enumerate}
\usepackage{hyperref}		%% For URLs
% \usepackage{calrfsf}		%% For scroll font \mathscr{}
%\usepackage{todonotes}		%% For \todo{} margin notes
\usepackage{tikz}

\theoremstyle{definition}  %% Use non-italic text for body of Theorem


\newtheorem{Definition}{Definition}
\newtheorem{Corollary}{Theorem}
\newtheorem{Theorem}{Theorem}
\newtheorem*{Proof}{Proof}
\newtheorem{Lemma}{Lemma}
\newtheorem{Example}{Example}


% \usepackage{delarray}

%\usepackage[all,cmtip,2cell]{xy}
%\UseAllTwocells
%\input xy
%\xyoption{all}
%\xyoption{v2}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% STANDARD NEW COMMANDS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\upwedge}{\wedge}
\newcommand{\downwedge}{\vee}
\newcommand{\glb}{\wedge}
\newcommand{\lub}{\vee}


\newcommand{\tstile}{\vdash}
\newcommand{\makestrue}{\models}

\newcommand{\andalso}{,\;}		%% Comma with more space, for premises


% \newcommand{\newIdea}[1]{\emph{#1}} %% Emphasis for the first intro of new terminology
\newcommand{\newIdea}[1]{\textbf{#1}} %% Bold text for the first intro of new terminology
\newcommand{\terminology}[1]{\textbf{#1}} %% Bold text for the first intro of new terminology
\newcommand{\pr}[1]{\ensuremath{{#1}^{\prime}}}

\newcommand{\cat}[1]{\ensuremath{\mathcal{#1}}}
\newcommand{\category}[1]{\ensuremath{\mathcal{#1}}}
\newcommand{\Sets}{{\textsc{Sets}}}

\newcommand{\following}{\circ}

\renewcommand{\emptyset}{\varnothing}  %% Use the nice symbol
% \newcommand{\Hom}[1]{\ensuremath{\mbox{\textup{Hom}}_{#1}}}
% \newcommand{\Nat}{\mbox{\textup{Nat}}}
\newcommand{\Id}[1]{\ensuremath{\mbox{\textup{Id}}_{#1}}}
\newcommand{\monoidunit}[1]{\ensuremath{\mathbf{1}_{#1}}}
% \newcommand{\nt}{natural transformation}
% \newcommand{\NT}{Natural transformation}

%% Numbers:
\newcommand{\CC}{\ensuremath{\mathbb{C}}} %% Complex numbers
\newcommand{\RR}{\ensuremath{\mathbb{R}}} %% Real numbers
\newcommand{\QQ}{\ensuremath{\mathbb{Q}}} %% Rational numbers
\newcommand{\NN}{\ensuremath{\mathbb{N}}} %% Natural numbers
\newcommand{\ZZ}{\ensuremath{\mathbb{Z}}} %% Integers
\newcommand{\BB}{\ensuremath{\mathbb{B}}} %% Booleans

\newcommand{\HomSet}[2]{\ensuremath{\{{#1} \to {#2}\}}}

%% Logical notation:
\newcommand{\AND}{\,\&\,}
\newcommand{\OR}{\vee}
\newcommand{\NOT}{\neg}
\newcommand{\IMPLIES}{\Rightarrow}
\newcommand{\ABSURDITY}{\bot}
\newcommand{\intersect}{\cap}
\newcommand{\union}{\cup}
\newcommand{\iso}{\cong}

\newcommand{\set}[1]{\ensuremath{
\{ #1 \}
}}  %% Curly brackets for sets
\newcommand{\setSuchThat}[2]{\ensuremath{
\{ #1 \,|\, #2 \}
}}  %% Curly brackets with 'pipe' divider for sets with conditions


\newcommand{\List}[1]{\texttt{List(}#1\texttt{)}}
%\newcommand{\List}[1]{\texttt{[}#1\texttt{]}}
\newcommand{\Nil}{\texttt{[\;]}}
\newcommand{\ListOf}[2]{
\texttt{[}
#1
\texttt{||}
#2
\texttt{]}
}

\newcommand{\BTree}[1]{\texttt{BTree(}#1\texttt{)}}



% %% Some type-theory notation
\newcommand{\mono}[1]{\texttt{#1}}
% \newcommand{\term}[1]{\texttt{\ensuremath{#1}}}
\newcommand{\term}[1]{\texttt{#1}}
% \newcommand{\type}[1]{\texttt{\ensuremath{#1}}}
\newcommand{\type}[1]{\texttt{#1}}

\newcommand{\DefinedAs}{:\equiv}

%\newcommand{\TermOfType}[2]{\term{#1}:\type{#2}}
%\newcommand{\ToT}[2]{\term{#1}:\type{#2}}		%% ToT = TermOfType

%\newcommand{\IdMathrm}{\mathrm{Id}}
\newcommand{\Identity}[2]{#1 \! = \! #2}
\newcommand{\IdType}[3]{#1 \! =_{#3}\! #2}
\newcommand{\ii}{\iota}
\newcommand{\pind}[1]{\texttt{pind}_{#1}}

\newcommand{\s}{\term{s}}					% successor in \NN
\newcommand{\zN}{\term{0}_{\type{\NN}}}		% zero of \NN
\newcommand{\N}[1]{\term{#1}_{\type{\NN}}}  % numerals of \NN

\newcommand{\fin}[2]{\term{#1}_{\term{#2}}}


\newcommand{\JEqTerms}[3]{\ensuremath{\term{#1} \!\equiv\! \term{#2}:\type{#3} }}
\newcommand{\JEqTypes}[2]{\ensuremath{\type{#1} \!\equiv\! \type{#2}}}

\newcommand{\ctx}{\,\textrm{ctx}}

\newcommand{\PROD}[2]{\ensuremath{\prod_{#1} #2}}
\newcommand{\SUM}[2]{\ensuremath{\sum_{#1} #2}}
\newcommand{\AltPROD}[2]{\ensuremath{\langle{#1}\rangle \to #2}}
\newcommand{\AltSUM}[2]{\ensuremath{\langle{#1}\rangle \x #2}}
\newcommand{\TYPE}{\type{TYPE}}

%\newcommand{\PType}[2]{\type{#1}\,\ensuremath{\times}\,\type{#2}}
%\newcommand{\CType}[2]{\type{#1}\,\ensuremath{+}\,\type{#2}}
%\newcommand{\FType}[2]{\type{#1}\,\ensuremath{\to}\,\type{#2}}

\newcommand{\x}{\times}
\newcommand{\+}{+}
\newcommand{\z}{\type{0}}

\newcommand{\rec}[1]{\ensuremath{\texttt{rec}_{#1}}}
\newcommand{\ind}[1]{\ensuremath{\texttt{ind}_{#1}}}


\newcommand{\inl}{\texttt{inl}}
\newcommand{\inr}{\texttt{inr}}

\newcommand{\refl}[1]{\ensuremath{\textrm{refl}_{#1}}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% DIAGRAM TEMPLATES
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

% A shortcut to make commutative squares: single-spaced
\newcommand{\SmallCommutativeSquare}[8]{
% Usage: \SmallCommutativeSquare{Top Left Object}{Top Right Object}{Bottom Left Object}{Bottom Right Object}{Top Arrow}{Left Arrow}{Right Arrow}{Bottom Arrow}
\xymatrix{
{#1} \ar[r]^{{#5}} \ar[d]_{{#6}} & {#2}\ar[d]^{{#7}} \\
{#3} \ar[r]_{{#8}}& {#4}
}
}

% A shortcut to make commutative squares: double-spaced
\newcommand{\LargeCommutativeSquare}[8]{
% Usage: \LargeCommutativeSquare{Top Left Object}{Top Right Object}{Bottom Left Object}{Bottom Right Object}{Top Arrow}{Left Arrow}{Right Arrow}{Bottom Arrow}
\xymatrix{
{#1} \ar[rr]^{{#5}} \ar[dd]_{{#6}} && {#2}\ar[dd]^{{#7}} \\
\\
{#3} \ar[rr]_{{#8}}&& {#4}
}
}


% A shortcut to make ``tent diagrams'' for natural transformations
\newcommand{\NatTransDiag}[9]{
% Usage: \NatTransDiag{Object 1}{Object 2}{Arrow}{Functor 1}{Functor 2}{Category 1}{Category 2}{NT Name}{Curvature of arrows}
\xymatrix{
&{#1} \ar[rrr]^{{#3}} \ar@/^{#9}/[ddddr]^{{#5}} \ar@/_{#9}/[dddl]_{{#4}} &&&{#2}\ar@/^{#9}/[ddddr]^{{#5}}\ar@/_{#9}/[dddl]_{{#4}}  &&& {#6} \ar@{-->}[dddd]^{{#4},\, {#5}}\\
\\
\\
{#4}({#1})\ar[drr]^{{#8}_{#1}} \ar@{->}[rrr]^{{#4}({#3})}	&&&	{#4}({#2})\ar[drr]^{{#8}_{#2}}  \\
&&	{#5}({#1})\ar[rrr]_{{#5}({#3})} 	&&&	{#5}({#2}) && {#7}
}}



% A shortcut to make ``constraint diagrams'' for natural transformations
\newcommand{\NTConstraint}[6]{
% Usage: \NTConstraint{NT Name}{Functor 1}{Functor 2}{Object 1}{Object 2}{Arrow}
\LargeCommutativeSquare
{{#2}({#4})}	% Top Left Object
{{#2}({#5})}	% Top Right Object
{{#3}({#4})}	% Bottom Left Object
{{#3}({#5})}	% Bottom Right Object
{{#2}({#6})}	% Top Arrow
{{#1}_{#4}}		% Left Arrow
{{#1}_{#5}}		% Right Arrow
{{#3}({#6})}	% Bottom Arrow
}