style.sty

\ProvidesPackage{style}

% required packages
\RequirePackage{checkend}
\RequirePackage{enumitem}
\RequirePackage{graphicx}
\RequirePackage{multicol}
\RequirePackage{booktabs}
\RequirePackage{xspace}
\RequirePackage{xcolor}
\RequirePackage{suffix}
\RequirePackage{minted}
\RequirePackage{tikz-cd}
\RequirePackage{stmaryrd}
\RequirePackage{mathtools}
\RequirePackage{mathpartir}
\RequirePackage[capitalize, noabbrev]{cleveref}

% font for code listings
\newfontfamily{\codefont}{iosevka.ttc}

% save default lengths
\newlength{\@fboxsepdefault}
\setlength{\@fboxsepdefault}{\fboxsep}

% \newcmd*{\cmd}[n]{expression} defines the suffixed command \cmd*
% similarly for \newcmd<
\WithSuffix\newcommand\newcmd*[3]{\WithSuffix\newcommand#1*#2{#3}}
\WithSuffix\newcommand\newcmd<[3]{\WithSuffix\newcommand#1<#2{#3}}

% rule labels:
% \rlabel{name}{label} creates given label and prints name
% \rref{label} prints "Rule <name>"
% \rref{label, label} prints "Rules <name> and <name>"
% \rref{label, ..., label} prints "Rules <name>, ..., and <name>"
% NOTE: \rule and \@rule seem to conflict with footnotes, somehow??
\newcounter{nrules}
\newcommand{\rlabel}[2]{%
  \edef\@currentlabelname{#1}%
  \phantomsection\label{#2}#1%
}
\newcmd*{\rlabel}[1]{\rlabel{#1}{#1}}
\newcommand{\rref}[1]{%
  \setcounter{nrules}{0}%
  \edef\r@les{\zap@space #1 \@empty}%
  \@for\r@le:={#1}\do{\addtocounter{nrules}{1}}%
  \ifcase \value{nrules}
  \or Rule~\mbox{\textsc{\nameref{#1}}}%
  \or Rules\@for\r@le:={\r@les}\do{
    \ifcase \value{nrules}
    \or and \mbox{\textsc{\nameref{\r@le}}}%
    \else \mbox{\textsc{\nameref{\r@le}}}%
    \fi
    \addtocounter{nrules}{-1}%
  }%
  \else Rules\@for\r@le:={\r@les}\do{
    \ifcase \value{nrules}
    \or and \mbox{\textsc{\nameref{\r@le}}}%
    \else \mbox{\textsc{\nameref{\r@le}}},%
    \fi
    \addtocounter{nrules}{-1}%
  }%
  \fi
}
\newcmd*{\rref}[1]{\mbox{\textsc{\nameref{#1}}}}

% colours for:
% - metafunctions (pale magenta)
% - keywords (golden yellow)
% - constants (soft blue)
% - constructions (turquoise)
% - target language (dark orange)
% by Okabe and Ito (https://jfly.uni-koeln.de/color/#pallet)
\definecolor{metacolour}{HTML}{CC79A7}
\definecolor{kwcolour}{HTML}{E69F00}
\definecolor{constcolour}{HTML}{0072B2}
\definecolor{constrcolour}{HTML}{009E73}
\definecolor{targetcolour}{HTML}{D55E00}
\definecolor{newcolour}{gray}{0.85}

% various theorem environments
\newtheorem{theorem}{Theorem}[section]
\newtheorem{definition}[theorem]{Definition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{sublemma}[theorem]{Sublemma}
\newtheorem{postulate}[theorem]{Postulate}
\newtheorem{corollary}[theorem]{Corollary}

% foreign phrases
\newcommand{\eg}{\emph{e.g.}\@\xspace}
\newcommand{\ie}{\emph{i.e.}\@\xspace}
\newcommand{\cf}{\emph{cf.}\@\xspace}
\newcommand{\etal}{\emph{et al.}\@\xspace}
\newcommand{\ala}{\emph{\`a la}\xspace}
\newcommand{\opcit}{\emph{op.\! cit.}\@\xspace}
\newcommand{\TODO}{\meta{\texttt{TODO}}\xspace}

% check mark, cross mark, interrogation mark
\newcmd*{\checkmark}[0]{\Large\textbf{\textcolor{constrcolour}{\checkmark}}}
\newcommand{\crossmark}{\large$\displaystyle\mathbf{\times}$}
\newcommand{\interromark}{?}

% slanted fractions
\newcommand{\sfrac}[2]{{}^{#1}\!/_{#2}}

% use this before footnote to stack footnote mark above punctuation
\newlength{\@punctwidth}
\newcommand{\punctstack}[1]{#1%
  \settowidth{\@punctwidth}{#1}%
  \hspace*{-\the\@punctwidth}%
}

% language names
\newcommand{\lang}{STT\xspace}
\newcommand{\GCC}{CC$^\omega$\xspace}
\newcommand{\Fstar}{F$\star$\xspace}
\newcommand{\lambdahat}{$\lambda\widehat{~}$\xspace}
\newcommand{\Fhat}{F$\widehat{~}$\xspace}
\newcommand{\Fhatomega}{F$\widehat{_\omega}$\xspace}
\newcommand{\Fhattimes}{F$\widehat{_{\times}}$\xspace}
\newcommand{\Fcopomega}{F$^{\textrm{cop}}_{\omega}$\xspace}
\newcommand{\CCE}{\texorpdfstring{CC$_E$}{CC(E)}\xspace}
\newcommand{\CICE}{\texorpdfstring{CIC$_E$}{CIC(E)}\xspace}
\newcommand{\CIChat}{CIC$\widehat{~}$\xspace}
\newcommand{\CIChatminus}{CIC$\widehat{_-}$\xspace}
\newcommand{\CChatomega}{CC$\widehat{\omega}$\xspace}
\newcommand{\CIChatstar}{CIC$\widehat{\ast}$\xspace}
\newcommand{\CIChatl}{CIC$\widehat{_\ell}$}
\newcommand{\CIChatsub}{CIC$\widehat{_\sqsubseteq}$\xspace}
\newcommand{\CCR}{$\mathfrak{CCR}$\xspace}

% styling
\newcommand{\meta}[1]{\textcolor{metacolour}{#1}}
\newcommand{\kw}[1]{\mathsf{\textcolor{kwcolour}{#1}}}
\newcommand{\const}[1]{\mathsf{\textcolor{constcolour}{#1}}}
\newcommand{\constr}[1]{\mathsf{\textcolor{constrcolour}{#1}}}
\newcommand{\tg}[1]{\mathtt{\textcolor{targetcolour}{#1}}}
\newcmd*{\tg}[1]{\textcolor{targetcolour}{#1}}
\newcommand{\new}[1]{%
  \setlength{\fboxsep}{3pt}%
  \colorbox{newcolour}{\rule{0em}{0.5\baselineskip}#1}%
  \setlength{\fboxsep}{\@fboxsepdefault}%
}

% delimiters
\DeclarePairedDelimiter{\sqbr}{[}{]}
\DeclarePairedDelimiter{\set}{\{}{\}}
\DeclarePairedDelimiter{\ang}{\langle}{\rangle}

% metafunctions
\newcommand{\mt}{\,\meta{\mathbf{\cdot}}\,}
\newcommand{\seq}{\,\meta{\textbf{\ldots}}\,}
\newcommand{\any}{\meta{\texttt{\_}}}
\newcommand{\hole}{\meta{\mathbf{?}}}
\renewcommand{\vec}[1]{\meta{\overline{\textcolor{black}{#1}}}}
\newcommand{\subst}[3]{#1\mathopen{\meta{\mathbf{[}}}#2 \mathrel{\meta{\mathbf{\mapsto}}} #3\mathclose{\meta{\mathbf{]}}}}
\newcommand{\card}[1]{\mathopen{\meta{\mathbf{\lvert}}} #1 \mathclose{\meta{\mathbf{\rvert}}}}
\newcommand{\compile}[1]{\mathopen{\meta{\mathbf{\llbracket}}} #1 \mathclose{\meta{\mathbf{\rrbracket}}}}
\newcmd*{\compile}[1]{\meta{\mathbf{\biggl\llbracket}} #1 \meta{\mathbf{\biggr\rrbracket}}}
\newcommand{\metafun}[2]{\meta{\textbf{#1(}}#2\meta{\textbf{)}}}
\newcmd*{\metafun}[1]{\meta{\textbf{#1}}}
\newcommand{\maximum}[1]{\metafun{max}{#1}}
\newcommand{\minimum}[1]{\metafun{min}{#1}}
\newcommand{\rules}[2]{\metafun{rule}{#1, #2}}
\newcommand{\axioms}[1]{\metafun{axiom}{#1}}
\newcmd*{\rules}[0]{\meta{\textbf{rule}}}
\newcmd*{\axioms}[0]{\meta{\textbf{axiom}}}
\newcommand{\fresh}[1]{\metafun{fresh}{#1}}
\newcommand{\FV}[1]{\metafun{FV}{#1}}
\newcommand{\elim}[3]{\metafun{elim}{#1, #2, #3}}

% source binders
\newcommand{\annot}[2]{#1 \mathrel{:} #2}
\newcommand{\define}[3]{#1 \mathrel{:} #2 \mathrel{\coloneqq} #3}
\newcmd*{\define}[2]{#1 \mathrel{\coloneqq} #2}
\newcommand{\bound}[2]{#1 \mathrel{<} #2}

% source language
\newcommand{\@et}{\:}
\newcommand{\Type}[1]{\const{Type}_{#1}}
\newcommand{\Prop}{\const{Prop}}
\newcommand{\Set}{\const{Set}}
\newcommand{\sss}[1]{\widehat{#1}}
\newcommand{\app}[1]{#1\@ifnextchar\bgroup{\@et\app}{\xspace}}
\newcommand{\@pp}[1]{\sqbr{#1}\@ifnextchar\bgroup{\@et\@pp}{\xspace}}
\newcommand{\App}[1]{#1\@ifnextchar\bgroup{\@et\@pp}{\xspace}}
\newcommand{\fun}[3]{\lambda \annot{#1}{#2} \mathpunct{.} #3}
\newcmd*{\fun}[2]{\lambda #1 \mathpunct{.} #2}
\newcommand{\Fun}[2]{\Lambda #1 \mathpunct{.} #2}
\newcmd<{\Fun}[3]{\Lambda \bound{#1}{#2} \mathpunct{.} #3}
\newcommand{\funtype}[3]{\Pi \annot{#1}{#2} \mathpunct{.} #3}
\newcommand{\Funtype}[2]{\forall #1 \mathpunct{.} #2}
\newcmd<{\Funtype}[3]{\forall \bound{#1}{#2} \mathpunct{.} #3}
\newcommand{\arr}[3]{\mathopen{(} \annot{#1}{#2} \mathclose{)} \mathrel{\rightarrow} \phantom{} #3}
\newcmd*{\arr}[1]{#1\@ifnextchar\bgroup{\mathrel{\rightarrow}\arr*}{\xspace}}
\newcommand{\letin}[4]{\kw{let} \@et #1 \mathrel{:} #2 \mathrel{\coloneqq} \phantom{} #3 \@et \kw{in} \@et #4}
\newcommand{\Let}[3]{\kw{let} \@et \annot{#1}{#2} \mathrel{\coloneqq} \phantom{} #3}
\newcommand{\Pairtype}[2]{\exists #1 \mathpunct{.} #2}
\newcommand{\Pair}[2]{\ang{#1 \mathpunct{,} #2}}
\newcommand{\unpair}[6]{\kw{let} \@et \Pair{#1}{#2}_{\Pairtype{#3}{#4}} \mathrel{\coloneqq} #5 \@et \kw{in} \@et #6}
\newcmd*{\unpair}[4]{\kw{let} \@et \Pair{#1}{#2} \mathrel{\coloneqq} #3 \@et \kw{in} \@et #4}
\newcommand{\eq}[3]{#1 \stackrel{#2}{=\joinrel=} #3}
\newcommand{\refl}[1]{\constr{refl}_{#1}}
\newcommand{\J}[3]{\constr{J}_{#1} \@et #2 \@et #3}
\newcmd*{\J}[0]{\constr{J}}
\newcommand{\Size}{\const{Size}}
\newcommand{\slim}[2]{\mathopen{\constr{\sqcup}_{#1}}#2}

% source inductives
\newcommand{\data}[2]{\kw{data} \@et \annot{#1}{#2} \@et \kw{where}}
\newcommand{\N}[1]{\App{\const{\mathbb{N}}}{#1}}
\newcmd*{\N}[0]{\const{\mathbb{N}}}
\newcommand{\W}[4]{\App{\const{\mathbb{W}} \annot{#1}{#2} \mathpunct{.} #3}{#4}}
\newcmd*{\W}[0]{\const{\mathbb{W}}}
\newcommand{\zero}[2]{\App{\constr{zero}_{\N{#1}}}{#2}}
\newcmd*{\zero}[0]{\constr{zero}}
\renewcommand{\succ}[3]{\app{\App{\constr{succ}_{\N{#1}}}{#2}}{#3}}
\newcmd*{\succ}[0]{\constr{succ}}
\renewcommand{\sup}[7]{\app{\App{\constr{sup}_{\W{#1}{#2}{#3}{#4}}}{#5}}{#6}{#7}}
\newcmd*{\sup}[0]{\constr{sup}}
\newcommand{\List}[2]{\App{\app{\const{List}}{#1}}{#2}}
\newcmd*{\List}[0]{\const{List}}
\newcommand{\nil}[3]{\App{\constr{nil}_{\List{#1}{#2}}}{#3}}
\newcmd*{\nil}[0]{\constr{nil}}
\newcommand{\cons}[5]{\app{\App{\constr{cons}_{\List{#1}{#2}}}{#3}}{#4}{#5}}
\newcmd*{\cons}[0]{\constr{cons}}
\newcommand{\Ord}[1]{\App{\const{Ord}}{#1}}
\newcmd*{\Ord}[0]{\const{Ord}}
\newcommand{\zord}[2]{\App{\constr{z}_{\Ord{#1}}}{#2}}
\newcmd*{\zord}[0]{\constr{z}}
\newcommand{\sord}[3]{\app{\App{\constr{s}_{\Ord{#1}}}{#2}}{#3}}
\newcmd*{\sord}[0]{\constr{s}}
\newcommand{\lord}[3]{\app{\App{\constr{\ell}_{\Ord{#1}}}{#2}}{#3}}
\newcmd*{\lord}[0]{\constr{\ell}}
\newcommand{\match}[3]{\kw{case} \@et #1 \@et \kw{return} \@et #2 \@et \kw{of} \@et \phantom{} #3}
\newcmd*{\match}[2]{\kw{case} \@et #1 \@et \kw{of} \@et \phantom{} #2}
\newcommand{\fix}[4]{\kw{fix} \@et #1 \@et \sqbr{#2} \mathrel{:} #3 \mathrel{\coloneqq} \phantom{} #4}

% source coinductives
\newcmd*{\M}[0]{\const{M}}
\newcmd*{\inf}[0]{\constr{inf}}
\newcommand{\Stream}[2]{\App{\app{\const{Stream}}{#1}}{{#2}}}
\newcmd*{\Stream}[0]{\const{Stream}}
\newcommand{\shd}[1]{#1\mathord{.}\constr{hd}}
\newcommand{\stl}[1]{#1\mathord{.}\constr{tl}}
\newcommand{\scons}[6]{\set{\constr{hd} \mathrel{\coloneqq} #3 \mathpunct{;} \app{\constr{tl}}{[\bound{#4}{#5}]} \mathrel{\coloneqq} #6}}
\newcmd*{\scons}[0]{\constr{scons}}
\newcommand{\cofix}[4]{\kw{cofix} \@et #1 \@et \sqbr{#2} \mathrel{:} #3 \mathrel{\coloneqq} \phantom{} #4}
\newcommand{\Thunk}[2]{\App{\app{\const{Thunk}}{#1}}{#2}}
\newcmd*{\Thunk}[0]{\const{Thunk}}
\newcommand{\force}[1]{#1\mathord{.}\constr{force}}
\newcmd*{\force}[0]{\constr{force}}
\newcommand{\thunk}[3]{\set{\app{\constr{force}}{[\bound{#1}{#2}]} \mathrel{\coloneqq} #3}}

% source names
\newcommand{\liftN}{\const{liftN}}
\newcommand{\liftW}{\const{liftW}}
\newcommand{\liftL}{\const{liftL}}
\newcommand{\liftO}{\const{liftO}}
\newcommand{\monus}{\const{monus}}
\newcommand{\pred}{\const{pred}}
\newcommand{\divv}{\const{div}}
\newcommand{\Nary}{\const{Nary}}
\newcommand{\maX}{\const{max}}
\newcommand{\MaX}{\const{maximum}}
\newcommand{\ifleq}{\const{ifleq}}
\newcommand{\append}{\const{append}}
\newcommand{\mrg}{\const{merge}}
\newcommand{\spt}{\const{split}}
\newcommand{\partition}{\const{partition}}
\newcommand{\qsort}{\const{qsort}}
\newcommand{\msort}{\const{msort}}
\newcommand{\msorted}{\const{msort'}}
\newcommand{\traverseW}{\const{traverseW}}
\newcommand{\natOrd}{\const{natOrd}}
\newcommand{\omegaOrd}{\const{\omega}}
\newcommand{\dup}{\const{repeat}}
\newcommand{\odds}{\const{odds}}
\renewcommand{\interleave}{\const{interleave}}
\newcommand{\zip}{\const{zip}}
\newcommand{\fibs}{\const{fibs}}

% example names
\newcommand{\id}{\mathit{id}}
\newcommand{\Id}{\mathit{Id}}
\newcommand{\hd}{\mathit{hd}}
\newcommand{\tl}{\mathit{tl}}
\newcommand{\lift}{\mathit{lift}}
\newcommand{\nary}[0]{\mathit{nary}}
\newcommand{\traverse}[0]{\mathit{traverse}}
\newcmd*{\monus}[0]{\mathit{monus}}
\newcmd*{\divv}[0]{\mathit{div}}
\newcmd*{\MaX}[0]{\mathit{maximum}}
\newcmd*{\qsort}[0]{\mathit{qsort}}
\newcmd*{\msort}[0]{\mathit{msort}}
\newcmd*{\natOrd}[0]{\mathit{natOrd}}
\newcmd*{\dup}[0]{\mathit{repeat}}
\newcmd*{\odds}[0]{\mathit{odds}}
\newcmd*{\interleave}[0]{\mathit{interleave}}
\newcmd*{\zip}[0]{\mathit{zip}}
\newcmd*{\fibs}[0]{\mathit{fibs}}

% judgements
\newcommand{\wf}[2]{#1 \mathrel{\vdash} #2}
\renewcommand{\check}[3]{#1 \mathrel{\vdash} #2 \mathrel{:} #3}
\renewcommand{\infer}[3]{#1 \mathrel{\vdash} #2 \mathrel{:} #3}
\newcommand{\type}[3]{#1 \mathrel{\vdash} \annot{#2}{#3}}
\newcommand{\defeq}[4]{#1 \mathrel{\vdash} \annot{#2 \mathrel{\equiv} #3}{#4}}
\newcommand{\subsize}[3]{#1 \mathrel{\vdash} #2 \mathrel{\leqslant} #3}
\newcmd*{\subsize}[2]{#1 \mathrel{\leqslant} #2}
\newcommand{\subtype}[3]{#1 \mathrel{\vdash} #2 \mathrel{\preccurlyeq} #3}
\newcommand{\acum}[2]{#1 \mathrel{\sqsubseteq} #2}
\newcommand{\red}[4][]{#2 \mathrel{\vdash} #3 \mathrel{\rhd}_{#1} #4}
\newcmd*{\red}[3]{#1 \mathrel{\vdash} #2 \mathrel{\rhd^*} #3}
\newcommand{\develop}[3]{#1 \mathrel{\vdash} #2 \mathrel{\blacktriangleright} #3}
\newcommand{\subsizeto}[4]{#1 \mathrel{\vdash} #2 \mathrel{\leqslant} #3 \mathrel{\rightsquigarrow} #4}
\newcommand{\wfto}[3]{#1 \mathrel{\vdash} #2 \mathrel{\rightsquigarrow} #3}
\newcommand{\typeto}[4]{#1 \mathrel{\vdash} \annot{#2}{#3} \mathrel{\rightsquigarrow} #4}

% target metavariables
\newcommand{\GammaT}{\tg*{\Gamma}}
\newcommand{\DeltaT}{\tg*{\Delta}}
\newcommand{\iT}{\tg{i}}
\newcommand{\jT}{\tg{j}}
\newcommand{\kT}{\tg{k}}
\newcommand{\mT}{\tg{m}}
\newcommand{\nT}{\tg{n}}
\newcommand{\UT}{\tg{U}}
\newcommand{\DT}{\tg{D}}
\newcommand{\eT}{\tg{e}}
\newcommand{\aT}{\tg{a}}
\newcommand{\bT}{\tg{b}}
\newcommand{\dT}{\tg{d}}
\newcommand{\pT}{\tg{p}}
\newcommand{\PT}{\tg{P}}
\newcommand{\rT}{\tg{r}}
\newcommand{\sT}{\tg{s}}
\newcommand{\alphaT}{\tg*{\alpha}}
\newcommand{\betaT}{\tg*{\beta}}
\newcommand{\gammaT}{\tg*{\gamma}}
\newcommand{\tauT}{\tg*{\tau}}
\newcommand{\sigmaT}{\tg*{\sigma}}
\newcommand{\XT}{\tg{X}}
\newcommand{\cT}{\tg{c}}
\newcommand{\fT}{\tg{f}}
\newcommand{\gT}{\tg{g}}
\newcommand{\wT}{\tg{w}}
\newcommand{\xT}{\tg{x}}
\newcommand{\yT}{\tg{y}}
\newcommand{\zT}{\tg{z}}
\newcommand{\RightarrowT}{\mathrel{\tg{\Rightarrow}}}

% target binders
\newcommand{\annotT}[2]{#1 \mathrel{\tg{:}} #2}
\newcmd*{\annotT}[2]{\mathmbox{#1 \mathrel{\tg{:}} #2}}
\newcommand{\defineT}[3]{#1 \mathrel{\tg{:}} #2 \mathrel{\tg{\coloneqq}} #3}
\newcommand{\boundT}[2]{#1 \mathrel{\tg{<}} #2}

% target language
\newcommand{\PropT}{\tg{Prop}}
\newcommand{\SPropT}{\tg{SProp}}
\newcommand{\TypeT}[1]{\tg{Type}_{#1}}
\newcommand{\sssT}[1]{\tg{\widehat{#1}}}
\newcommand{\funT}[3]{\tg{\lambda} \annotT{#1}{#2} \mathpunct{\tg{.}} #3}
\newcmd*{\funT}[3]{\tg{\lambda} #1 \mathord{\tg{.}} #2 \mathpunct{\tg{.}} #3}
\newcommand{\funtypeT}[3]{\tg*{\Pi} \annotT{#1}{#2} \mathpunct{\tg{.}} #3}
\newcommand{\arrT}[3]{\mathopen{\tg{(}} \annotT{#1}{#2} \mathclose{\tg{)}} \mathrel{\tg{\rightarrow}} \phantom{} #3}
\newcmd*{\arrT}[1]{#1\@ifnextchar\bgroup{\mathrel{\tg{\rightarrow}}\arr*}{\xspace}}
\newcommand{\letinT}[4]{\tg{let} \@et #1 \mathrel{\tg{:}} #2 \mathrel{\tg{\coloneqq}} \phantom{} #3 \@et \tg{in} \@et #4}
\newcommand{\LetT}[3]{\tg{let} \@et \annotT{#1}{#2} \mathrel{\tg{\coloneqq}} \phantom{} #3}
\newcommand{\eqT}[3]{#1 \stackrel{#2}{\tg{=\joinrel=}} #3}
\newcommand{\reflT}[1]{\tg{refl}_{#1}}
\newcommand{\JT}[3]{\tg{J} \@et {#1} \@et #2 \@et #3}
\newcmd*{\JT}[0]{\tg{J}}
\newcommand{\inftyT}{\tg{\infty}}

% target inductives
\newcommand{\dataT}[2]{\tg{data} \@et \annotT{#1}{#2} \@et \tg{where}}
\newcommand{\matchT}[3]{\tg{case} \@et #1 \@et \tg{return} \@et #2 \@et \tg{of} \@et \phantom{} #3}
\newcmd*{\matchT}[2]{\tg{case} \@et #1 \@et \tg{of} \@et \phantom{} #2}
\newcommand{\fixT}[4]{\tg{fix}_{#1} \@et #2 \mathrel{\tg{:}} #3 \mathrel{\tg{\coloneqq}} \phantom{} #4}
\newcommand{\botT}{\tg{\bot}}
\newcommand{\SizeT}{\tg{Size}}
\newcommand{\SizeUnivT}{\tg{SizeUniv}}
\newcommand{\baseT}{\tg{base}}
\newcommand{\sucT}{\tg{suc}}
\newcommand{\limT}{\tg{lim}}
\newcommand{\szleT}{\mathbin{\tg{\le}}}
\newcommand{\szltT}{\mathbin{\tg{<}}}
\newcommand{\monoT}{\tg{mono}}
\newcommand{\coconeT}{\tg{cocone}}
\newcommand{\limitT}{\tg{limiting}}
\newcommand{\AccT}{\tg{Acc}}
\newcommand{\accT}{\tg{acc}}
\newcommand{\NatT}{\tg{Nat}}
\newcommand{\zeroT}{\tg{zero}}
\newcommand{\succT}{\tg{succ}}
\newcommand{\WT}{\tg{W}}
\newcommand{\supT}{\tg{sup}}

% target names
\newcommand{\baseleq}{\tg{base\mathord{\le}}}
\newcommand{\reflleq}{\tg{refl\mathord{\le}}}
\newcommand{\sucleq}{\tg{suc\mathord{\le}}}
\newcommand{\transleq}{\tg{trans\mathord{\le}}}
\newcommand{\funext}{\tg{funext}}
\newcommand{\accIsProp}{\tg{accIsProp}}
\newcommand{\accleq}{\tg{acc\mathord{\le}}}
\newcommand{\accessible}{\tg{wf}}
\newcommand{\access}{\tg{access}}
\newcommand{\wfacc}{\tg{wfAcc}}
\newcommand{\wfind}{\tg{wfInd}}
\newcommand{\inftyltinfty}{\tg{\infty\text{<}\infty}}
\newcmd*{\wfacc}[0]{\tg{wfAcc'}}