\newcommand{\blank}{\mathord{\hspace{1pt}\text{--}\hspace{1pt}}} %from the book
\newcommand{\Set}{\mathsf{Set}}
\newcommand{\Type}{\mathsf{Type}}
\newcommand{\Id}{\mathsf{Id}}
\newcommand{\refl}{\mathsf{refl}}
\newcommand{\ra}{\rightarrow}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\sProp}{\mathsf{sProp}}
\newcommand{\hProp}{\mathsf{hProp}}
\newcommand{\pfProp}{\mathsf{pfProp}}
\newcommand{\pfPropd}{\mathsf{pfPropd}}
\newcommand{\isHProp}{\mathsf{isHProp}}
\newcommand{\isHPropd}{\mathsf{isHPropd}}
\newcommand{\isPfProp}{\mathsf{isPfProp}}
\newcommand{\isExtPfProp}{\mathsf{isExtPfProp}}
\newcommand{\isPfPropd}{\mathsf{isPfPropd}}
\newcommand{\N}{\mathbb{N}}
\newcommand{\ap}{\mathsf{ap}}
\newcommand{\transp}{\mathsf{transp}}
\newcommand{\elim}{\mathsf{elim}}
\newcommand{\Bool}{\mathsf{Bool}}
\newcommand{\true}{\mathsf{true}}
\newcommand{\false}{\mathsf{false}}
\newcommand{\Nat}{\mathsf{Nat}}
\newcommand{\Con}{\mathsf{Con}}
\newcommand{\Sub}{\mathsf{Sub}}
\newcommand{\Ty}{\mathsf{Ty}}
\newcommand{\Tm}{\mathsf{Tm}}
\newcommand{\con}{\mathsf{con}}
\newcommand{\sub}{\mathsf{sub}}
\newcommand{\ty}{\mathsf{ty}}
\newcommand{\lam}{\mathsf{lam}}
\newcommand{\app}{\mathsf{app}}
\newcommand{\p}{\mathsf{p}}
\newcommand{\q}{\mathsf{q}}
\newcommand{\proj}{\mathsf{proj}}
\newcommand{\id}{\mathsf{id}}
\renewcommand{\tt}{\mathsf{tt}}
\newcommand{\TyP}{\mathsf{TyP}}
\renewcommand{\P}{\mathsf{P}}
\makeatletter
\DeclareRobustCommand{\sqcdot}{\mathbin{\mathpalette\morphic@sqcdot\relax}}
\newcommand{\morphic@sqcdot}[2]{%
  \sbox\z@{$\m@th#1\centerdot$}%
  \ht\z@=.33333\ht\z@
  \vcenter{\box\z@}%
}
\makeatother
\newcommand{\J}{\mathsf{J}}
% \newcommand{\ab}{{a\hspace{-0.12em}b}}
\newcommand{\ab}{\ensurestackMath{\stackengine{0pt}{a\hspace{0.35em}}{\hspace{0.35em}b}{O}{c}{F}{F}{L}}}
% \newcommand{\da}{{d\hspace{-0.12em}a}}
\newcommand{\da}{\ensurestackMath{\stackengine{0pt}{d\hspace{0.35em}}{\hspace{0.4em}a}{O}{c}{F}{F}{L}}}
% \newcommand{\gammaa}{{\gamma\hspace{-0.15em}a}}
\newcommand{\gammaa}{\ensurestackMath{\stackengine{0pt}{\gamma\hspace{0.35em}}{\hspace{0.4em}a}{O}{c}{F}{T}{L}}}
\renewcommand{\v}{\mathsf{v}}
\newcommand{\irr}{\mathsf{irr}}
\newcommand{\oldapp}{\mathbin{\$}}
\newcommand{\RR}{\mathsf{R}}
\renewcommand{\SS}{\mathsf{S}}
\newcommand{\TT}{\mathsf{T}}
\newcommand{\coe}{\mathsf{coe}}
\newcommand{\coh}{\mathsf{coh}}
\newcommand{\U}{\mathsf{U}}
\newcommand{\El}{\mathsf{El}}
\newcommand{\Nf}{\mathsf{Nf}}