\makeatletter
\autodefs{\bSet\bMag\bVect\bPoset\bRelGr\bCat\bGr\bmSLat\ftype\fprop\fctx\fpreterm\bPrCat\bCoprCat\bMCat\bRepMCat\bSymMulti\bCartMulti\bMGr\bMPos\bRelMGr\bMonPos\bMonCat\bSMPos\bSMC\bProp\bTV\bHeyting\fapp\bPres\nSub\nSieve\nMap\bStrMonCat\sPrCat\sCartMulti}
\autodefs{\nAut\nShuf}
\def\tv{\mathbf{2}}
\def\tr{\mathrm{tr}}
\let\sect\section
\def\idfunc{\mathsf{id}}
\def\finsubset{\subset_{\mathrm{fin}}}
% coalgebras
\let\comult\triangle
\let\counit\varepsilon
% well-founded trees and algebras
\def\ay{\mathrm{ar}}
\def\sig{\Sigma}
\def\axes{\Lambda}
\def\act#1{[#1]}
\def\equivsym{\mathord{\equiv}}
% derivations
\def\derivof#1{\inferrule*{\vdots}{#1}}
\def\labderivof#1#2{\inferrule*{#1\\\\\vdots}{#2}}
% contexts
\let\merge\boxplus
\def\ec{()} % empty context
% judgments
\let\types\vdash
\let\cb\mid
\def\type{\;\ftype}
\def\prop{\;\fprop}
\def\ctx{\;\fctx}
\def\preterm{\;\fpreterm}
\newcommand{\pc}{\mathrel{\mathord{:}?}}
\newcommand{\atom}{\mathrel{\downarrow}}
\newcommand{\can}{\mathrel{\uparrow}}
\newcommand{\var}{\mathrel{\Downarrow}}
\newcommand{\pop}{\mathsf{pop}}
\newcommand{\shf}{\mathsf{shift}}
\newcommand{\use}{\mathsf{use}}
\newcommand{\atomcan}{\ensuremath{\mathord{\downarrow\uparrow}}}
\newcommand{\focus}[1]{[#1]}
\newcommand{\postcsym}[1]{#1\mathord{\circ}}
\newcommand{\postc}[2]{\postcsym{#1}(#2)}
\newcommand{\precsym}[1]{\mathord{\circ}#1}
\let\preceeds\prec
\renewcommand{\prec}[2]{(#1)\precsym{#2}}
% props and their type theory
\def\s#1{_{\scriptscriptstyle(#1)}}
\def\ss#1#2{_{\scriptscriptstyle(#1)(#2)}}
\let\ptens\bullet
\newcommand{\actv}[1]{{#1}^\star}
\newcommand{\atleastone}[1]{{#1}^{\scriptscriptstyle \ge 1}}
\newcommand{\oneactv}[1]{{#1}^{\star\scriptscriptstyle\ge 1}}
\newcommand{\zeroactv}[1]{{#1}^{\star\scriptscriptstyle = 0}}
\newcommand{\allactv}[1]{{#1}^{\star}}
% substitution
\newcommand{\alsub}[1]{\langle #1\rangle}
\newcommand{\hsub}[1]{\llbracket #1\rrbracket}
\newcommand{\hid}[1]{\mathbbb{id}_{#1}}
% free functors
\newcommand{\F}[1]{\mathfrak{F}_{#1}}
% composition
\def\comp#1{\circ_{#1}}
% meet
\let\meet\wedge
\def\meetL{\mathord{\meet}L}
\def\meetR{\mathord{\meet}R}
\def\meetE{\mathord{\meet}E}
\def\meetI{\mathord{\meet}I}
% join
\let\join\vee
\let\bigjoin\bigvee
\def\joinL{\mathord{\join}L}
\def\joinR{\mathord{\join}R}
\def\joinE{\mathord{\join}E}
\def\joinI{\mathord{\join}I}
% unit
\def\unit{\mathbbb{1}}%{\top}%{\mathbf{1}}
\def\ttt{\mathord{\ast}}%{\mathsf{tt}}
% product
\def\timesE{\ensuremath{\mathord{\times}E}}
\def\timesI{\ensuremath{\mathord{\times}I}}
\def\timesR{\ensuremath{\mathord{\times}R}}
\def\timesL{\ensuremath{\mathord{\times}L}}
\def\pair#1#2{\langle #1,#2\rangle}
\def\pr#1#2#3{\pi_{#1}^{#2,#3}}
% coproduct
\def\plusE{\mathord{+}E}
\def\plusI{\mathord{+}I}
\def\plusL{\mathord{+}L}
\def\plusR{\mathord{+}R}
\def\inl{\mathsf{inl}}
\def\inr{\mathsf{inr}}
\def\acase#1#2{\mathsf{match}_{#1+#2}}
\def\case{\mathsf{match}_+}
% general positives
\def\match{\mathsf{match}}
% empty
\def\zero{\mathbf{0}}
\def\zeroE{\mathbf{0}E}
%\def\abort{\mathsf{abort}}
\def\abort{\match_{\zero}}
% one
\def\one{\mathbf{1}}
\def\ott{\mathord{\star}}%{\mathsf{tt}}
%\def\discard#1in{\mathsf{discard}\; #1 \; \mathsf{in} \;}
% tensor
\let\tensor\otimes
\def\tensorL{\mathord{\tensor}L}
\def\tensorR{\mathord{\tensor}R}
\def\tensorI{\mathord{\tensor}I}
\def\tensorE{\mathord{\tensor}E}
% \def\flet#1:{\mathsf{let}\;#1 \@ifnextchar:\@fletdoublecolon\@fletsinglecolon}
% \def\fletp#1:{\mathsf{let}'\;#1 \@ifnextchar:\@fletdoublecolon\@fletsinglecolon}
% \def\@fletdoublecolon:=#1in{\Coloneqq #1\;\mathsf{in}\;}
% \def\@fletsinglecolon=#1in{\coloneqq #1\;\mathsf{in}\;}
\def\tpair#1#2{\text{\textlquill} #1,#2 \text{\textrquill}}%{\llparenthesis #1,#2\rrparenthesis}
\let\bigtensor\bigotimes
% hom
\let\map\hom
\let\hom\multimap
\def\homL{\mathord{\hom}L}
\def\homR{\mathord{\hom}R}
\def\homI{\mathord{\hom}I}
\def\homE{\mathord{\hom}E}
\let\To\Rightarrow
\def\ToL{\mathord{\To}L}
\def\ToR{\mathord{\To}R}
\def\ToI{\mathord{\To}I}
\def\ToE{\mathord{\To}E}
\def\toL{\mathord{\to}L}
\def\toR{\mathord{\to}R}
\def\toI{\mathord{\to}I}
\def\toE{\mathord{\to}E}
% dual
\def\d{^\bullet}
% forall
\let\all\forall
\def\forall#1:#2.{\all #1\mathord{:}#2.\,}
\def\forallI{\mathord{\all}I}
\def\forallE{\mathord{\all}E}
\def\forallR{\mathord{\all}R}
\def\forallL{\mathord{\all}L}
\def\forallS{\mathord{\all}S}
% exists
\let\exis\exists
\def\exists#1:#2.{\exis #1\mathord{:}#2.\,}
\def\existsI{\mathord{\exis}I}
\def\existsE{\mathord{\exis}E}
\def\existsR{\mathord{\exis}R}
\def\existsL{\mathord{\exis}L}
\def\existsS{\mathord{\exis}S}
% equality
\def\eqI{\mathord{=}I}
\def\eqE{\mathord{=}E}
\def\eqR{\mathord{=}R}
\def\eqL{\mathord{=}L}
% Theories
\def\timespres#1{\bPres_{\times,#1}}
\def\prcat#1{\bPrCat_{#1}}
\def\stlcpres#1{\bPres_{\times,+,\to,#1}}
\def\cccc#1{\mathbf{CCCC}_{#1}}
\def\m#1{\llbracket #1\rrbracket}
% Multicategories
\let\convolve\boxtimes
\def\catctx#1{\widehat{#1}}
\def\intern{{\textstyle\mathord{\int}}}
% hyperdoctrines
\newcommand{\sub}{\nSub}
\newcommand{\sieve}{\nSieve}
% free morphisms
\newcommand{\pfree}{\omega}
\newcommand{\free}{\overline{\omega}}
% 
% Collect exercises at the end of each chapter.  The upshot of this
% hackery is that we can write \begin{ex}\label{ex:name}...\end{ex} as
% usual in the text, and then at the end of each chapter
% write \ChapterExercises to get a re-stated list of all exercises
% from that chapter (or, more precisely, since the last
% time \ChapterExercises was run) with the same numbers.
%
% NB: Every \begin{ex} MUST be followed immediately by a \label!
\newtheorem*{rep@theorem}{\rep@title}
\def\repex#1\endrepexname{%
  \def\rep@title{\bf Exercise \ref{#1}}
  \begin{rep@theorem} }
\def\endrepex{\end{rep@theorem}}
\def\exaccum{}
\def\exname{}
\def\get@lab#1\label{\get@@lab}
\def\get@@lab#1{\gdef\exname{#1}\eat@body}
\long\def\eat@body#1\end@eat{}
\NewEnviron{ex}{%
  \begin{@ex}\BODY\end{@ex}%
  \ea\get@lab\BODY\end@eat
  \g@addto@macro\exaccum{\repex}
  \ea\g@addto@macro\ea\exaccum\ea{\exname}
  \g@addto@macro\exaccum{\endrepexname}
  \ea\g@addto@macro\ea\exaccum\ea{\BODY}
  \g@addto@macro\exaccum{\endrepex}
}{}
\def\ChapterExercises{\section*{Collected Exercises}
  For convenient reference, we collect the exercises from all sections in this chapter.
  \bgroup\def\label##1{}\exaccum\egroup%
  \def\exaccum{}}
%
\makeatother