paper: final polish

paper/paper.tex

@@ -478,17 +478,17 @@ \section{Relating to parametricity\label{sec:rel-param}}
 \section{Our construction}
 In this section, we describe our parametricity-based construction of $\nu$-sets in indexed form at two levels of formality.
 
-Sections \ref{sec:ett} and \ref{sec:itt} describe the construction at an informal level of discourse:
+Sections~\ref{sec:ett} and~\ref{sec:itt} describe the construction at an informal level of discourse:
 \begin{enumerate}
-  \item In \ref{sec:ett}, we present it in informal extensional type theory where equational reasoning is left implicit.
-  \item While reasoning in extensional type theory is similar to reasoning in set theory regarding how equality is handled, extensional type theory has two limitations. The first limitation is that it enforces the principle of Uniqueness of Identity Proofs and this is inconsistent with the Univalence principle, thus making it inexpressible in Homotopy Type Theory. The second limitation is that we want the construction to be formalizable in the Coq proof assistant whose underlying type theory is intensional. Section \ref{sec:itt} thus rephrases the construction in (informal) intensional type theory.
+  \item In~\ref{sec:ett}, we present it in informal extensional type theory where equational reasoning is left implicit.
+  \item While reasoning in extensional type theory is similar to reasoning in set theory regarding how equality is handled, extensional type theory has two limitations. The first limitation is that it enforces the principle of Uniqueness of Identity Proofs and this is inconsistent with the Univalence principle, thus making it inexpressible in Homotopy Type Theory. The second limitation is that we want the construction to be formalizable in the Coq proof assistant whose underlying type theory is intensional. Section~\ref{sec:itt} thus rephrases the construction in (informal) intensional type theory.
 \end{enumerate}
 
-Sections \ref{sec:wf}, \ref{sec:le}, and \ref{sec:eqproperties} describe additional issues to be addressed in order to get a fully formal construction:
+Sections~\ref{sec:wf},~\ref{sec:le}, and~\ref{sec:eqproperties} describe additional issues to be addressed in order to get a fully formal construction:
 \begin{enumerate}
-  \item The well-foundedness of the induction requires a special termination evidence which will be discussed in section \ref{sec:wf}.
-  \item The construction is indexed over integers and holds under some constraints on the range of these integers. There is a standard formalization dilemma in this kind of situation: either the constraints on the range are embedded in the construction so that the construction makes sense only on the corresponding range, or the construction is made first on a more general domain than needed but restricted to a smaller domain at the time of use. We adopted the former approach, requiring the construction to be dependent on proofs of inequalities on natural numbers. We discuss how we deal with such dependencies in section \ref{sec:le}.
-  \item A number of standard groupoid properties of equality as well as type isomorphisms have been left implicit in the informal definition. This is discussed in section \ref{sec:eqproperties}.
+  \item The well-foundedness of the induction requires a special termination evidence which will be discussed in section~\ref{sec:wf}.
+  \item The construction is indexed over integers and holds under some constraints on the range of these integers. There is a standard formalization dilemma in this kind of situation: either the constraints on the range are embedded in the construction so that the construction makes sense only on the corresponding range, or the construction is made first on a more general domain than needed but restricted to a smaller domain at the time of use. We adopted the former approach, requiring the construction to be dependent on proofs of inequalities on natural numbers. We discuss how we deal with such dependencies in section~\ref{sec:le}.
+  \item A number of standard groupoid properties of equality as well as type isomorphisms have been left implicit in the informal definition. This is discussed in section~\ref{sec:eqproperties}.
 \end{enumerate}
 
 \subsection{The construction in informal type theory\label{sec:ett}}
@@ -533,11 +533,11 @@ \subsection{The construction in informal type theory\label{sec:ett}}
 
 A $\nu$-set is a sequence of families of $\U$, that is $\U[m]$ for some universe level $m$. We call such sequence a $\nu$-set at level $m$, whose type thus lives in $\U[m+1]$.
 
-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 $n$ 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 in the unit type, and there is thus only one $0$-truncated $\nu$-set, namely the canonical inhabitant $\kstar$ of $\unittype$.
+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 $n$ 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 in 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 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$. It is recursively defined in table \ref{tab:frames}, using the auxiliary definitions of $\framep$, $\layer$ and $\painting$. A $\fullframe$ describes a boundary of a standard form (simplex, cube), which we decompose into $\layer$, and a $\painting$ corresponds to a filled frame. Notice 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 auxiliary definitions $\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$. It is recursively defined in table~\ref{tab:frames}, using the auxiliary definitions of $\framep$, $\layer$ and $\painting$. A $\fullframe$ describes a boundary of a standard form (simplex, cube), which we decompose into $\layer$, and a $\painting$ corresponds to a filled frame. Notice 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 auxiliary definitions $\restrl$ and $\restrc$.
 
-Notably, the definition of $\restrl$ relies on an equality expressing the commutation of the composition of two $\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 defined in one go 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}.
+Notably, the definition of $\restrl$ relies on an equality expressing the commutation of the composition of two $\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 defined in one go 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 in this case the construction builds an effective sequence of types not mentioning coherences anymore. \\
 
@@ -605,9 +605,10 @@ \subsection{Intuition for our formal construction\label{sec:intuition}}
 \renewcommandx{\coht}{\cohtwo{frame}[][][][][][][][]}
 
 There is a $\fullframe$ for each level $n$, written $\fullframe[n]$, and
-every $X_n$ is uniformly assigned a type of the form $\fullframe[n] \rightarrow \U$. Compared to the informal description given in section \ref{sec:rel-param}, this amounts to applying isomorphisms such as $(A \rightarrow B \rightarrow C) \simeq (A \times B \rightarrow C)$ or $(\Pi a: A.\, (B a \rightarrow C)) \simeq ((\Sigma a: A.\, B a) \rightarrow C)$. In particular, $\fullframe[n]$ is a ``telescope'', or a nesting of $\Sigma$-types.
+every $X_n$ is uniformly assigned a type of the form $\fullframe[n] \rightarrow \U$. Here, $\fullframe[n]$ is thus a ``telescope'' collecting all arguments of the type of $X_i$ in section~\ref{sec:rel-param} as a nesting of $\Sigma$-types.
+
+To illustrate how to recursively build $\fullframe[n]$, let us begin by setting $\fullframe[0] \defeq \unittype$, so that the type $\U$ given to $X_0$ in section~\ref{sec:rel-param} can be equivalently formulated as $\unittype \rightarrow \U$. Then, more generally, let each $\fullframe[n]$ consist of $n$ layers, written $\layer[n][p]$ with $p < n$, that we stack in order, starting from $\unittype$, and writing $\framep[n][p]$ for the $p$ first layers of a $\fullframe[n]$, so that $\fullframe[n]$ is $\framep[n][n]$. For instance, $X_1$ is made of one layer, so that it can be written as a $\Sigma$-type of an inhabitant of $\unittype$ and $\layer[1][0]$. Then, $X_2$ is similarly made of two layers.
 
-To illustrate how to recursively build $\fullframe[n]$, let us begin by setting $\fullframe[0] \defeq \unittype$, so that the type $\U$ given to $X_0$ in section \ref{sec:rel-param} can be equivalently formulated as $\unittype \rightarrow \U$. Then, more generally, let each $\fullframe[n]$ consist of $n$ layers, written $\layer[n][p]$ with $p < n$, that we stack in order, starting from $\unittype$, and writing $\framep[n][p]$ for the $p$ first layers of a $\fullframe[n]$, so that $\fullframe[n]$ is $\framep[n][n]$. For instance, $X_1$ is made of one layer, so that it can be written as a $\Sigma$-type of an inhabitant of $\unittype$ and $\layer[1][0]$, as shown below. The figure also mentions how the type of $X_2$ is structured.
 \begin{small}
   \begin{equation*}
     \begin{array}{ll}
@@ -739,13 +740,13 @@ \subsection{Intuition for our formal construction\label{sec:intuition}}
   \painting[n-2][p](D.\hd.\hd)(\restrf[n-1][p][\omega][p](\restrf[n][p][\epsilon][q+1](d)))
 \end{equation*}
 
-Hence, we need a coherence condition to commute the restrictions. Coherence conditions similar to this necessitate what are shown as, $\cohf$, $\cohl$ and $\cohc$ in table \ref{tab:coh}. These are by induction on the structure of $\framep$, $\layer$ and $\painting$. Note that, for the construction in intensional type theory, we further need a $2$-dimensional coherence condition, $\coht$, for $\cohl$, which is explained in the next section.
+Hence, we need a coherence condition to commute the restrictions. Coherence conditions similar to this necessitate what are shown as, $\cohf$, $\cohl$ and $\cohc$ in table~\ref{tab:coh}. These are by induction on the structure of $\framep$, $\layer$ and $\painting$. Note that, for the construction in intensional type theory, we further need a $2$-dimensional coherence condition, $\coht$, for $\cohl$, which is explained in the next section.
 
 \subsection{From extensional to intensional type theory: making explicit the equality proofs\label{sec:itt}}
 \renewcommandx{\cohf}{\coh{frame}[][][][][][][][]}
-In this section, we intend to get rid of the reflection rule and make explicit what is needed to rephrase the construction in intensional type theory. For readability purpose, we however make explicit only the key coherence conditions of the construction. Other cases of equality reasoning would have to be made explicit to fully obtain a construction in intensional type theory, but these steps are standard enough to be omitted at this stage. See section \ref{sec:eqproperties} for the details.
+In this section, we intend to get rid of the reflection rule and make explicit what is needed to rephrase the construction in intensional type theory. For readability purpose, we however make explicit only the key coherence conditions of the construction. Other cases of equality reasoning would have to be made explicit to fully obtain a construction in intensional type theory, but these steps are standard enough to be omitted at this stage. See section~\ref{sec:eqproperties} for the details.
 
-The need for transport along a proof of commutation of $\restrf$ in the definition of $\restrl$ is made explicit in table \ref{fulltab:faces}, where the arrow over $\cohf$ indicates the direction of rewrite. \\
+The need for transport along a proof of commutation of $\restrf$ in the definition of $\restrl$ is made explicit in table~\ref{fulltab:faces}, where the arrow over $\cohf$ indicates the direction of rewrite. \\
 
 % Insert fulltab:faces and fulltab:coh, after overriding macros to make
 % everything but the universe letter explicit.
@@ -850,7 +851,7 @@ \subsection{Dependencies in inequality proofs\label{sec:le}}
 Compared to \texttt{leY}, \texttt{leI} has no proof-irrelevance properties. This definition is specially crafted for $\painting$, where we have to reason inductively from $p \leq n$ to $n$. In our usage, we have lemmas \texttt{leY\_of\_leI} and \texttt{leI\_of\_leY} in order to equip \texttt{leY} with the induction scheme of \texttt{leI}. The resulting induction scheme has computational rules holding propositionally.
 
 \subsection{Groupoid properties of equality and basic type isomorphisms\label{sec:eqproperties}}
-The construction relies on the groupoid properties of equality which are left implicit in table \ref{fulltab:coh}. The use of the equivalence between $u = v$ and $\Sigma (p:u.\hd = v.\hd). (u.\tl = v.\tl)$ for $u$ and $v$ in a $\Sigma$-type is left implicit in the same table. Also implicit is the use of the equivalence between $f = g$ and $\Pi a: A.\, f(a) = g(a)$ for $f$ and $g$ in $\Pi a: A.\, B$, where it should be recalled that the right-to-left map, or functional extensionality, holds by default in extensional type theory. These have to be made explicit in the formalization.
+The construction relies on the groupoid properties of equality which are left implicit in table~\ref{fulltab:coh}. The use of the equivalence between $u = v$ and $\Sigma (p:u.\hd = v.\hd). (u.\tl = v.\tl)$ for $u$ and $v$ in a $\Sigma$-type is left implicit in the same table. Also implicit is the use of the equivalence between $f = g$ and $\Pi a: A.\, f(a) = g(a)$ for $f$ and $g$ in $\Pi a: A.\, B$, where it should be recalled that the right-to-left map, or functional extensionality, holds by default in extensional type theory. These have to be made explicit in the formalization.
 
 As a final remark, note that as a consequence of $\eta$-conversion for finite enumerated types, the requirement of functional extensionality disappears when $\nu$ is finite. However, this is a conversion which Coq does not implement, and the alternative would be to replace $\Pi a: \nu.\, B$ by a ``flat'' iterated product $B(1) \times B(2) \times \ldots \times B(\nu)$.