notations.tex

% \usepackage{hyperref}
\usepackage{anyfontsize} % kill warnings about font sizes
\usepackage{amsmath}     % Mathematics FTW!
% \usepackage[capitalise]{cleveref}
\usepackage{amsthm}      % Warning, I've only proven it correct :).
% %\usepackage{amssymb}     % needed for \mathbb and mathcal
% %\usepackage{bbm}
% \usepackage[english]{babel}
% %\usepackage{amsbsy}      % for \boldsymbol
\usepackage{stmaryrd}   % provides some PLy symbols, like Scott Brackets
\usepackage{mathpartir}  % for \mathpar
% \usepackage{color}
% \usepackage{braket}      % for \set and \braket
% \usepackage{mathtools}   % for \bigtimes
% \usepackage{thmtools}    % to duplicate theorems in the appendix
% %\usepackage{marvosym} % for deniarius (gradual label)
% %\usepackage{wasysym}     % for \smiley
% %\usepackage{balance}     % for the references
% \usepackage{xspace}
% %\usepackage{mathrsfs} % for mathscr font
% \usepackage{proof}
% % \usepackage{yhmath}
% \usepackage{rotating}
% \usepackage{tikz-cd}
% \usepackage{xcolor}
% \usepackage{changepage}
% \usepackage{centernot}
\usepackage{comment}
% \usepackage{listings}
% \usepackage{mdframed}
% \usepackage{centernot}
% \usepackage{mathtools}
% \usepackage{multirow}
\usepackage{xparse}
% \definecolor{darkblue}{rgb}{0.0, 0.0, 0.55}
% \definecolor{darkgreen}{rgb}{0.0, 0.55, 0.13}
% \definecolor{darkred}{rgb}{0.55, 0.0, 0.0}
% \definecolor{darkviolet}{rgb}{0.58, 0.0, 0.83}
% \definecolor{lightblue}{rgb}{0.68, 0.85, 0.9}
% \usepackage{lstcoq}
% % Literate Agda
\usepackage{agda}
% \usepackage[all]{xy}
% \usepackage{subcaption,verbatim}
\usepackage{agda-syntax}
% \usepackage[utf8x]{inputenc}
% \usepackage[outline]{contour}
\usepackage{catchfilebetweentags}
\usepackage{tikz}
\usetikzlibrary{arrows,matrix,decorations.pathmorphing,
  decorations.markings, calc, backgrounds}
\usepackage{tikz-cd}
\usepackage{floatrow}
\usepackage{cancel}
\usepackage{newunicodechar}

\DeclareMathAlphabet{\mathbbm}{U}{bbm}{m}{n}

\makeatletter
\@ifpackageloaded{stix}{%
}{%
  \DeclareFontEncoding{LS2}{}{\noaccents@}
  \DeclareFontSubstitution{LS2}{stix}{m}{n}
  \DeclareSymbolFont{stix@largesymbols}{LS2}{stixex}{m}{n}
  \SetSymbolFont{stix@largesymbols}{bold}{LS2}{stixex}{b}{n}
  \DeclareMathDelimiter{\lBrace}{\mathopen} {stix@largesymbols}{"E8}%
                                            {stix@largesymbols}{"0E}
  \DeclareMathDelimiter{\rBrace}{\mathclose}{stix@largesymbols}{"E9}%
                                            {stix@largesymbols}{"0F}
}
\makeatother
%% \DeclareMathAlphabet{\mathcal}{OMS}{cmsy}{m}{n} % Reset mathcal font because ACM version sucks

% text
% \newcommand{\ie}{\emph{i.e.,}\xspace}
% \newcommand{\etal}{\emph{
%     et al.}\xspace}
% \newcommand{\eg}{\emph{e.g.,}\xspace}

% LaTeX references

\newcommand{\myref}[2]{\hyperref[#2]{#1~\ref*{#2}}}
\newcommand{\figref}[1]{\myref{Fig.}{fig:#1}}
\newcommand{\secref}[1]{\myref{Sect.}{sec:#1}}
\newcommand{\defref}[1]{\myref{Definition}{def:#1}}
\newcommand{\lemref}[1]{\myref{Lemma}{lem:#1}}
\newcommand{\thmref}[1]{\myref{Theorem}{thm:#1}}
\newcommand{\eqnref}[1]{\hyperref[#1]{(\ref{#1})}}
\newcommand{\exref}[1]{\myref{Example}{ex:#1}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%Reference to inference rules, inspired by https://tex.stackexchange.com/questions/340788/cross-referencing-inference-rules

\makeatletter
\let\originferrule\inferrule
\DeclareDocumentCommand \inferrule { s O {} m m }{%
	\IfBooleanTF{#1}%
	{%
		\mpr@inferstar[#2]{#3}{#4}%
	}{%
		\mpr@inferrule[#2]{#3}{#4}%
	}%
  % Modification of the SO code: we reuse the main label
	\IfValueT{#2}%
	{%
		\my@name@inferrule{#2}%
	}%
}
\NewDocumentCommand \my@name@inferrule { m }{%
	\def\@currentlabelname{\textsc{#1}}%
}

% inference rules or something
\newcommand{\mathsc}[1]{\ensuremath{\textsc{#1}}}
\newcommand{\rulename}[1]{{\footnotesize\mathsc{#1}}}
\newcommand{\nru}[3]{\dfrac{\begin{array}{@{}c@{}}#1\end{array}}{\begin{array}{@{}c@{}}#2\end{array}}\ifthenelse{\isempty{#3}}{}{\ \rulename{#3}}}
\newcommand{\ru}[2]{\nru{#1}{#2}{}}

\newcommand*{\ilabel}[1]{%
  % \edef\@currentlabel{#1}% Set target label
  \phantomsection% Correct hyper reference link
  \label{#1}% Print and store label
}
\makeatother


% Type Theories

\newcommand{\CIC}{\ensuremath{\mathsf{pCIC}}\xspace}
\newcommand{\MLTT}{\ensuremath{\mathsf{MLTT}}\xspace}
\newcommand{\MLTTW}{\ensuremath{\mathsf{MLTT}^\mathsf{ind}}\xspace}
\newcommand{\sMLTT}{\ensuremath{\mathsf{sMLTT}}\xspace}
\newcommand{\ETT}{\ensuremath{\mathsf{ETT}}\xspace}
\newcommand{\HTS}{\ensuremath{\mathsf{HTS}}\xspace}
\newcommand{\HoTT}{\ensuremath{\mathsf{HoTT}}\xspace}
\newcommand{\HoTTminus}{\ensuremath{\mathsf{HoTT}^\mathrm{pf}}\xspace}
\newcommand{\SetoidTT}{\ensuremath{\mathsf{TT}^\mathrm{obs}}\xspace}
\newcommand{\SetoidCC}{\ensuremath{\mathsf{CC}^\mathrm{obs}}\xspace}
\newcommand{\SetoidCCtitle}{{\textsf{CC}\textsuperscript{obs}}}
\newcommand{\SetoidCCW}{\ensuremath{\mathsf{CC}^\mathrm{obs}}\xspace}
\newcommand{\SetoidCCplus}{\ensuremath{\mathsf{CC}^\mathrm{obs+}}\xspace}

% Properties of type theories

\newcommand{\UIP}{${\mathrm{UIP}}$\xspace}

% Proof assistants

\def\Coq{\textsc{Coq}\xspace}
\def\Agda{\textsc{Agda}\xspace}
\def\CubicalAgda{\textsc{Cubical} \textsc{Agda}\xspace}
\def\Lean{\textsc{Lean}\xspace}
\def\Idris{\textsc{Idris}\xspace}
\def\cubicaltt{\textsc{cubicaltt}\xspace}





% BNF grammars

\newcommand{\bnfis}{::=}
\newcommand{\bnfin}{\in}
\newcommand{\sep}{|}
\newcommand{\qsep}{\ | \ }





% terms of pCIC

%% Meta-theoretical classification

\newcommand\head[1]{\mathop{\text{hd}}#1}
\newcommand\whnf[1]{\mathop{\text{whnf}}#1}
\newcommand\neutral[1]{\mathop{\text{neutral}} #1}

%% PTS style relations

\newcommand{\piRel}[2]{\mathcal{R} ( #1 , #2)}
\newcommand{\univRel}[2]{\mathcal{A} ( #1 , #2)}

%% Universes

\newcommand{\Prop}{\mathbb{P}}
\newcommand{\varProp}{\mathsf{Prop}}
\newcommand{\sProp}{\Omega}
\newcommand{\varsProp}{\mathsf{sProp}}
\newcommand{\hProp}{\oblset{hProp}}

\newcommand{\Type}{\mathcal{U}}
\newcommand{\varType}{\mathsf{Type}}
\newcommand{\varSet}{\mathsf{Set}}

\newcommand{\Univ}{\mathfrak{s}}

%% Functions 

\newcommand{\Depfun}[3][x]{\Pi (\tm{#1}{#2}).\, {#3}}
\newcommand{\Fun}[2]{{#1} \to {#2}}
\newcommand{\lam}[3][x]{\lambda (\tm{#1}{#2}).\, #3}

%% Proof-relevant Datatypes
\newcommand\metaop[1]{{\color{RoyalBlue}{\mathsf{#1}}}}

\newcommand{\Nat}{\mathbb{N}}
\newcommand{\Natprop}{\mathbb{N}_{\mathsf{p}}}
\newcommand{\zero}{\metaop{0}}
\newcommand{\sucName}{\metaop{S}}
\newcommand{\suc}[1]{\sucName\ #1}
\newcommand{\natrec}[4]{{\color{RoyalBlue}\Nat} \metaop{-elim}({#1},{#2},{#3},{#4})}

\newcommand{\Bool}{\mathsf{Bool}}

\newcommand{\Acc}{\metaop{Acc}}
\newcommand{\accintro}{\metaop{Acc{-}intro}}
\newcommand{\accelim}{\metaop{Acc{-}elim}}

\newcommand{\Depsum}[3][x]{\Sigma (\tm{#1}{#2}).\, {#3}}
\newcommand{\Sig}[3][x]{\Sigma (\tm{#1}{#2}).\, {#3}}
\newcommand{\relpair}[2]{\langle #1\ {;}\ #2 \rangle }
\newcommand{\relfst}[1]{\metaop{proj}_{\metaop{1}}({#1})}
\newcommand{\relsnd}[1]{\metaop{proj}_{\metaop{2}}({#1})}

\newcommand{\Subtype}[3][x]{\{ (\tm{#1}{#2}) \ |\ {#3} \}}

\newcommand{\Quo}[2]{{#1}/{#2}}
\newcommand{\quo}[1]{\pi(#1)}
\newcommand{\quorec}[4]{\metaop{Q\mathsf{-}elim}(#1,#2,#3,#4)}

\newcommand{\Id}[3]{\metaop{Id}(#1,#2,#3)}
\newcommand{\id}[1]{\metaop{Idrefl}(#1)}
\newcommand{\idpath}[1]{\metaop{Idpath}(#1)}
\newcommand{\J}[6]{\metaop{J}(#1,#2,#3,#4,#5,#6)}
\newcommand{\eqJ}[5]{\metaop{eq_J}(#1,#2,#3,#4,#5)}

\newcommand{\Indeq}[3]{{#2 =_{#1} #3}}
\newcommand{\indrefl}[1]{\mathsf{refl}_{#1}}
\newcommand{\indJ}[6]{\mathsf{J}(#1,#2,#3,#4,#5,#6)}

\newcommand{\Boxt}[1]{\square{#1}}
\newcommand{\boxt}[1]{\diamond{#1}}
\newcommand{\unboxt}[1]{\metaop{\Box\mathsf{-elim}}(#1)}

%% Proof-irrelevant Datatypes

\newcommand{\Prod}[2]{{#1} \land {#2}}

\newcommand{\Exists}[3][x]{(\tm{#1}{#2})\ \&\ {#3}}
\newcommand{\ExistsUnique}[3][x]{\exists ! (\tm{#1}{#2}).\, {#3}}
\newcommand{\varExists}[3][x]{\exists (\tm{#1}{#2}).\, {#3}}
\newcommand{\pair}[2]{\langle #1 , #2 \rangle }
\newcommand{\fst}[1]{\metaop{fst}({#1})}
\newcommand{\snd}[1]{\metaop{snd}({#1})}

\newcommand{\Obseq}[3][]{#2 \sim_{#1} #3}
\newcommand{\Heteq}[4]{#1~{{}_{#2}\!\!\sim_{#4}}~#3}
\newcommand{\refl}[2]{\metaop{refl}(#1)}
\newcommand{\sym}[1]{{#1}^{-1}}
\newcommand{\transitivity}[2]{{#1}\cdot{#2}}
\newcommand{\ap}[2]{\metaop{ap}~{#1}~{#2}}
\newcommand{\castName}{\metaop{cast}}
\newcommand{\cast}[4]{\castName(#1,#2,#3,#4)}
\newcommand{\transportName}{\metaop{transp}}
\newcommand{\transport}[6]{\transportName(#1,#2,#3,#4,#5,#6)}
\newcommand{\hettransport}[7]{\transportName(#1,#2,#3,#4,#6,#7)}
\newcommand{\castreflName}{\metaop{castrefl}}
\newcommand{\castrefl}[2]{\castreflName(#1,#2)}

\newcommand{\Empty}{\bot}
\newcommand{\Emptyprop}{\bot_{\mathsf{p}}}
\newcommand{\emptyrec}[2]{{\color{RoyalBlue}\bot}\metaop{-elim}({#1}, {#2})}
\newcommand{\emptyrecName}{{\color{RoyalBlue}\bot}\metaop{-elim}}

\newcommand{\Unit}{\top}
\newcommand{\unit}{*}

\newcommand{\Squash}[1]{\| #1 \|}
\newcommand{\squash}[1]{| #1 |}
\newcommand{\unsquash}[3]{\metaop{\mathsf{S}\mathsf{-elim}}(#1,#2,#3)}

\newcommand{\CubicalPath}{\metaop{Path}}

%% Contexts of pCIC

\newcommand{\emptyctx}{\bullet}
\newcommand{\extctx}[3][x]{#2 , \tm{#1}{#3}}
\newcommand{\inctx}[4][x]{\tmannotated{#1}{#3}{#4}{} \in {#2}}


%% Judgments of pCIC

\newcommand{\subst}[3][x]{#2[{#1}:={#3}]}

\newcommand\dashPar{\vdash_{p}}
\newcommand\dashEco{\vdash_{e}}

\newcommand{\wfctx}[2][]{#1 \vdash #2}
\newcommand{\tyty}[3][]{#1 #2 \vdash #3}
\newcommand{\tytm}[4][]{#1 #2 \vdash #3 : #4}
\newcommand{\tytmPara}[4][]{#1 #2 \dashPar #3 : #4}
\newcommand{\tytmEco}[4][]{#1 #2 \dashEco #3 : #4}
\newcommand{\tm}[2]{#1 : #2}
\newcommand{\tytms}{\tytm}
% \newcommand{\eqeq}[2]{#1 \equiv abd #2}
\newcommand{\eqtm}[5][]{#1 #2 \vdash #3 \equiv #4 : #5}
\newcommand{\red}[5][]{#1 #2 \vdash #3 \Rightarrow #4 : #5}
\newcommand{\redT}[5][]{#1 #2 \vdash #3 \Rightarrow^* #4 : #5}
\newcommand{\eqtmmultiline}[5][]{#1 #2 \vdash \begin{array}{l} #3 \equiv \\ #4 \end{array} : #5}
\newcommand{\redmultiline}[5][]{#1 #2 \vdash \begin{array}{l} #3 \Rightarrow \\ #4 \end{array} : #5}
\newcommand{\redmultilineExt}[6][]{#1 #2 \vdash \begin{array}{l} #3 \Rightarrow \\ #4 \\ #5 \end{array} : #6}

%% With some annotations?

\newcommand{\tmannotated}[3]{#1 : #2 : #3}%{#1 :^{#3} #2}
\newcommand{\extctxannotated}[4][x]{#2 , \tmannotated{#1}{#3}{#4}{}}
\newcommand{\tytmannotated}[5][]{#1 #2 \vdash \tmannotated{#3}{#4}{#5}}
\newcommand{\tytmParaannotated}[5][]{#1 #2 \dashPar \tmannotated{#3}{#4}{#5}}
\newcommand{\tytmEcoannotated}[5][]{#1 #2 \dashEco \tmannotated{#3}{#4}{#5}}
\newcommand{\eqtmannotated}[6][]{#1 #2 \vdash #3 \equiv #4 : #5 : #6}
\newcommand{\algoeqtmannotated}[6][]{#1 #2 \vdash #3 \cong #4 : #5 : #6}
\newcommand{\eqtmParaannotated}[6][]{#1 #2 \dashPar #3 \equiv #4 : #5 : #6}
\newcommand{\eqtmEcoannotated}[6][]{#1 #2 \dashEco #3 \equiv #4 : #5 : #6}
\newcommand{\redannotated}[6][]{#1 #2 \vdash #3 \Rightarrow #4 : #5 : #6}
\newcommand{\Depfunannotated}[6][x]{\Pi_{}^{#5, #6} (\tm{#1}{#2}).\, {#3}}
\newcommand{\Depsumannotated}[6][x]{\Sigma_{}^{#5, #6} (\tm{#1}{#2}).\, {#3}}
\newcommand{\Existsannotated}[5][x]{\exists (\tm{#1}{#2}).\, {#3}}
\newcommand{\castannotated}[5]{\mathsf{cast}^{#5}(#1,#2,#3,#4)}





% Reducibility model

\newcommand{\Context}{\AgdaData{Context}}
\newcommand{\Term}{\AgdaData{Term}}
\newcommand{\Sort}{\AgdaData{Sort}}

\newcommand{\VU}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\AgdaCon{U}}}
\newcommand{\VOmega}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\textcolor{AgdaInductiveConstructor} \Omega}}
\newcommand{\Vempty}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\textcolor{AgdaInductiveConstructor} \bot}}
\newcommand{\Vpi}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\textcolor{AgdaInductiveConstructor} \Pi}}
\newcommand{\Vsigma}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\textcolor{AgdaInductiveConstructor} \Sigma}}
\newcommand{\Vbox}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\textcolor{AgdaInductiveConstructor} \Box}}
\newcommand{\Vforall}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\textcolor{AgdaInductiveConstructor} \Pi \mathsf{\textcolor{AgdaInductiveConstructor} i}}}
\newcommand{\Vexists}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\textcolor{AgdaInductiveConstructor} \exists}}
\newcommand{\Vnat}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\AgdaCon{N}}}
\newcommand{\Vne}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\AgdaCon{ne}}}
\newcommand{\Vquo}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\AgdaCon{Q}}}
\newcommand{\Vid}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\AgdaCon{Id}}}
\newcommand{\Vemb}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\AgdaCon{emb}}}
\newcommand{\VX}{{\textcolor{AgdaInductiveConstructor} \Vdash}_{\AgdaCon{X}}}

\newcommand{\RU}{\AgdaCon{R}_{\AgdaCon{U}}}
\newcommand{\ROmega}{\AgdaCon{R}_{\textcolor{AgdaInductiveConstructor} \Omega}}
\newcommand{\Rempty}{\AgdaCon{R}_{\textcolor{AgdaInductiveConstructor} \bot}}
\newcommand{\Rpi}{\AgdaCon{R}_{\textcolor{AgdaInductiveConstructor} \Pi}}
\newcommand{\Rsigma}{\AgdaCon{R}_{\textcolor{AgdaInductiveConstructor} \Sigma}}
\newcommand{\Rbox}{\AgdaCon{R}_{\textcolor{AgdaInductiveConstructor} \Box}}
\newcommand{\Rforall}{\AgdaCon{R}_{\textcolor{AgdaInductiveConstructor} \Pi \mathsf{\textcolor{AgdaInductiveConstructor} i}}}
\newcommand{\Rexists}{\AgdaCon{R}_{\textcolor{AgdaInductiveConstructor} \exists}}
\newcommand{\Rnat}{\AgdaCon{R}_{\AgdaCon{N}}}
\newcommand{\RW}{\AgdaCon{R}_{\AgdaCon{W}}}
\newcommand{\Rquo}{\AgdaCon{R}_{\AgdaCon{Q}}}
\newcommand{\Rid}{\AgdaCon{R}_{\AgdaCon{Id}}}
\newcommand{\Rne}{\AgdaCon{R}_{\AgdaCon{ne}}}
\newcommand{\Remb}{\AgdaCon{R}_{\AgdaCon{emb}}}

\newcommand{\tytyR}[4]{#2 \Vdash_{#1} #3 : #4}
\newcommand{\tytmR}[5]{#2 \Vdash_{#1} #3 : #4 : #5}
\newcommand{\eqtmR}[6]{#2 \Vdash_{#1} #3 \equiv #4 : #5 : #6}
\newcommand{\eqtyR}[5]{#2 \Vdash_{#1} #3 \equiv #4 : #5}

\newcommand{\tytyReco}[4]{#2 \Vdash_{#1} #3}
\newcommand{\tytmReco}[5]{#2 \Vdash_{#1} #3 : #4}
\newcommand{\eqtmReco}[6]{#2 \Vdash_{#1} #3 \equiv #4 : #5}
\newcommand{\eqtyReco}[5]{#2 \Vdash_{#1} #3 \equiv #4}

\newcommand{\nattmR}[2]{#1 \Vdash_{\mathbb{N}\mathsf{t}}\ {#2}}
\newcommand{\nateqR}[3]{#1 \Vdash_{\mathbb{N}\mathsf{t}=}\ {#2} \equiv {#3}}
\newcommand{\quotmR}[2]{#1 \Vdash_{\mathsf{Q}\mathsf{t}}\ {#2}}
\newcommand{\quoeqR}[3]{#1 \Vdash_{\mathsf{Q}\mathsf{t}=}\ {#2} \equiv {#3}}
\newcommand{\boxtmR}[2]{#1 \Vdash_{\Box\mathsf{t}}\ {#2}}
\newcommand{\boxeqR}[3]{#1 \Vdash_{\Box\mathsf{t}=}\ {#2} \equiv {#3}}
\newcommand{\idtmR}[2]{#1 \Vdash_{\mathsf{Id}\mathsf{t}}\ {#2}}
\newcommand{\ideqR}[3]{#1 \Vdash_{\mathsf{Id}\mathsf{t}=}\ {#2} \equiv {#3}}

\newcommand{\ctxV}[1]{{\Vdash^v #1}}
\newcommand{\tytyV}[4]{#2 \Vdash^v_{#1} #3 : #4}
\newcommand{\tytmV}[5]{#2 \Vdash^v_{#1} #3 : #4 : #5}
\newcommand{\eqtyV}[5]{#2 \Vdash^v_{#1} #3 \equiv #4 : #5}
\newcommand{\eqtmV}[6]{#2 \Vdash^v_{#1} #3 \equiv #4 : #5 : #6}
\newcommand{\substV}[3]{#1 \Vdash^s #2 : #3}
\newcommand{\eqsubstV}[4]{#1 \Vdash^s #2 \equiv #3 : #4}

\newcommand{\emptyctxV}{{\textcolor{AgdaInductiveConstructor} \varepsilon}}
\newcommand{\extctxVname}{\textcolor{AgdaInductiveConstructor}{\_ , \_ }}

\newcommand{\tytyS}[3]{#1 \Vdash #2 : #3}
\newcommand{\eqtyS}[4]{#1 \Vdash #2 \equiv #3 : #4}
\newcommand{\wk}[3]{{#1}}% : {#2} \le {#3}}
\newcommand{\wkrho}{(\rho : \Delta ⊑ \Gamma)}





% Set theoretic model

%% Set theoretic universe

\newcommand{\codeemb}{\mathsf{c}_\mathsf{emb}}
\newcommand{\codenat}{\mathsf{c}_\mathsf{N}}
\newcommand{\codepi}{\mathsf{c}_{\Pi}}
\newcommand{\codepiuu}{\mathsf{c}_{\Pi\mathsf{UU}}}
\newcommand{\codepisu}{\mathsf{c}_{\Pi\Omega\mathsf{U}}}
\newcommand{\codepius}{\mathsf{c}_{\Pi\mathsf{U}\Omega}}
\newcommand{\codepiss}{\mathsf{c}_{\Pi\Omega\Omega}}
\newcommand{\codesigma}{\mathsf{c}_{\Sigma}}
\newcommand{\codebox}{\mathsf{c}_{\Box}}
\newcommand{\codequo}{\mathsf{c}_\mathsf{Q}}
\newcommand{\codeid}{\mathsf{c}_\mathsf{Id}}
\newcommand{\codeex}{\mathsf{c}_{\exists}}
\newcommand{\codeU}{\mathsf{c}_\mathsf{U}}
\newcommand{\codesProp}{\mathsf{c}_{\sProp}}
\newcommand{\codeempty}{\mathsf{c}_\bot}


\newcommand{\Setoid}{\mathsf{Setoid}}
\newcommand{\metasProp}{\mathsf{Prop}}
\newcommand{\metanat}{\mathsf{N}}
\newcommand{\metazero}{0}
\newcommand{\metasuc}[1]{\mathsf{S}\ #1}
\newcommand{\metaempty}{\bot}
\newcommand{\metaunit}{\top}
\newcommand{\metarefl}{\mathsf{refl}}

% kinda stupid, might remove?
\newcommand{\metatm}[2]{{#1} :: {#2}}
\newcommand{\metaforall}[2]{\forall {#1},\ {#2}}
\newcommand{\metaimply}[2]{{#1}\ \to\ {#2}}




% Setoid model ??

\newcommand{\mctx}[1]{\llbracket #1 \rrbracket}
\newcommand{\mty}[2][\Gamma]{\llbracket {#2} \rrbracket_{#1}}
\newcommand{\mtm}[3][\Gamma]{[\tm{#2}{#3}]_{#1}}

\newcommand{\Con}{\mathsf{Con}}
\newcommand{\cwfty}[1][]{\mathsf{Ty}_{#1}}
\newcommand{\cwftm}[1][]{\mathsf{tm}_{#1}}
\newcommand{\cwfprop}[1][]{\mathsf{Pr}_{#1}}
\newcommand{\cwfpr}[1][]{\mathsf{pr}_{#1}}

\renewcommand{\ne}{N}
\newcommand{\neu}{N}

\newcommand{\sV}{\mathbf{V}}
\newcommand{\sU}{\mathbf{U}}
\newcommand{\Upred}{\mathbf{U}^{\varepsilon}}
\newcommand{\sType}{\mathbf{s}}
\newcommand{\ssProp}{\Two}
\newcommand{\sFun}[2]{#1 \to_s #2}
\newcommand{\sEq}[2]{#1 = #2}
\newcommand{\el}{\mathsf{el}}
\newcommand{\eleq}{\mathsf{el\text{-}eq}}
\newcommand{\val}{\mathsf{val}}
\newcommand{\valeq}{\mathsf{val\text{-}eq}}


% Category Theory

\newcommand{\cat}[1]{\mathcal{#1}}
\newcommand{\catCat}{\mathrm{Cat}}
\newcommand{\catSet}{\mathrm{Set}}
\newcommand{\catPsh}[1]{\mathrm{Psh}(#1)}
\newcommand{\catsPsh}[1]{\mathrm{sPsh}(#1)}
\newcommand{\catCube}{\square}

\newcommand{\op}[1]{{#1}^{\mathrm{op}}}
\newcommand{\yo}{\textjapanesefont よ}
\renewcommand{\hom}[3][]{\mathrm{Hom}_{#1}(#2, #3)}
\newcommand{\obj}[1]{\mathrm{Obj}(#1)}


% De Morgan Cubes

\newcommand{\izero}{i_0}
\newcommand{\ione}{i_1}
\newcommand{\interval}{\mathbb{I}}
\newcommand{\demorgan}[1]{\mathrm{dM}(#1)}
\newcommand{\horn}{\sqcap}
\newcommand{\faces}{\mathbb{F}}


% unsure

% Automatically insert parentheses
\newcommand{\maybeparens}[2]{%
  \ifthenelse{\isempty{#2}}{#1}{%  if argument is empty
  \ifthenelse{\equal{#2}{(}}{#1#2}{%  or (, then do not parenthesize
  #1(#2)}}} % otherwise, parenthesize
\newcommand{\tdom}{\mathrm{dom}}
\newcommand{\dom}{\maybeparens{\tdom}}
\newcommand{\tPV}{\mathrm{PV}}
\newcommand{\PV}{\maybeparens{\tPV}}
\newcommand{\tFV}{\mathrm{FV}}
\newcommand{\FV}{\maybeparens{\tFV}}

\newcommand{\joinsub}{\uplus}%{\|}
\newcommand{\Joinsub}{\biguplus}%{\|}

\newcommand{\bbfamily}{\fontencoding{U}\fontfamily{bbold}\selectfont}
\DeclareMathAlphabet{\mathbbold}{U}{bbold}{m}{n}
\newcommand{\Two}{\mathbb{B}}
%% \newcommand{\Two}{{\color{white}\contour{black}{$\Omega$}}}
%% \newcommand{\Two}{\mathbbm{\Omega}}
\newcommand\independent{\protect\mathpalette{\protect\independenT}{\perp}}
\def\independenT#1#2{\mathrel{\rlap{$#1#2$}\mkern2mu{#1#2}}}

% \newcommand{\agdahtml}{https://htmlpreview.github.io/?https://raw.githubusercontent.com/CoqHott/logrel-mltt/impredicativity-SProp-POPL/html}
\newcommand{\agdahtml}{https://htmlpreview.github.io/?https://raw.githubusercontent.com/CoqHott/logrel-mltt/impredicativity-SProp-POPL/html}
\newcommand{\refAgdaRoot}[1]{{\small{\href{\agdahtml/#1.html}{\emph{[#1.agda]}}}}}
\newcommand{\refAgda}[2]{{\small{\href{\agdahtml/Definition.#1#2.html}{\emph{[#2.agda]}}}}}
\newcommand{\refCoq}[1]{{\color{darkblue}\emph{[#1]}}}
% \newcommand{\vrefCoq}[2]{\href{https://github.com/TheoWinterhalter/template-coq/tree/rewrite-rules/pcuic/theories/#1}{\emph{[#2]}}}
\newcommand{\vrefCoq}[2]{\href{https://github.com/TheoWinterhalter/template-coq/tree/popl21-artifact/pcuic/theories/#1}{\emph{[#2]}}}



\newcommand{\shepherd}[1]{{\color{red} #1}}


\newunicodechar{≃}{\ensuremath{\simeq}}