macros.tex

% Magenta keeps notes clear of the change-markup palette.
\newcommand*{\note}[1]{\textcolor{magenta}{\textbf{note:} #1}}
\newcommand*{\todo}[1]{\textcolor{magenta}{\textbf{todo:} #1}}
\newcommand*{\GPS}{Galois slicing\xspace} % in case we change our mind about how to refer to this

\newcommand*{\enummargin}{8mm}

\newcommand{\AGDA}{\textit{(Formalised in Agda)}}

\makeatletter
\@ifclasswith{acmart}{anonymous}{
  \newcommand{\anonymise}[2]{#2}
}{
  \newcommand{\anonymise}[2]{#1}
}
\makeatother

\newcommand*{\etal}{{\it et al.}\xspace}

\newcommand{\bob}[1]{\textcolor{purple}{\textbf{BOB:} #1}}
\newcommand{\roly}[1]{\textcolor{red}{\textbf{ROLY:} #1}}

% Attribute inline edits with the optional id, e.g. \added[id=roly]{...}.
\definechangesauthor[name=Bob, color=purple]{bob}
\definechangesauthor[name=Roly, color=red]{roly}
% No strikethrough: ulem's \sout is neither line-breakable nor metric-neutral.
\colorlet{deletedgray}{gray!70}
\setdeletedmarkup{\textcolor{deletedgray}{#1}}
% Capitalised variants add a margin changebar; use the lowercase forms inside
% figures or math, where changebar spans misbehave. \leavevmode commits a run-in
% heading in the default colour before the markup colour starts.
\newcommand{\Added}[1]{\leavevmode\protect\cbstart\added{#1}\protect\cbend\xspace}
\newcommand{\Deleted}[1]{\leavevmode\protect\cbstart\deleted{#1}\protect\cbend\xspace}
% The control space after #1 separates the new text from the deleted text shown
% after it (a plain space at the start of #2 is eaten by the changes package).
\newcommand{\Replaced}[2]{\leavevmode\protect\cbstart\replaced{#1\ }{#2}\protect\cbend\xspace}
% Deleted display material (diagrams, figures) that cannot live inside \Deleted:
% greyed out with a changebar in draft mode, discarded in final mode.
\newenvironment{DeletedBlock}{\par\cbstart\color{deletedgray}}{\cbend\par}
% Added display material (tables, figures) that cannot live inside \Added: alignment
% and rule material is fragile inside the changes package's argument.
\newenvironment{AddedBlock}{\par\cbstart\color{blue}}{\cbend\par}
% Final mode bypasses the changes package: its \IfIsEmpty test expands the
% replacement text, and any macro with #1 in its body then causes a runaway \iffalse.
\ifdefined\finalmode
  \renewcommand{\Added}[1]{#1}%
  \renewcommand{\Deleted}[1]{}%
  \renewcommand{\Replaced}[2]{#1}%
  \renewcommand{\added}[2][]{#2}%
  \renewcommand{\deleted}[2][]{}%
  \renewcommand{\replaced}[3][]{#2}%
  \renewenvironment{DeletedBlock}{\setbox0\vbox\bgroup}{\egroup}%
  \renewenvironment{AddedBlock}{\par}{\par}%
\fi

\newenvironment{salign*}
   {\par\nobreak\small\noindent\csname align*\endcsname}
   {\csname endalign*\endcsname}

\newcommand*{\defref}[1]{Definition~\ref{def:#1}}
\newcommand*{\corref}[1]{Corollary~\ref{cor:#1}}
\newcommand*{\conref}[1]{Conjecture~\ref{con:#1}}
\newcommand*{\exref}[1]{Example~\ref{ex:#1}}
\newcommand*{\figref}[1]{Figure~\ref{fig:#1}}
\newcommand*{\figrefTwo}[2]{Figures~\ref{fig:#1} and \ref{fig:#2}}
\newcommand*{\propref}[1]{Proposition~\ref{prop:#1}}
\newcommand*{\lemref}[1]{Lemma~\ref{lem:#1}}
\newcommand*{\remref}[1]{Remark~\ref{rem:#1}}
\newcommand*{\thmref}[1]{Theorem~\ref{thm:#1}}
\newcommand*{\secref}[1]{\S\ref{sec:#1}}
\newcommand*{\eqnref}[1]{Equation~\ref{eqn:#1}}
% Possessive citation: author's (year), rather than the ill-formed author (year)'s.
\newcommand*{\posscite}[1]{\citeauthor{#1}'s~\citeyearpar{#1}}

% Syntax
\newcommand*{\syn}[1]{\mathbf{#1}} % keywords
\newcommand*{\synVar}[1]{\mathrm{#1}} % variables

\newcommand*{\PrimTy}{\mathsf{PrimTy}}
\newcommand*{\PrimOp}{\mathsf{Op}}
\newcommand*{\Lift}{L} % {\mathsf{Lift}} % {\mathcal{L}}
\newcommand*{\List}{\mathrm{List}}
\newcommand*{\fold}{\mathsf{fold}}
\newcommand*{\nil}{\mathsf{nil}}
\newcommand*{\cons}{\mathsf{cons}}

% \newcommand*{\kType}{\mathsf{type}}

\newcommand*{\tmApp}[2]{#1\;#2}
\newcommand*{\tmBind}[2]{{#1}\gg={#2}}
\newcommand*{\tmCase}[5]{\syn{case}\;#1\;\{#2.#3; #4.#5\}}
\newcommand*{\tmCons}[2]{\syn{cons}\;#1\;#2}
\newcommand*{\tmFold}[2]{\syn{fold}\;#1\;#2}
\newcommand*{\tmFoldList}[3]{\syn{fold}\;#1\;#2\;#3}
\newcommand*{\tmFst}[1]{\syn{fst}\;#1}
\newcommand*{\tmFun}[2]{\lambda#1.#2}
\newcommand*{\tmInl}[1]{\syn{inl}\;#1}
\newcommand*{\tmInr}[1]{\syn{inr}\;#1}
\newcommand*{\tmNil}{\syn{nil}}
\newcommand*{\tmPair}[2]{(#1,#2)}
\newcommand*{\tmReturn}[1]{\syn{return}\;#1}
\newcommand*{\tmRoll}[1]{\syn{roll}\;#1}
\newcommand*{\tmSnd}[1]{\syn{snd}\;#1}
\newcommand*{\tmUnit}{()}

\newcommand*{\tyFun}{\to}
\newcommand*{\tyLift}{\syn{lift}}
\newcommand*{\tyList}{\syn{list}}
\newcommand*{\tyProd}{\times}
\newcommand*{\tySum}{+}
\newcommand*{\tyUnit}{\syn{1}}
\newcommand*{\tyZero}{\syn{0}}
\newcommand*{\Rel}{\mathsf{Rel}}
\newcommand*{\Op}{\mathsf{Op}}

\newcommand*{\emptyCxt}{\cdot}
\newcommand*{\Pol}{\mathsf{Pol}}
\newcommand*{\subst}[3]{#1[#2/#3]}

\newcommand{\naturalto}{%
  \mathrel{\vbox{\offinterlineskip
    \mathsurround=0pt
    \ialign{\hfil##\hfil\cr
      \normalfont\scalebox{1.2}{.}\cr
%      \noalign{\kern-.05ex}
      $\rightarrow$\cr}
  }}%
}

\newcommand*{\adj}{\dashv}
\newcommand*{\transpose}[1]{#1^{\top}}
\newcommand*{\biinj}{\mathsf{i}}
\newcommand*{\biprod}{\oplus}
\newcommand*{\biproj}{\mathsf{p}}
\newcommand*{\cat}[1]{\mathcal{#1}}
\newcommand*{\codiag}{\nabla}
\newcommand*{\comp}{\circ}
\newcommand*{\const}{\mathsf{const}}
\newcommand*{\coprodM}[2]{[#1, #2]}
\newcommand*{\cotangents}{\tangents^*}
\newcommand*{\diag}{\Delta}
\newcommand*{\directImage}[2]{#1\langle#2\rangle}
\newcommand*{\eval}{\varepsilon}
\newcommand*{\faml}[1]{\overline{#1}} % \fam already defined
\newcommand*{\fin}{\mathsf{fin}}
\newcommand*{\cata}{\phi}
\newcommand*{\id}{\mathsf{id}}
\newcommand*{\idx}[1]{\widehat{#1}}
\newcommand*{\inj}{\mathsf{inj}}
\newcommand*{\inMap}{\mathsf{in}}
\newcommand*{\internalHom}[2]{#1 \Rightarrow #2}
\newcommand*{\iso}{\cong}
\newcommand*{\join}{\vee}
\newcommand*{\bigjoin}{\bigvee}
\newcommand*{\length}[1]{|#1|}
\newcommand*{\linearto}{\multimap}
\newcommand*{\meet}{\wedge}
\newcommand*{\bigmeet}{\bigwedge}
\newcommand*{\disj}{\mathrel{\#}}
\newcommand*{\scalarmeet}{\odot}
\newcommand*{\Mor}{\mathsf{Mor}}
\newcommand*{\mult}{\cdot}
\newcommand*{\namedcat}[1]{\mathbf{#1}}
\newcommand*{\Ob}{\mathsf{Ob}}
\newcommand*{\op}{\mathsf{op}}
\newcommand*{\pairM}[2]{(#1, #2)}
% \renewcommand*{\prod}{\times} -- probably not a good idea
\newcommand*{\prodFam}[1]{\langle #1\rangle} % \lambda(f) bit overloaded
\newcommand*{\prodM}[2]{\langle #1, #2\rangle}
\newcommand*{\proj}{\pi}
\newcommand*{\pullf}[1]{#1^{*}}
\newcommand*{\pushf}[1]{{#1_{*}}}
\newcommand*{\reindex}[2]{#1[#2]}
\newcommand*{\residual}{\Rightarrow}
\newcommand*{\sem}[1]{\llbracket #1 \rrbracket}
\newcommand*{\cbn}[1]{\langle\kern-2pt\langle #1 \rangle\kern-2pt\rangle}
\newcommand*{\sqgeq}{\sqsupseteq}
\newcommand*{\sqleq}{\sqsubseteq}
\newcommand*{\tangents}{\mathrm{T}}
\newcommand*{\tensor}{\otimes}
\newcommand*{\zero}{0}

\newcommand*{\One}{\mathbbm{1}}
\newcommand*{\Two}{\mathbbm{2}}

\newcommand*{\Hom}[3]{{#1}(#2,#3)}
\newcommand*{\Nat}{\mathbbm{N}}
\newcommand*{\RR}{\mathbbm{R}}
\newcommand*{\Yoneda}{\mathcal{Y}}
\newcommand*{\Zero}{\mathbb{0}}

% Specific categories and functors
\newcommand*{\Ab}{\namedcat{Ab}}
\newcommand*{\Cat}{\namedcat{Cat}}
\newcommand*{\CMon}{\namedcat{CMon}}
\newcommand*{\Diff}{\namedcat{Diff}}
\newcommand*{\Fam}{\namedcat{Fam}}
\newcommand*{\FinVect}{\namedcat{FDVect}}
\newcommand*{\FinRel}{\namedcat{FinRel}}
\newcommand*{\Vect}{\namedcat{Vect}}
\newcommand*{\Func}[2]{[#1,#2]}
\newcommand*{\Grothendieck}[1]{\int_{#1}}
\newcommand*{\HoEmbed}{H}
\newcommand*{\Mat}{\namedcat{Mat}}
\newcommand*{\SemiMod}{\namedcat{SemiMod}}
\newcommand*{\SDSemiMod}{\namedcat{SDSemiMod}}
\newcommand*{\conj}[1]{#1^{\dagger}}
\newcommand*{\LatGal}{\namedcat{LatGal}}
\newcommand*{\CLatGal}{\namedcat{CLatGal}}
\newcommand*{\demorgan}[1]{{#1}^{\circ}}
\newcommand*{\HeytConj}{\namedcat{HeytConj}}
\newcommand*{\muPoly}{\mu\namedcat{Poly}}
\newcommand*{\Pred}{\mathrm{Pred}}
\newcommand*{\PSh}{\namedcat{PSh}}
\newcommand*{\PosGal}{\namedcat{PosGal}}
\newcommand*{\Poset}{\namedcat{Poset}}
\newcommand*{\SemiLat}{\namedcat{SemiLat}}
\newcommand*{\Sem}{\namedcat{Sem}}
\newcommand*{\Set}{\namedcat{Set}}
\newcommand*{\Setoid}{\namedcat{Setoid}}
\newcommand*{\Man}{\namedcat{Man}}
\newcommand*{\CM}{\namedcat{CM}} % Bounded meet posets and conditionally multiplicative functions
\newcommand*{\MeetSLat}{\namedcat{MeetSLat}}
\newcommand*{\JoinSLat}{\namedcat{JoinSLat}}
\newcommand*{\Lposet}{\namedcat{Stable}}
\newcommand*{\GLR}{\namedcat{GLR}} % Grothendieck Logical Relations
\newcommand*{\Disc}{\mathrm{Disc}}
\newcommand*{\LatConj}{\namedcat{LatConj}}
\newcommand*{\QQ}{\mathbbm{Q}}
\newcommand*{\Intv}{\mathsf{Intv}}
\newcommand*{\IntvL}{\Intv_{\bot}}
\newcommand*{\add}{\mathsf{add}}
\newcommand*{\addT}{\add^{\mathsf{T}}}

\newcommand{\downset}[1]{\mathop{\downarrow}(#1)}

\theoremstyle{acmdefinition}
\newtheorem{remark}{Remark}