~ohad-kammar/ohads-thesis/trunk

\usepackage{okcategory}
\usepackage{oksemantics}
\usepackage{xcolor}
\usepackage{colortbl}
\usepackage{xargs}

\let\Cate\Cat
\let\Cat\undefined

\newnotation{\ValCat}{{\Cate{V}}}{Value category}
\newnotation{\CompCat}{{\Cate{C}}}{Stack category}
\newnotation{\F}{{F}}{Left adjoint}
\newnotation{\Fv}{{\hat F}}{Left adjoint}
\newnotation\RightAdjoint{G}{Right adjoint metavariable}
\newnotation{\U}{{U}}{Right adjoint in a CBPV adjunction}
\newnotation{\Uv}{{\hat U}}{Right adjoint in a CBPV adjunction}
\newnotation{\AdjunctionBijection}{\phi}{The natural bijection
$\AdjunctionBijection \of \homset[\CompCat]{\F\mV}\mC \isomorphic \homset[\ValCat]{\mV}{\RightAdjoint\mC}$}

\newnotation{\mX}{X}{Generic set.}
\newnotation{\mY}{Y}{Generic set.}
\newcommand\mXv\mY
\newnotation{\mZ}{Z}{Generic set.}
\newnotation{\mx}{x}{Generic element of the set $\mX$.}
\newnotation{\my}{y}{Generic element of the set $\mY$.}
\newnotation{\mz}{z}{Generic element of the set $\mZ$.}

\newnotationargs{\inObj}{1}{\in\Obj{#1}}{$A$ is an object in $\Cate
C$}{A \inObj {\Cate C}}
\WithSuffix\newcommand\inObj*[1]{\inObj{\smash{#1}}}

\newnotationgroup{arity}{the effect operation $\mop$ is assigned arity
$\Ar$ and parameter $\Pa$}{\mop \of \arity\Ar\Pa}
\newnotation\mar{a}{element of an arity}
\newnotation\mpa{p}{element of a parameter type}
\newnotationmember{arity}{\Pa}{P}
\newnotationmember{arity}{\Ar}{A}
\newnotationargsmember{arity}{\arity}{2}{{#1}\anglebrackets{#2}}

\newnotation\StorVal{\mathbb{V}}{Set modeling storable values}
\newnotation\Char{\mathbb{Char}}{Set modeling terminal characters.}
\newnotation\Exc{\mathbb{E}}{Set modeling exceptions.}
\newnotation\Loc{\mathbb{L}}{Set modeling possible memory locations.}
\newnotation\mloc{\ell}{Metavariable for $\Loc$}
\newnotation\mchar{c}{Metavariable for $\Char$}
\newnotation\mterm{t}{Metavariable for a term}
\newnotation\mtermset{\tau}{Metavariable for a set of terms (in the
semantics of non-determinism).}
\newnotation\mtermv{s}{Metavariable for a term}
\newnotation\mtermu{u}{Metavariable for a term}
\newnotation\String{\mathbb{Str}}{$\Char^*$}
\newnotation\mstring{s}{Metavariable for $\String$}

\newnotation\Monad{T}{Monad metavariabe}
\newnotationgroup{monoid}{A monoid.}
                         {\Monoid= \triple{\carrier\Monoid}\mdot\munit}
\newnotationmember{monoid}\Monoid{M}
\newnotationmember{monoid}\mdot{\cdot}
\newnotationmember{monoid}\munit{1}
\newnotation\mmonoid{m}{Monoid metavariable}
\newnotation\Monadv{T'}{Monad metavariabe}
\newnotation\vMonad{S}{Monad metavariabe}
\newnotationargs\AlgebraCat{2}{{#1}^{#2}}{Eilenberg-Moore category for a
monad $\Monad$ over $\ValCat$}{\AlgebraCat\ValCat\Monad}
\newnotationargsopt\Algebra{1}{B}{\underline{#1}}{Algebra for monad.}{\Algebra}{}
\newnotation\Algebrav{\mCv}{Algebra for monad.}
\newnotationx\algebra{2}{1={\Algebra},2={\placeholder}}{{#1}\scottbrackets{#2}}{algebra map for an algebra}{\algebra}
\newnotation\algebrahom{h}{algebra homomorphism for a monad}
\newnotation\malg{\mc}{Metavariable for an element of an algebra for a
        monad.}

\newnotationgroup{val obj}{Generic objects in the value category
$\ValCat$}{\mV, \mVv, \mVw, \mVu, \mVx, \mVy, \mVz, \mG}
\newnotationmember{val obj}\mV{A}
\newnotationmember{val obj}\mVv{B}
\newnotationmember{val obj}\mVw{C}
\newnotationmember{val obj}\mVu{D}
\newnotationmember{val obj}\mVx{X}
\newnotationmember{val obj}\mVy{Y}
\newnotationmember{val obj}\mVz{Z}
\newnotationmember{val obj}\mG{\Gamma}

\newnotationgroup{vals}{Metavariables for elements of value
objects.}{\mv, \mvv, \mvw, \mvx, \mvy, \mvz, \mg}
\newnotationmember{val obj}\mv {a}
\newnotationmember{val obj}\mvv{b}
\newnotationmember{val obj}\mvw{c}
\newnotationmember{val obj}\mvx{x}
\newnotationmember{val obj}\mvy{y}
\newnotationmember{val obj}\mvz{z}
\newnotationmember{val obj}\mg{\gamma}
\newnotationmember{val obj}\mgv{\delta}

\newnotation\mC{\underline{B}}{Generic object in the stack category
$\CompCat$}
\newnotation\mCv{\underline{C}}{Generic object in the stack category
$\CompCat$}
\newnotation\mc{b}{Metavariable for an element of the computation type
$\mC$.}

\makeatletter
\newnotation\eval{\mathrm{eval}}{evaluation map for an exponential}
\newcommand\oh@dcomma[2]{{#1},{#2}}
\newnotationargsopt{\strength}{1}{nosubscript}{{\ifthenelse{\equal{#1}{nosubscript}}{\mathrm{str}}{\mathrm{str}_{\oh@dcomma#1}}}}
{The monadic strength}{\strength\mG\mV \of \mG\times\Monad\mV \to \Monad(\mG\times\mV)}
\newnotationargsopt{\costrength}{1}{nosubscript}{{\ifthenelse{\equal{#1}{nosubscript}}{\mathrm{costr}}{\mathrm{costr}_{\oh@dcomma#1}}}}
{The costrength, namely $\swap\compose\strength\compose\swap$.}{\costrength\mG\mV\of (\Monad\mV)\times\mG \to \Monad(\mV\times\mG)}
\newnotationargs\ilam{2}{\lam{#1}{#2}}{The map uniquely determined from
$f \of \mVw\times\mV \to \mVv$ by the universal property of the
exponent ${\mVv}^{\mV}$.}{\ilam\mV f}

\newnotationargs{\lifting}{1}{{#1}^{\dagger}}{}{}
\newnotationargs{\powerlifting}{2}{{#2}^{\ddagger{#1}}}{}{}

\newnotation\e{\epsilon}{Effect set}
\newnotationx\opsem   {3}{2={}, 1={\e}}{\mathcal{O}^{#2}_{#1}\scottbrackets{#3}}{Algebraic
operation assigned to $\mop$ at level $\e$}{\opsem\mop}
\newnotationargsopt\opsemv{2}{\e}{\mathcal{O}'_{#1}\scottbrackets{#2}}{Variant of an algebraic
operation assigned to $\mop$ at level $\e$}{\opsemv\mop}
\newnotationargsopt\genopsem{2}{\e}{\mathcal{G}_{#1}\scottbrackets{#2}}{Generic
effect assigned to $\mop$ at level $\e$}{\genopsem\mop}
\newcommand\vgenopsem[2][\e]{\hat\mathcal{G}_{#1}\scottbrackets{#2}}

\newnotationgroup{ops}{Effect operations}{\lookupop, \updateop,
\inputop, \outputop, \raiseop}
\newnotationmember{ops}\lookupop{\mathrm{lookup}}
\newnotationmember{ops}\updateop{\mathrm{update}}
\newnotationmember{ops}\inputop {\mathrm{input}}
\newnotationmember{ops}\outputop{\mathrm{output}}
\newnotationmember{ops}\raiseop {\mathrm{raise}}
\newnotationmember{ops}\tact    {\mathrm{act}}
\newnotationmember{ops}\throwop {\mathrm{throw}}
\newnotationmember{ops}\divergeop{\mathrm{diverge}}
\newnotationmember{ops}\chooseop{\mathrm{choose}}
\newnotation\orop{\vee}{Infix non-deterministic choice operation.}
\newnotation\Orop{\bigvee}{Prefix non-deterministic choice operation.}

\newnotationgroup{gens}{Generic effects}{\derefop, \setop}
\newnotationmember{gens}\derefop{\mathrm{deref!}}
\newnotationmember{gens}\setop{\mathrm{set!}}
\newnotationmember{gens}\tossop{\mathrm{toss}}
\newnotationmember{gens}\getop{\mathrm{get}}
\newnotationmember{gens}\putop{\mathrm{put}}
\newnotationargs\generic{1}{\mgen_{#1}}{Generic effect corresponding
to $\mop$.}{\generic\mop}
\newnotationargs\operation{2}{\mop^{#1}_{#2}}{Algebraic operation corresponding
to $\mgen$.}{\operation\mop{}}
\newnotationargs\lawoperation{1}{\mop^{#1}}{Algebraic operation
in a Lawvere theory corresponding
to $\mgen$.}{\lawoperation\mop}


\newnotation\mcomp{k}{Metavariable for an element modeling a computation.}
\newnotation\mparcomp{\kappa}{Metavariable for a parametrised family
of elements modeling computations.}
\newnotationgroup{stor vals}{Metavariables for an element of a
storable value type.}{\mval, \mvalv, \mvalw}
\newnotationmember{stor vals}\mval{v}
\newnotationmember{stor vals}\mvalv{u}
\newnotationmember{stor vals}\mvalw{w}
\newnotation{\mexc}{e}{Metavariable for an exception.}

\newcommand\lam[2]{\lambda{#1}.{#2}}

\usepackage{amsmath}
\usepackage{mathbbol}

\newnotation{\E}{\Cate{E}}{Effect hierarchy}
\newnotationargsopt\Opset{1}{{}}{\Pi_{#1}}{Set of effect operations}{\Opset}
\newnotation\Signature{\Sigma}{Signature}
\newnotationargs\carrier{1}{\left\lvert{#1}\right\rvert}{Carrier of a
signature}{\carrier\Signature}
\newnotation\Presheaf{\mathbb{P}}{Presheaf metavariable}
\newnotation\arities{\mathrm{type}}{Function assigning
(arity,parameter) pairs to effect operations.}

\newcommand\cbpv{\textsc{cbpv}}

\newnotation\mop{\mathrm{op}}{Effect operation metavariable}
\newnotation\mopv{\mop'}{Effect operation
metavariable}
\newnotation\mopw{\mop''}{Effect operation metavariable}
\newnotation\mgen{\mathrm{gen}}{Generic effect metavariabe}
\newnotation\mgenv{\mathrm{gen}'}{Generic effect metavariabe}
\newnotation\mgenw{\mathrm{gen}''}{Generic effect metavariabe}

\newnotationargs\Adjunctions{1}{\mathop{\text{\cbpv{}}\!}_{#1}}{Category of
\cbpv{} adjunctions and monad morphisms}{\wCPOAdjunctions\ValCat}
\newnotationargs\wCPOAdjunctions{1}{\mathop{\wCPO\text{-}\mathrm{Adj}}#1}{Category of
\cbpv{} adjunctions and monad morphisms}{\wCPOAdjunctions\ValCat}

\newnotationargs\self{1}{\mathop{\mathrm{self}}#1}{The construction
equipping $\ValCat$ with a $\CpPPresheaves\ValCat$-enriched category structure}{\self\ValCat}
\newcommand\Presheaves[1]{\Set^{\opposite{#1}}}

\newnotationargs\CpPPresheaves{1}{\Presheaves{#1}_{+}}{Finite-product
preserving presheaves}{\CpPPresheaves\ValCat}

\newnotation\MonadMorphism{m}{Monad morphism metavariabe}

\newcommand\homset[3][{\mathrm{Hom}}]{\mathop{#1}\parent{{#2}, {#3}}}
\WithSuffix\newcommand\homset*[3][{\mathrm{Hom}}]{\mathop{#1}({{#2}, {#3}})}
\newnotationgroup{presheaf input objects}{Metavariables for an input
object to a presheaf}{\mG, \mGv}
\newnotationmember{presheaf input objects}\mGv{\Delta}

\newcommand\GlobalState[1][\parent\StorVal]{\mathrm{GS}#1}
\newcommand\Environment[1][\parent\StorVal]{\mathrm{Env}#1}
\newcommand\Overwrite  [1][\parent\StorVal]{\mathrm{OW}#1}
\newcommand\Writer     [1][\parent\Monoid]{\mathrm{W}#1}
\newcommand\Exceptions [1][\parent\Exc]{\mathrm{Exc}#1}
\newcommand\IO  [1][\parent\Char]{\mathrm{IO}#1}
\newcommand\ND  {\mathrm{ND}}
\newcommand\PlotkinPowerdomain{\Powerset{\mathrm{Plo}}}
\newcommand\Lifting{\bot}
\newcommand\Monoids{\mathrm{Mon}}
\newcommand\CommutativeMonoids{\mathrm{ComMon}}
\newnotationargs{\NonemptyFinitePowerset}{1}{\mathop{\mathcal{P}_{+}^{\aleph_0}}\parent{#1}}{Powerset
of non-empty,
finite subsets $\mY \subset\mX$}{\NonemptyFinitePowerset\mX}
\newnotation{\NonemptyFinitePowersetSymbol}{\mathop{\mathcal{P}_{+}^{\aleph_0}}}{Powerset
of non-empty,
finite subsets $\mY \subset\mX$}
\newnotationargsopt\GlobalStateMonad{1}{\parent{\StorVal}}{\Monad_{\mathrm{GS}#1}}{Global
$\StorVal$-state monad}{\GlobalStateMonad}
\newnotationargsopt\GlobalStateTheory{1}{\parent{\StorVal}}{\mL_{\mathrm{GS}#1}}{Global
$\StorVal$-state theory.}{\GlobalStateTheory}
\newnotationargsopt\GlobalStateSignature{1}{\parent{\StorVal}}{\uaSignature_{\mathrm{GS}#1}}{Global
$\StorVal$-state theory.}{\GlobalStateTheory}
\newnotationargsopt\EnvMonad{1}{\parent{\StorVal}}{\Monad_{\mathrm{Env}#1}}{$\StorVal$-environment
monad}{\EnvMonad}
\newnotationargsopt\EnvTheory{1}{\parent{\StorVal}}{\mL_{\mathrm{Env}#1}}{$\StorVal$-environment
theory.}{\EnvTheory}
\newnotationargsopt\OverwriteMonad{1}{\parent{\StorVal}}{\Monad_{\mathrm{OW}#1}}{$\StorVal$-overwrite
monad}{\OverwriteMonad}
\newnotationargsopt\OverwriteTheory{1}{\parent{\StorVal}}{\mL_{\mathrm{OW}#1}}{$\StorVal$-overwrite
Theory}{\OverwriteTheory}
\newnotationargsopt\IOMonad{1}{\parent{\Char}}{\Monad_{\mathrm{I/O}#1}}{Input/Output
-state monad}{\IOMonad}
\newnotationargsopt\IOTheory{1}{\parent{\Char}}{\mL_{\mathrm{I/O}#1}}{Input/Output theory.}{\IOTheory}
\newnotationargsopt\IMonad{1}{\parent{\Char}}{\Monad_{\mathrm{I}#1}}{Input
-state monad}{\IOMonad}
\newnotationargsopt\ITheory{1}{\parent{\Char}}{\mL_{\mathrm{I}#1}}{Input theory.}{\IOTheory}
\newnotationargsopt\OMonad{1}{\parent{\Char}}{\Monad_{\mathrm{O}#1}}{Output
-state monad}{\IOMonad}
\newnotationargsopt\OTheory{1}{\parent{\Char}}{\mL_{\mathrm{O}#1}}{Output theory.}{\IOTheory}
\newnotation\IdentityMonad{\Monad_{\id}}{Identity monad}
\newnotation\InitialTheory{\mL_{\initial}}{Identity theory}
\newnotation\PlotkinMonad{\Monad_{\PlotkinPowerdomain}}{The Plotkin
powerdomain monad.}
\newnotation\LiftingMonad{\Monad_{\Lifting}}{The lifting monad
$\LiftingMonad\mW = \set{\bot}+\mW$.}
\newnotation\NDTheory{\mL_{\ND}}{The non-determinism theory (i.e.,
semilattices)}
\newnotation\ExcMonad{\Monad_{\Exceptions}}{The exception monad
$\placeholder + \Exc$}
\newnotation\ExcTheory{\mL_{\Exceptions}}{The non-determinism theory
(i.e., semilattices)}
\newnotationargsopt\WriterTheory{1}{\parent{\Monoid}}{\mL_{\mathrm{W}#1}}{Writer theory.}{\WriterTheory}
\newnotationargsopt\WriterMonad{1}{\parent{\Monoid}}{\Monad_{\mathrm{W}#1}}{Writer
monad}{\WriterMonad}
\newnotation\MonoidTheory{\mL_{\Monoids}}{The monoid theory.}
\newnotation\CommutativeMonoidTheory{\mL_{\CommutativeMonoids}}{The commutative monoid theory.}



\newnotationargs\EM{1}{\mathop{\mathrm{EM}}\parent{#1}}{Eilenberg-Moore
resolution}{\EM\Monad}
\newnotationargs\KleisliCat{2}{{#1}_{#2}}{Kleisli category for a monad
$\Monad$ over $\SymMonCat$.}{\KleisliCat\SymMonCat\Monad}
\newnotationargsopt\PresKleisliCat{3}{\regcard}{{#2}_{#3}^{#1}}{The
restriction of the Kleisli category for a monad $\Monad$ over
$\SymMonCat$ to the $\regcard$-presentable objects.}{\KleisliCat\SymMonCat\Monad}
\newnotation\unit{\eta}{Unit for a monad}
\newnotation\counit{\theta}{Counit for an adjunction}
\newnotation\monmult{\mu}{Multiplication for a monad}
\newnotation\updateaction{\delta}{Metavariable for an element of the
overwriting monoid}
\newnotationargs\inj{1}{\injection_{#1}}{Category theoretic
injection}{\inj i}
\newnotationargs\proj{1}{\projection_{#1}}{Category theoretic
projection}{\proj i}
\newnotation\unitval{\star}{The element of a (the?) singleton}
\newnotationargs\prodmorphism2{\pair{#1}{#2}}{The universal morphism into the
product $A \times B$ determined by the two morphisms $f$,$g$ into
$A$,$B$}{\prodmorphism fg}
\newnotationargs\coprodmorphism2{\bracks{{#1},{#2}}}{The universal morphism from the
coproduct $A+ B$ determined by the two morphisms $f$,$g$ from
$A$,$B$}{\coprodmorphism fg}
\newnotation\terminalmorphism{\mathord{!}}{The unique morphism into
the terminal object}
\newnotation\initialmorphism{\mathord{\text{!`}}}{The unique morphism from
the initial object}
\newnotation\twoobj{{\mathbb 2}}{The boolean object $\terminal + \terminal$.}
\newnotationargsopt\prodmorphismseq{2}{{}}{\seq[{#1}]{#2}}{The tupling
universal morphism of an $I$ indexed family of morphisms
$f_i$}{\prodmorphismseq[i \in I]{f_i}}
\newnotationargsopt\coprodmorphismseq{2}{{}}{\bracks{#2}_{{#1}}}{The cotupling
universal morphism of an $I$ indexed family of morphisms
$f_i$}{\prodmorphismseq[i \in I]{f_i}}
\newnotationargs\underlyingMorphism{1}{\carrier{#1}}{The $\ValCat$ morphism
underlying a $\self\ValCat$ morphism $f$}{\underlyingMorphism f}
\newnotationargs\charLiteral{1}{\text{'\texttt{#1}'}}{A character
literal}{\charLiteral c}
\newnotationargs\stringLiteral{1}{\text{"\texttt{#1}"}}{A string literal}{\stringLiteral{hello
world}}
\newnotation\nilChar{\charLiteral{\textbackslash0}}{The null character}

%Domain theory
\newcommand\wcpo{$\omega$-cpo}
\newcommand\wchain{$\omega$-chain}
\newnotation\ebot{\bot}{Bottom element of an \wcpo}

%%% Commutative diagram explanations
\newcommand\ProductsExp{products}
\newcommand\CoproductsExp{coproducts}
\newcommand\TerminalExp{terminality}
\newcommand\ExponentialUniversalExp{exponential universality}
\WithSuffix\newcommand\ExponentialUniversalExp*{exponential\\universality}
\newcommand\DefinitionExp[1]{{$#1$} def.}
\newcommand\BifunctorialityExp[1]{{$#1$} bifunctoriality}
\WithSuffix\newcommand\BifunctorialityExp*[1]{{$#1$} bifunct.}
\newcommand\NaturalityExp[1]{{$#1$} naturality}
\newnotation\NaturalTransformation{\alpha}{A natural transformation meta-variable}
\newcommand\EnrichedNaturalityExp[1]{enriched {$#1$} naturality}
\WithSuffix\newcommand\EnrichedNaturalityExp*[1]{enriched\\{$#1$} naturality}
\WithSuffix\newcommand\NaturalityExp*[1]{{$#1$}\\naturality}
\newcommand\StrengthExp[1]{$\strength$ {#1}}
\newcommand\AssociativityExp{associativity}
\newcommand\UnitExp{unit}
\newcommand\MultiplicationExp{multiplication}
\newcommand\ProjectionsExp{proj.}
\newcommand\AlgebraicOperationExp[1]{alg. op. def.}
\newcommand\AdjunctionExp{adjunction}
\newcommand\IdentityExp{$\id$}
\newcommand\MonadLawExp{monad law}
\newcommand\MonadMorphismExp{monad morphism}
\WithSuffix\newcommand\MonadMorphismExp*{monad\\morphism}
\newcommand\StrongMonadMorphismExp{strong monad morphism}
\newcommand\SymMonFunctorCompositionExp{mon. fun. comp.}
\WithSuffix\newcommand\SymMonFunctorCompositionExp*{mon. fun.\\comp.}
\newcommand\SymMonFunctorIdentityExp{mon. fun. id.}
\WithSuffix\newcommand\SymMonFunctorIdentityExp*{mon. fun.\\id.}
\newcommand\EnrichedCatExp{enriched cat.}
\newcommand\EnrichedFunctorCompositionExp{enriched functor
composition}
\WithSuffix\newcommand\EnrichedFunctorCompositionExp*{enriched\\functor\\composition}
\WithSuffix\newcommand\EnrichedCatExp*{enriched\\cat.}
\newcommand\EnrichedFunctorCompositionAxiomExp{enriched functor
composition axiom}
\WithSuffix\newcommand\EnrichedFunctorCompositionAxiomExp*{enriched functor\\
composition axiom}
\newcommand\AssumptionExp{assumption}
\newcommand\PowerPreservationExp{power preservation}
\newcommand\ConeExp{cone}
\newcommand\InductionHypothesisExp{induction hypothesis}
\WithSuffix\newcommand\PowerPreservationExp*{power\\preservation}
\definecolor{shade}{RGB}{220,220,220}
%We need to keep the old mode: math or text.
\newcommand\DELTA[1]{\ifmmode{\DELT@{\ensuremath{#1}}}\else\DELT@{{#1}}\fi}
\newcommand\DELT@[1]{\setlength{\fboxsep}{0pt}\colorbox{shade}{{#1}}}
\newcommand\sml{\textsc{sml}}
\newcommand\ML{\textsc{ml}}

\newnotation\uaSignature{\sigma}{Metavarialbe for an algebraic
signature (universal algebra notion)}
\newnotation\uaOpset{\pi}{Metavarialbe for the set of operations in an algebraic
signature (universal algebra notion)}
\newnotation\uaArities{\mathrm{ar}}{Metavarialbe for the arity assignment in an algebraic
signature (universal algebra notion)}
\newnotation\uaconst{c}{Metavarialbe for a constant operation symbol (universal algebra notion)}
\newnotationargsopt\TermAlgebra{2}{nothing}{\mathop{\mathrm{Terms_{#2}}\ifthenelse{\equal{#1}{nothing}}{}{\parent{#1}}}}{The
set of terms over $\mX$ generated from the signature $\uaSignature$}
{\TermAlgebra[\mX]\uaSignature}
\newnotationargs\varset1{\mathrm{var}\parent{#1}}{The set of variables of the universal algebraic term $\mterm$.}{\varset\mterm}
\newnotation\uaEq{E}{Set of (universal algebraic) equations.}
\newnotation\uaeq{e}{Metavariable for a (universal algebraic) equations.}
\newnotation\Ax{\mathrm{Ax}}{A (set-theoretic, universal algebraic) presentation.}
\newnotationargs\Theory{1}{\mathrm{Th}_{#1}}{The (finitary) Lawvere (set-theoretic) theory
  generated by the presentation $\Ax$.}{\Theory\Ax}
\newnotation\AbGrpAx{\Ax_{\mathrm{Ab}}}{Presentation of Abelian groups.}
\newnotation\AbGrpSig{\uaSignature_{\mathrm{Ab}}}{Presentation of Abelian groups.}
\newnotation\AbMinusAx{\Ax_{\mathrm{Neg}}}{Presentation of Abelian groups.}
\newnotation\AbMinusSig{\uaSignature_{\mathrm{Neg}}}{Presentation of Abelian groups.}
\newnotation\PresentationCat{\Category{Presentation}}{The category of presentations and translations.}
\newnotation\TheoryCat{\Category{Theory}}{The category of presentations and translation equivalence classes.}

\newnotationargsopt\uaAlgebra{1}{B}{\underline{#1}}{$\uaSignature$-algebra .}{\uaAlgebra}{}
\newnotation\uaAlgebrav{\mCv}{$\uaSignature$-algebra .}
\newnotationx\uaalgebra{2}{1={\uaAlgebra},2={\placeholder}}{{#1}\scottbrackets{#2}}{interpretation for an algebra}{\algebra}
\newnotation\valuation{\rho}{Meta-variable for valuation (in universal algebra).}
\newnotationargs\uasem1{\scottbrackets{#1}}{Valuation of a term $\mterm$ in a model under a valuation $\valuation$.}{\uasem\mterm\valuation}
\newnotation\entails\models{Validity of an equation from a theory.}
\newnotation\uahomo{h}{Homomorphism between $\uaSignature$-algebras.}
\newnotationargs\Kleene1{{#1}^{\ast}}{The set of finite lists of elements from $\mX$.}{\Kleene\mX}
\newnotation\uasub{\theta}{A substitution in universal algebra.}

\newnotationgroup{domain metavariable}{Metavariables for domains
($\mW$ is mnemonic of $\omega$, and we go in reverse alphabetical
order from there.)}{\mW,
\mWv, \mWw}
\newnotationmember{domain metavariable}\mW{W}
\newnotationmember{domain metavariable}\mWv{V}
\newnotationmember{domain metavariable}\mWw{U}
\newnotationgroup{domain element metavariable}{Metavariable of
elements of the domains $\mW$, $\mWv$, and $\mWw$,
respectively}{\mw, \mwv, \mww}
\newnotationmember{domain element metavariable}\mw{w}
\newnotationmember{domain element metavariable}\mwv{v}
\newnotationmember{domain element metavariable}\mww{u}

\newnotation\Diagram{D}{A (usually small) diagram.}
\newnotation\DiagramIndex{J}{The (usually small) domain of a diagram
$\Diagram \of \DiagramIndex \to \ValCat$..}
\newnotation\mindex{j}{Metavariable for objects in the domain of a
diagram $\Diagram \of \DiagramIndex \to \ValCat$.}
\newnotationargsopt{\Limit}{1}{{}}{{\mathop{\mathrm{Lim}}}_{#1}}{Limit
(limit object and morphism) for a diagram
$\Diagram \of \DiagramIndex \to \ValCat$ in the category
$\ValCat$}{\Limit[\ValCat]\Diagram}
\newnotation\mlimit{L}{Metavariable for a limit.}
\newnotation\mcone{\sigma}{Metavariable for a cone for a diagram.}
\newnotation\lub{\bigvee}{supremum of an $\omega$-chain.}
\newnotation\EgliMilnerLeq{\leq_{\rm{EM}}}{The Egli-Milner relation
induced by $\leq$.}

\newnotationargsopt\swap{1}{nosubscript}{{\ifthenelse{\equal{#1}{nosubscript}}{\mathrm{swap}}{\mathrm{swap}_{\oh@dcomma#1}}}}
{The symmetry isomorphism
$\swap[\mV\mVv]\of\mV\times\mVv\to\mVv\times\mV$ in a cartesian category.}{\swap[\mV\mVv]}

\newnotation\mR{\mathcal{R}}{Relation metavariable}
\newnotation\Diagonal{\Delta}{Diagonal relation}
\newnotation\mPoset{P}{Poset metavariable.}
\newnotationargs\wChains{1}{\omega\mathrm{Chains}({#1})}{The set of ascending $\omega$-chains of
the poset $\mPoset$}{\wChains\mPoset}
\newnotation\trueval{\mathtt{True}}{The Boolean value 'true'.}
\newnotation\falseval{\mathtt{False}}{The Boolean value 'false'.}

\newnotation\SymMonCat{\ValCat}{Symmetric monoidal closed category.}
\newnotationargs\symmoncatcarrier{1}{\carrier{#1}}{Underlying category
of a symmetric monoidal category $\SymMonCat$}{\symmoncatcarrier\SymMonCat}
\newnotation\oI{\mathbb{I}}{Unit in a symmetric monoidal
category.}
\newnotation\ox{\otimes}{Tensor product in a symmetric monoidal
category.}
\newnotation\oto{\multimap}{Closed structure in a symmetric monoidal
category.}
\newnotation{\leftunitor}{\mathrm{unit}_{\mathrm{left}}}{Left unitor
in a monoidal category.}
\newnotation{\rightunitor}{\mathrm{unit}_{\mathrm{right}}}{Right
unitor in a monoidal category.}
\newnotation{\associator}{\mathrm{assoc}}{Associator in a monoidal
category.}
\newnotation{\symmetry}{\mathrm{symm}}{Symmetry of a symmetric
monoidal category.}
\newnotation{\richCat}{\Cate{C}}{Enriched category.}
\newnotation{\richCatv}{\Cate{B}}{Enriched category.}
\newnotation{\richCatw}{\Cate{A}}{Enriched category.}
\newnotation{\richCatfact}{\Cate{L}}{Factorised enriched category.}
\newnotation{\richCatfactv}{\Cate{M}}{Variant of a factorised enriched category.}
\newnotation{\enA}{\underline{A}}{Object in an enriched category.}
\newnotation{\enAv}{\underline{B}}{Object in an enriched category.}
\newnotation{\enAw}{\underline{C}}{Object in an enriched category.}
\newnotation{\enAx}{\underline{D}}{Object in an enriched category.}
\newnotationargs{\richConcept}{1}{\underline{#1}}{The
enriched concept (arrow, natural transformation) corresponding to the
ordinary one.}{\richConcept{X}}
\newnotationargsopt{\enId}{1}{}{\underline{\id}_{#1}}{Identity morphism
in an enriched category.}{\enId}
\newnotationargsopt{\enComp}{1}{}{\mathbin{\underline{\compose}_{#1}}}{Composition
in an enriched category.}{\enComp{\enA,\enAv,\enAw}}
\newnotationargsopt{\enCompWithCat}{2}{}{\mathbin{\underline{\compose}_{#1}^{#2}}}{Composition
in an enriched category.}{\enComp{\enA,\enAv,\enAw}{\richCat}}
\newnotationargs{\ordinary}{1}{\carrier{#1}_{\mathrm{o}}}{Ordinary
concept (category, functor, transformation) underlying the enriched one.}{\ordinary{\richCat}}
\newnotation{\symV}{V}{Metavariable for an object in a symmetric
monoidal closed category.}
\newnotation{\symVv}{W}{Metavariable for an object in a symmetric
monoidal closed category.}
\newnotation{\symVw}{U}{Metavariable for an object in a symmetric
monoidal closed category.}
\newnotationargsopt\powertuple{2}{}{\seq[#1]{#2}}{The canonical isomorphism
exhibiting $\power\symV\enA$ as a power.}{\powertuple[\symV]{f \of \enAv
\to \enA}}
\newnotationargsopt\invpowertuple{2}{}{\seq[#1][-1]{#2}}{The inverse
of the canonical isomorphism
exhibiting $\power\symV\enA$ as a power.}{\invpowertuple[\symV]{g}}
\newnotationargsopt\powertupleWithCat{3}{}{\seq[#2]{#3}}{The canonical isomorphism
exhibiting $\power\symV\enA$ as a power.}{\powertuple[\symV]{f \of \enAv
\to \enA}}
\newnotationargsopt\invpowertupleWithCat{3}{}{\seq[#2][-1]{#3}}{The inverse
of the canonical isomorphism
exhibiting $\power\symV\enA$ as a power.}{\invpowertuple[\symV]{g}}
\WithSuffix\newcommand\powertupleWithCat*[3][{}]{\seq[#2]{\,\richConcept{#3}\,}}
\WithSuffix\newcommand\invpowertuple*[2][{}]{\invpowertuple[{#1}]{\,\richConcept{#2}\,}}
\WithSuffix\newcommand\powertuple*[2][{}]{\powertuple[{#1}]{\,\richConcept{#2}\,}}
\newnotationargsopt\copowertuple{2}{}{\coprodmorphismseq[#1]{#2}}{The canonical isomorphism
exhibiting $\copower\symV\enA$ as a copower.}{\copowertuple[\symV]{f \of \enAv
\to \enA}}
\newnotationargsopt\invcopowertuple{2}{}{\bracks{#2}_{#1}^{-1}}{The inverse
of the canonical isomorphism
exhibiting $\copower\symV\enA$ as a copower.}{\invcopowertuple[\symV]{g}}

\newnotationargs\power{2}{\prod_{#1}{#2}}{The power of $\enA$ by
$\symV$}{\power\symV\enA}
\newnotationargs\copower{2}{\sum_{#1}{#2}}{The copower of $\enA$ by $\symV$}{\copower\symV\enA}


\newnotationargs\powercounit{1}{\projection_{#1}}{Power
counit.}{\powercounit\placeholder}
\WithSuffix\newcommand\powercounit*[1]{\richConcept\projection_{#1}}
\newnotationargs\copowercounit{1}{\injection_{#1}}{Copower counit.}{\copowercounit\placeholder}
\newnotationargs\plam{2}{\lam{#1}{#2}}{The bijection
$\plam\symV \of \homset[\SymMonCat]{\symVv\ox\symV}{\symVw} \isomorphic
\homset[\SymMonCat]{\symV}{\symV\oto\symVw}$ induced by a
symmetric monoidal closed structure}{\plam\symV f}
\newnotationargs\invplam{2}{\inv*{\lambda{#1}}.{#2}}{The (inverse) bijection
$\plam\symV \of \homset[\SymMonCat]{\symVv\ox\symV}{\symVw} \xfrom{\isomorphic}
\homset[\SymMonCat]{\symV}{\symV\oto\symVw}$ induced by a
symmetric monoidal closed structure}{\invplam\symV f}

\newnotation\Functor{F}{Enriched functor metavariable.}
\newnotation\Functorv{G}{Enriched functor metavariable.}
\newnotation\Functorw{H}{Enriched functor metavariable.}
\newnotationargsopt\enMonadUnit{1}{}{\underline{\eta}_{#1}}{Enriched
monad unit.}{\enMonadUnit}
\newnotationargsopt\enMonadMult{1}{}{\underline{\mu}_{#1}}{Enriched monad multiplication.}{\enMonadMult}

\newnotationargs\ModCat{2}{\mathop{{\bf Mod}}\!\!\parent{{#1},{#2}}}{Category
of $L$ models.}{\ModCat{L}{\mCat}}

\newnotationargsopt\Pres{2}{\regcard}{\mathop{\Category{Pres}_{#1}}\!\!{#2}}{Full
subcategory of $\mCat$ consisting of the $\regcard$-presentable objects.}{\Pres\mCat}
\newnotationargsopt\PresOp{2}{\regcard}{\mathop{\opposite{\Category{Pres}}_{#1}}\!\!{#2}}{The
opposite $\mCat$-category of $\Pres\mCat$.}{\PresOp\mCat}

\newnotation\mL{\Cate L}{Meta-variable for an enriched Lawvere theory.}
\newnotation\mLv{\widehat{\Cate L}}{Meta-variable for an enriched Lawvere theory.}
\newnotationargs{\LawCat}{1}{\carrier{#1}}{Underlying category of an enriched
Lawvere theory $\mL$.}{\LawCat\mL}
\newnotationargs{\LawFunctor}{2}{{#1}\scottbrackets{#2}}{The functor associated with an
enriched Lawvere theory $\mL$}{\LawFunctor\mL\placeholder}
\newnotationargs{\LawOpsem}{2}{{#1}\scottbrackets{#2}}{The algebraic
operation for $\mop$ in a Lawvere theory $\mL$ for $\mop$.}{\LawOpsem\mL\mop}
\newnotationargs{\MonadTheory}{1}{\mL_{#1}}{The Lawvere theory
associated with a monad $\Monad$.}{\MonadTheory\Monad}
\newnotation{\mModel}{\Cate M}{A model of a Lawvere theory.}
\newnotation{\mhomo}{h}{A homomorphism between models of
Lawvere theories.}

\newnotationargs{\LawU}1{U_{#1}}{The forgetful functor from
$\ModCat\mL\richCat$ to $\richCat$}{\LawU\mL}
\newnotationargs{\LawF}1{F_{#1}}{The free model functor from
$\richCat$ to $\ModCat\mL\richCat$}{\LawF\mL}
\newnotationargs{\LawMonad}1{\Monad_{#1}}{The free $\mL$-model monad
over $\SymMonCat$.}{\LawMonad\mL}
\newnotation{\LawHomo}{\mathfrak{T}}{A morphism (i.e., translation)
between Lawvere theories.}
\newnotation{\LawHomos}{\mathfrak{S}}{A morphism (i.e., translation)
between Lawvere theories.}
\newnotation{\LawFillin}{\mathfrak{F}}{A morphism (i.e., translation)
between Lawvere theories.}
\newnotation{\LawFillinv}{\hat{\mathfrak{F}}}{A morphism (i.e., translation)
between Lawvere theories.}
\newnotation{\LawHomov}{\hat{\mathfrak{T}}}{A morphism (i.e., translation)
between Lawvere theories.}
\newnotation{\LawMono}{{\mathfrak{M}}}{A componentwise monomorphism (i.e., translation)
between Lawvere theories.}
\newnotation{\LawMonov}{\hat{\mathfrak{M}}}{A componentwise monomorphism (i.e., translation)
between Lawvere theories.}
\newnotation{\LawEpi}{\mathfrak{E}}{A morphism (i.e., translation)
between Lawvere theories.}
%% \newnotation{\LawEpiv}{\hat{\mathfrak{E}}}{A componentwise epimorphism (i.e., translation)
%% between Lawvere theories.}
\newnotationargsopt{\Lawvere}2{\regcard}{\Category{Law}_{#1}{#2}}{The
category of $\regcard$-Lawvere $\SymMonCat$-theories.}{\Lawvere\SymMonCat}
\newnotationargs{\EnrichedMonad}1{{#1}\mhyphen\Category{Monads}}{The
category of $\SymMonCat$-enriched monads over $\SymMonCat$.}{\EnrichedMonad\SymMonCat}
\newnotationargsopt{\EnrichedRankedMonad}2{\regcard}{{#2}\mhyphen\Category{Monads}_{#1}}{The
category of $\regcard$-ranked $\SymMonCat$-enriched monads over $\SymMonCat$.}{\EnrichedRankedMonad\SymMonCat}

\newnotation\equivalence{\simeq}{Categorical equivalence.}
\newnotation\LawSignature{\sigma}{Signature for a Lawvere theory.}
\newnotationargs\SignatureTheory{1}{\mL_{#1}}{The initial $\LawSignature$-theory.}{\SignatureTheory\LawSignature}

\newnotation\SignatureFunctor{\Sigma}{A signature functor (for using
free monads.)}

\newnotationargs\FreeMonad{1}{\Monad_{#1}}{Free monad for the
signature functor $\SignatureFunctor$}{\FreeMonad\SignatureFunctor}

\newnotation{\Epi}{\mathcal{E}}{Epi class in a factorisation system.}
\newnotation{\Mono}{\mathcal{M}}{Mono class in a factorisation
system.}
\newnotation{\MorClass}{\mathcal{F}}{A morphism class.}
\newnotation\mepi{e}{pseudo-epimorphism metavariable}
\newnotation\epimor{\twoheadrightarrow}{pseudo-epi arrow.}
\newnotation\mmono{m}{pseudo-monomorphism metavariable}
\newnotation\monic{\monomo}{A monomorphism.}
\newnotation\monomor{\rightarrowtail}{pseudo-mono arrow.}
\newnotation\monofrom{\leftarrowtail}{pseudo-mono arrow.}
\newnotation\mVfact{L}{The factorisation object in a factorisation
system.}
\newnotation\mVfactv{M}{The factorisation object in a factorisation
system.}
\newnotation\leftorth{\perp}{Left orthogonality relation}
\newnotationargs\LeftOrth{1}{{\vphantom{#1}^{\perp}\!{#1}}}{Left
orthogonality class of $\Mono$}{\LeftOrth\Mono}
\newnotationargs\pullbackalong{2}{{#1}^*\!\parent{#2}}{The pullback of
$\mmorph$ along $\mmorphv$}{\pullbackalong\mmorphv\mmorph}
\usepackage{extpfeil}

\newnotationargs\FunctorFact{1}{{#1}^{\mathrm{law}}}{The factorisation
system on $\SymMonCat$-functors induced by a factorisation system
in $\SymMonCat$.}{\pair{\FunctorFact\Epi}{\FunctorFact\Mono}}
\WithSuffix\newcommand\FunctorFact*[1]{\FunctorFact{#1}_{*}}
\newnotationargs\MonadFact{1}{{#1}^{\mathrm{mon}}}{The factorisation
system on ranked $\SymMonCat$-monads induced by a factorisation system
in $\SymMonCat$.}{\pair{\MonadFact\Epi}{\MonadFact\Mono}}
\newnotation\mEpi{E}{A componentwise epi functor.}
\newnotation\mMono{M}{A componentwise mono functor.}
\newnotationargs\xepimor{1}{\xtwoheadrightarrow{#1}}{Extensible pseudo-epimorphism}{\mV \xepimor{\ilam\mV
{f\compose g}} \mVv}
\newnotationargs\xmonomor{1}{\xrightarrowtail{\ \ #1\ \ }}{Extensible pseudo-monomorphism}{\mV \xmonomor{\ilam\mV
{f\compose g}} \mVv}
\newnotationargs\xmonofrom{1}{\xleftarrowtail{\ \ #1\ \ }}{Extensible pseudo-monomorphism}{\mV \xmonofrom{\ilam\mV
{f\compose g}} \mVv}
\newnotation\ArrowCat{\sierp}{The arrow category consisting of two
objects and a single non-trivial arrow.}
\newnotation\SolutionSet{S}{Meta-variable for a solution set.}
\newnotation\Pullback{P}{Pullback object.}

\newnotation\PresObj{\mathbb{P}}{A set of representatives of
equivalence classes of the $\regcard$-presentable objects.}
\newnotationargs\Subobjects{1}{\mathop{\mathrm{Sub}}\!\parent{#1}}{The
set of non-isomorphic representatives of subojects of $\mV$ in a
well-powered category}{\Subobjects\mV}

\newnotation\skeletal\partial{An equivalence functor from $\Pres\SymMonCat$ to
one of its skeleton.}

\newnotationargs\TheoryPresheaf{1}{\mL_{#1}}{Presheaf of theories
  metavariable.}{\TheoryPresheaf\placeholder}
\newnotationargsopt\algopsem{2}{\e}{\mL_{#1}\scottbrackets{#2}}{Algebraic
operation assigned in  to $\mop$ at level $\e$ in an algebraic model}{\algopsem\mop}
\newnotation\equivalent{\simeq}{Equivalence of categories.}
\newnotationargs\restrict{2}{\left.{#1}\right\rvert_{#2}}{The
restriction of the function $f$ to a subset $\mX$ of its
domain}{\restrict f\mX}

\newcommand\benchmarksymbol\flat
\newcommand\conservativesymbol\sharp
\newnotationargs\benchmark1{{#1}_{\flat}}{Benchmark model arising from
$\mModel$.}{\benchmark\mModel}
\newnotationargs\conservative1{{#1}_{\sharp}}{Conservative restriction
model arising from $\mModel$.}{\conservative\mModel}

\newnotationargsopt\PredCat1{}{\Category{Pred}_{#1}}{The
category of predicates over a category}{\PredCat[\Set], \PredCat[\wCPO]}

\newnotationgroup{predicates}{Meta-variables for predicates.}
                             {\mPred, \mPredv, \mPredr, \mPreds}
\newnotationmember{predicates}\mPred{P}
\newnotationmember{predicates}\mPredv{Q}
\newnotationmember{predicates}\mPredr{R}
\newnotationmember{predicates}\mPreds{S}

\newnotationgroup{predicates-members}{Meta-variables for elements of predicates.}
                                     {\mpred, \mpredv, \mpredr, \mpreds}
\newnotationmember{predicates-members}\mpred{p}
\newnotationmember{predicates-members}\mpredv{q}
\newnotationmember{predicates-members}\mpredr{r}
\newnotationmember{predicates-members}\mpreds{s}

\newnotationgroup{lifted}{The lifting of a concept (morphism, monad, etc.) to a predicate.}{\lmorph, \lltimes, \ldots}
\newnotationmember{lifted}\lmorph{\dot{f}}
\newnotationmember{lifted}\lAlgebra{\underline{\dot{B}}}
\newnotationmember{lifted}\lAr{\dot{A}}
\newnotationmember{lifted}\lPa{\dot{P}}
\newnotationmember{lifted}\lltimes{\mathbin{\dot{\times}}}
\newnotationmember{lifted}\lMonadMorphism{\dot{m}}

\newnotation\IndexSet{I}{Index set}
\newnotation\mind{i}{element of an index set}
\newnotation\LogRel{\Category{LogRel}}{The category of logical relations.}

\newnotationgroup{logrel}{The predicate part in a logical relation.}{\lX, \lY, \lZ}
\newnotationmember{logrel}\lX{\dot X}
\newnotationmember{logrel}\lY{\dot Y}
\newnotationmember{logrel}\lZ{\dot Z}

\newnotation{\SetPairFun}{\U_{\Set\times\Set}}{The forgetful functor from $\LogRel$ to $\Set\times\Set$.}
\newnotation{\PredFun}{\U_{\PredCat}}{The forgetful functor from $\LogRel$ to $\PredCat$.}
\newnotation{\CodFun}{\mathrm{Cod}}{The forgetful functor from $\PredCat$ to $\Set$ (the codomain fibration).}
\newnotation{\RelMon}{\dot{T}}{The relation part a lifted monad.}
\newnotation{\RelFam}{\mathcal{R}}{The family of relations respecting the monad unit and operations in the free lifting construction.}

\newnotation\tu{{{\bf u}}}{Universal algebra variable.}
\newnotation\tv{{{\bf v}}}{Universal algebra variable.}
\newnotation\tw{{{\bf w}}}{Universal algebra variable.}
\newnotation\tx{{{\bf x}}}{Universal algebra variable.}
\newnotation\ty{{{\bf y}}}{Universal algebra variable.}
\newnotation\tz{{{\bf z}}}{Universal algebra variable.}
\newnotationgroup{opsym}{Universal algebra operation symbols.}{\uamop, \uamopv, \uamopw}
\newnotationmember{opsym}{\uamop}{f}
\newnotationmember{opsym}{\uamopv}{g}
\newnotationmember{opsym}{\uamopw}{h}

\newnotationargs{\PresAx}{1}{\Ax_{#1}}{The presentation at level $\e$
of a presentation $\Signature$-model.}{\PresAx\e}

\newnotationargs{\PresTrans}{1}{\mathfrak{L}_{#1}}{The translation
from level $\e$ to level $\e'$ in a presentation
$\Signature$-model.}{\PresTrans{\e\subset\e'}}

\newnotationargsopt{\presopsem}{2}{\e}{\mathcal{T}_{#1}\scottbrackets{#2}}{The
interpretation of operation $\mop$ at level $\e$ of a presentation
$\Signature$-model.}{\presopsem\mop}


\newnotation\mDoubleStrength {\psi}{Double strength for
monad $\e$.}
\newnotation\mVarDoubleStrength{\tilde\psi}{Other double strength for
monad $\e$.}

\newnotation\vmorph{\tilde f}{A variation on a morphism $\mmorph$. }
\newnotation\vmonmult{\tilde \mu}{A variation on the monadic multiplication.}
\newnotationargs\TensorEq2{E_{{#1}\tensor{#2}}}{The commuting equations
of the tensor product of two
presentations.}{\TensorEq{\uaSignature_1}{\uaSignature_2}}
\newnotation\Tensor{\bigotimes}{$A$-fold tensor of theories.}

\newnotation\Translation{\mathfrak{T}}{Metavariable fora translation
between presentation.}
\newnotation\EpiTrans{\mathfrak{E}}{Metavariable for a surjective
translation between presentation.}
\newnotation\IsoTrans{\mathfrak{I}}{Metavariable for an isomorphism
translation between presentation.}
\newnotation\MonoTrans{\mathfrak{M}}{Metavariable for a conservative translation between presentation.}
\newnotation\TransEq{\sim}{The equivalence relation between translations.}
\newnotation\VarSet{\mathbb{Var}}{A fixed set of variables.}

\newnotationargs\ressig1{\uaSignature_{#1}}{The auxiliary signature
used in presentation conservative restriction theorem.}{\ressig\e}
\newnotationargs\enum1{\mathrm{enum}_{#1}}{The auxiliary
enumeration bijection used in presentation conservative restriction
theorem.}{\enum\mop}
\WithSuffix\newcommand\enum*[1]{\mathrm{enum}_{#1}^{-1}}
\newnotationargs\resinit1{\Translation_{#1}}{The auxiliary initial translation
used in presentation conservative restriction theorem.}{\resinit\e}
\newnotationargs\resepi1{\EpiTrans_{#1}}{The auxiliary surjective translation
used in presentation conservative restriction theorem.}{\resepi\e}
\newnotationargs\resmono1{\MonoTrans_{#1}}{The auxiliary conservative translation
used in presentation conservative restriction theorem.}{\resmono\e}
\newnotationargs\resinittrans1{\mathfrak{S}_{#1}}{The auxiliary initial
translation used in presentation conservative restriction
theorem.}{\resinittrans{\e\subset\e'}}