paper: macro cleanup, NFC

paper/paper.tex

@@ -163,9 +163,6 @@
   \captionof{table}{#1}
 }
 
-% The label, since we're including twice
-\newcommand*{\lab}{}
-
 % \midrule color
 \def\graymidrule{\arrayrulecolor{gray30}\midrule\arrayrulecolor{gray65}}
 
@@ -564,24 +561,24 @@ \subsection{The construction in informal type theory\label{sec:ett}}
 
 Table \ref{tab:coind} describes the type of a $\nu$-set at level $m$ in indexed form, as the type of a coinductively-defined infinite sequence of type families representing the limit of $n$-truncated $\nu$-sets: $\Xfrom{m}{n}$ denotes an infinite sequence $X_{n+1}, X_{n+2}, \ldots$ dependent on a $n$-truncated $\nu$-set, $\Xto{m}{n}$, so that, when $m$ is $0$, it denotes a full $\nu$-set, written $\Xp{m}$. This is made possible because the $0$-truncated $\nu$-set, $\Xto{m}{0}$, is degenerated: it is an empty family, defined to be the unit type, and there is thus only one $0$-truncated $\nu$-set, namely the canonical inhabitant $\kstar$ of $\unittype$.
 
-The definition of the type of a $n$-truncated $\nu$-set is in turn described in \ref{tab:core}. In the infinite sequence of type families representing a $\nu$-set, the $n$-th component is a type dependent over a $\fullframe$. The type $\fullframe$ represents a matching object. It is recursively defined in \ref{tab:frames}, using the auxiliary definitions of $\framep$, $\layer$ and $\painting$. The rationale behind $\framep$, $\layer$ and $\painting$ will be explained later but it should already be noticed that the type $\layer$ relies on an operator of frame restriction $\restrf$ which is defined in \ref{tab:faces}, and this restriction operator is in turn defined using the auxiliary definitions of $\restrl$ and $\restrc$.
+The definition of the type of a $n$-truncated $\nu$-set is in turn described in table \ref{tab:core}. In the infinite sequence of type families representing a $\nu$-set, the $n$-th component is a type dependent over a $\fullframe$. The type $\fullframe$ represents a matching object. It is recursively defined in table \ref{tab:frames}, using the auxiliary definitions of $\framep$, $\layer$ and $\painting$. The rationale behind $\framep$, $\layer$ and $\painting$ will be explained later but it should already be noticed that the type $\layer$ relies on an operator of frame restriction $\restrf$ which is defined in table \ref{tab:faces}, and this restriction operator is in turn defined using the auxiliary definitions of $\restrl$ and $\restrc$.
 
 Notably, the definition of $\restrl$ relies on an equality expressing the commutation of the composition of $\restrf$. The proof of this commutation is worth being made explicit, which we do in table \ref{tab:coh} using proof-term notations. The proof requires an induction on the dimension, and on the structure of $\framep$, $\layer$, and $\painting$. This is what $\cohf$ does using auxiliary proofs $\cohl$ and $\cohc$. Even though it looks independent of the definitions from the the other tables, $\cohf$ has to be proved mutually with the definitions of $\framep$, $\layer$, $\painting$, and their corresponding restrictions. More precisely, for a fixed $n$, the block of $\framep$, $\restrf$, and $\cohf$ has to be mutually defined by induction on $p$. Also, each of $\painting$, $\restrc$, and $\cohc$ is built by induction from $p$ to $n$. The $\painting$ block at $n$ relies on the $\framep$ block at $n$, but the converse dependency is only on lower $n$, so this is well-founded. Note that $\layer$, $\restrl$ and $\cohl$ are just abbreviations. The exact way this mutual recursion is eventually formalized is explained in section~\ref{sec:wf}.
 
 Note that for a fixed constant $n$, relying on the evaluation rules of type theory, the coherence conditions degenerate to a reflexivity proof, so that the construction builds an effective sequence of types not mentioning coherences anymore. \\
 
-\renewcommand*{\lab}{tab:coind}
+\def\lab{tab:coind}
 \input{tab-coind.tex}
 
 % For just the second table, keep the universe letter in fullframe
 \renewcommandx{\fullframe}[3][1,2,3]{\prim{fullframe}[#1][#2][][][#3]}
 
-\renewcommand*{\lab}{tab:core}
+\def\lab{tab:core}
 \input{tab-core.tex}
 
 % Drop the universe letter in fullframe for all remaining tables
 \renewcommandx{\fullframe}[3][1,2,3]{\prim{fullframe}[][#2][][][#3]}
-\renewcommand*{\lab}{tab:frames}
+\def\lab{tab:frames}
 \input{tab-frames.tex}
 
 % Truncated sets, otherwise referred to as X
@@ -593,7 +590,7 @@ \subsection{The construction in informal type theory\label{sec:ett}}
 % The third table mentions cohframe; keep ε, ω in this instance
 \renewcommandx{\cohf}[9][1,2,3,4,5,6,7,8,9]{\coh{frame}[][#2][#3][][][#6,#7][#8][#9]}
 
-\renewcommand*{\lab}{tab:faces}
+\def\lab{tab:faces}
 \input{tab-faces-ett.tex}
 
 % Restriction for frame, layer, and painting
@@ -617,7 +614,7 @@ \subsection{The construction in informal type theory\label{sec:ett}}
 \renewcommandx{\cohc}[9][1,2,3,4,5,6,7,8,9]{\coh{painting}[][#2][#3][#4][#5][#6,#7][#8][#9]}
 \renewcommandx{\coht}[9][1,2,3,4,5,6,7,8,9]{\cohtwo{frame}[][#2][#3][#4][#5][#6][#7,#8][#9]}
 
-\renewcommand*{\lab}{tab:coh}
+\def\lab{tab:coh}
 \input{tab-coh-ett.tex}
 
 \subsection{Intuition for our formal construction\label{sec:intuition}}
@@ -793,10 +790,10 @@ \subsection{From extensional to intentional type theory: explication of the equa
 \renewcommandx{\cohl}[9][1,2,3,4,5,6,7,8,9]{\coh{layer}[][#2][#3][#4][#5][#6,#7][#8][#9]}
 \renewcommandx{\cohc}[9][1,2,3,4,5,6,7,8,9]{\coh{painting}[][#2][#3][#4][#5][#6,#7][#8][#9]}
 \renewcommandx{\coht}[9][1,2,3,4,5,6,7,8,9]{\cohtwo{frame}[][#2][#3][#4][#5][#6][#7,#8][#9]}
-\renewcommand*{\lab}{fulltab:faces}
+\def\lab{fulltab:faces}
 \renewcommand{\thetable}{4'}
 \input{tab-faces.tex}
-\renewcommand*{\lab}{fulltab:coh}
+\def\lab{fulltab:coh}
 \renewcommand{\thetable}{5'}
 \input{tab-coh.tex}
 

paper/tab-coh-ett.tex

@@ -1,5 +1,5 @@
-\providecommand*{\lab}{}
-\begin{eqntable}{Commutation of $q$-th projection and $r$-th projection, or coherence conditions\label\lab}
+\providecommand{\lab}{fulltab:coh}
+\begin{eqntable}{Commutation of $q$-th projection and $r$-th projection, or coherence conditions\label{\lab}}
   \eqnline{\cohf[m][\epsilon][\omega][q][r][n][p][p \leq r \leq q \leq n - 2]}{\makecell{\eqnarg{cohframe}{D}{\Xto{m}{n}} \\ \eqnarg{cohframe}{d}{\framep[m][n][p][][D=\D]}}}{:}{\makecell{\restrf[m][\epsilon][q][n-1][p][][D=\hdD, d={\restrf[m][\omega][r][n][p][][D=\D, d=\d]}] \\ = \restrf[m][\omega][r][n-1][p][][D=\hdD, d={\restrf[m][\epsilon][q+1][n][p][][D=\D, d=\d]}]}}
   \eqnline{\cohf[m][\epsilon][\omega][q][r][n][0]}{\D~\unitpoint}{\defeq}{\refl(\unitpoint)}
   \eqnline{\cohf[m][\epsilon][\omega][q][r][n][p'+1]}{\D~(\pair{\d}{\l})}{\defeq}{(\cohf[m][\epsilon][\omega][q][r][n][p'][][D=\D, d=\d], \cohl[m][\epsilon][\omega][q][r][n][p'][][D=\D, d=\d, l=\l])}

paper/tab-coh.tex

@@ -1,4 +1,4 @@
-\providecommand*{\lab}{}
+\providecommand{\lab}{tab:coh}
 \begin{eqntable}{Commutation of $q$-th projection and $r$-th projection, or coherence conditions\label{\lab}}
   \eqnline{\cohf[m][\epsilon][\omega][q][r][n][p][p \leq r \leq q \leq n - 2]}{\makecell{\eqnarg{cohframe}{D}{\Xto{m}{n}}                                                                                                                                                                                                  \\ \eqnarg{cohframe}{d}{\framep[m][n][p][][D=\D]}}}{:}{\makecell{\restrf[m][\epsilon][q][n-1][p][][D=\hdD, d={\restrf[m][\omega][r][n][p][][D=\D, d=\d]}] \\ = \restrf[m][\omega][r][n-1][p][][D=\hdD, d={\restrf[m][\epsilon][q+1][n][p][][D=\D, d=\d]}]}}
   \eqnline{\cohf[m][\epsilon][\omega][q][r][n][0]}{\D~\unitpoint}{\defeq}{\refl(\unitpoint)}

paper/tab-coind.tex

@@ -1,4 +1,4 @@
-\providecommand*{\lab}{}
+\providecommand{\lab}{tab:coind}
 \begin{eqntable}{Main definition\label{\lab}}
   \eqnline{\Xp{m}}{}{:}{\U[m+1]}
   \eqnline{\Xp{m}}{}{\defeq}{\Xfrom{m}{0}[D=\unitpoint]}

paper/tab-core.tex

@@ -1,4 +1,4 @@
-\providecommand*{\lab}{}
+\providecommand{\lab}{tab:core}
 \begin{eqntable}{Truncated $\nu$-sets, the core\label{\lab}}
   \eqnline{\Xto{m}{n}}{}{:}{\U[m+1]}
   \eqnline{\Xto{m}{0}}{}{\defeq}{\unittype}

paper/tab-faces-ett.tex

@@ -1,4 +1,4 @@
-\providecommand*{\lab}{}
+\providecommand{\lab}{fulltab:faces}
 \begin{eqntable}{$q$-th projection of $\mathsf{restr}$, or faces\label{\lab}}
   \eqnline{\restrf[m][\epsilon][q][n][p][p \leq q \leq n - 1]}{\makecell{\eqnarg{restrframe}{D}{\Xto{m}{n}} \\ \eqnarg{restrframe}{d}{\framep[m][n][p][][D=\D]}}}{:}{\framep[m][n-1][p][][D=\hdD]}
   \eqnline{\restrf[m][\epsilon][q][n][0]}{D~\unitpoint}{\defeq}{\unitpoint}

paper/tab-faces.tex

@@ -1,4 +1,4 @@
-\providecommand*{\lab}{}
+\providecommand{\lab}{tab:faces}
 \begin{eqntable}{$q$-th projection of $\mathsf{restr}$, or faces\label{\lab}}
   \eqnline{\restrf[m][\epsilon][q][n][p][p \leq q \leq n - 1]}{\makecell{\eqnarg{restrframe}{D}{\Xto{m}{n}}  \\ \eqnarg{restrframe}{d}{\framep[m][n][p][][D=\D]}}}{:}{\framep[m][n-1][p][][D=\hdD]}
   \eqnline{\restrf[m][\epsilon][q][n][0]}{D~\unitpoint}{\defeq}{\unitpoint}

paper/tab-frames.tex

@@ -1,4 +1,4 @@
-\providecommand*{\lab}{}
+\providecommand{\lab}{tab:frames}
 \begin{eqntable}{$\mathsf{frame}$, $\mathsf{layer}$, and $\mathsf{painting}$\label{\lab}}
   \eqnline{\fullframe[m][n]}{\eqnarg{fullframe}{D}{\Xto{m}{n}}}{:}{\U[m]}
   \eqnline{\fullframe[m][n]}{D}{\defeq}{\framep[m][n][n][][D=\D]}