paper: changes to Our Construction

paper/paper.tex

@@ -469,10 +469,9 @@ \section{Relating to parametricity\label{sec:rel-param}}
   \ldots
 \end{align*}
 
-In there, the process of construction of the type of $X_1$ from that of $X_0$, and from the type of $X_2$ to that of $X_1$, and so on, is similar to iteratively applying a binary parametricity translation. The parametricity which we consider interprets a type $A$ by a graph $A_\kstar$ over this type, and a term $t: A$ as an edge in $A_\kstar(t)(t)$. In particular, $\U$ is interpreted as the graph ${\U}_\kstar$, which takes $A_L$ and $A_R$ in $\U$ and returns the type $A_L \rightarrow A_R \rightarrow \U$ of graphs over $A_L$ and $A_R$. Also, for $A$ interpreted by $A_\kstar$ and $B$ interpreted by $B_\kstar$, a dependent function type $\Pi a: A.\, B$ is interpreted as the graph $(\Pi a: A.\, B)_\kstar$ that takes two functions $f_L$ and $f_R$ of type $\Pi a: A.\, B$, and expresses that these functions map related arguments in $A$ to related arguments in $B$:
+In there, the process of construction of the type of $X_1$ from that of $X_0$, and from the type of $X_2$ to that of $X_1$, and so on, is similar to iteratively applying a binary parametricity translation. The parametricity which we consider interprets a type $A$ by a family $A_\kstar$ of edges in a graph over $A$, and a term $t: A$ as an edge in $A_\kstar(t)(t)$. To each type constructor is then associated the construction of a graph. In particular, the type of types $\U$ is interpreted as the family of families ${\U}_\kstar$, which takes $A_L$ and $A_R$ in $\U$ and returns the type $A_L \rightarrow A_R \rightarrow \U$ of families of edges over $A_L$ and $A_R$. Also, for $A$ interpreted by $A_\kstar$ and $B$ interpreted by $B_\kstar$, a dependent function type $\Pi a: A.\, B$ is interpreted as the graph $(\Pi a: A.\, B)_\kstar$ that takes two functions $f_L$ and $f_R$ of type $\Pi a: A.\, B$, and expresses that these functions map related arguments in $A$ to related arguments in $B$:
 \begin{align*}
-   & (\Pi a: A.\, B)_\kstar(f_L)(f_R) \defeq                                                      \\
-   & \Pi a_L: A.\, \Pi a_R: A.\, \Pi a_\kstar: A_\kstar(a_L)(a_R).\, B_\kstar(f_L(a_L))(f_R(a_R))
+  (\Pi a: A.\, B)_\kstar(f_L)(f_R) \; \defeq \; \Pi a_L: A.\, \Pi a_R: A.\, \Pi a_\kstar: A_\kstar(a_L)(a_R).\, B_\kstar(f_L(a_L))(f_R(a_R))
 \end{align*}
 
 In particular, for $X: \U$, applying the parametricity translation is about canonically associating to $X$ an inhabitant $X_\kstar$ of ${\U}_\kstar(X)(X)$ i.e. of $X \rightarrow X \rightarrow \U$. In turn, applying the parametricity translation to $X_\kstar: X \rightarrow X \rightarrow \U$ is about canonically associating to $X_\kstar$ an inhabitant $X_{\kstar\kstar}$ of $(X \rightarrow X \rightarrow \U)_\kstar(X_\kstar)(X_\kstar)$ i.e. of:
@@ -518,7 +517,7 @@ \section{Our construction}
           \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 implicitly 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{itemize}
-  \item Sections~\ref{sec:wf}, \ref{sec:le}, and \ref{sec:eqproperties} describe issues to be addressed in order to get a fully formal construction:
+  \item 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{itemize}
           \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 only at the time of use. We adopted the first approach, requiring however 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}.
@@ -568,11 +567,13 @@ \subsection{The construction in informal type theory\label{sec:ett}}
 \renewcommandx{\cohl}[9][1,2,3,4,5,6,7,8,9]{\coh{layer}[][#2][#3][][][][][#9]}
 \renewcommandx{\cohc}[9][1,2,3,4,5,6,7,8,9]{\coh{painting}[][#2][#3][][][][][#9]}
 
-The definition is dispatched over tables \ref{tab:coind}, \ref{tab:core}, \ref{tab:frames} and \ref{tab:faces}. The extra table~\ref{tab:coh} shows the proof of a coherence condition used implicitly in \ref{tab:faces}. Table \ref{tab:coind} describes a $\nu$-set in indexed form, as a coinductively-defined infinite sequence of types representing the limit of $n$-truncated $\nu$-sets. The definition of a $n$-truncated $\nu$-set is in turn described in \ref{tab:core}. In the infinite sequence of types 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 type $\layer$ relies on an operator of frame restriction $\restrf$ which is defined in \ref{tab:faces}. This restriction operator is defined using the auxiliary definitions of $\restrl$ and $\restrc$.
+We use the type $\U$ to represent $\nu$-sets in type theory and fix for that purpose a universe level $m$, that is, we define $\nu$-sets at level $m$ living in $\U[m+1]$.
 
-Notably, the definition of $\restrl$ relies on an equality expressing the commutation of the composition of $\restrf$. This commutation is not provable by computation so we have to prove it propositionally before using the reflection rule. Proving this itself requires an induction on the dimension, and on the structure of $\framep$, $\layer$, and $\painting$. This is what $\cohf$ proves, as shown in the table \ref{tab:coh}, using auxiliary definitions $\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}.
+Table \ref{tab:coind} describes a $\nu$-set at level $m$ in indexed form, as a coinductively-defined infinite sequence of types 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}{n}$ is degenerated: it is defined to be the unit type and there is thus only one $0$-truncated $\nu$-set, namely the canonical inhabitant $\kstar$ of $\unittype$.
 
-Most components of the construction takes inequality constraints as parameters, and we have left implicit that they are satisfied in the tables. Comparison of inequality proofs depends on the definition of inequality, which we leave implicit, only assuming that we can pick a definition for which proofs of $m \leq n$ are provably unique and thus definitionally equal by the reflection rule (formal details are given in section~\ref{sec:le}).
+The definition of a $n$-truncated $\nu$-set is in turn described in \ref{tab:core}. In the infinite sequence of types 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$.
+
+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.