paper: minor polish

paper/paper.tex

@@ -185,11 +185,7 @@
     \email{[email protected]}}
 \end{authgrp}
 \begin{abstract}
-  Semi-simplicial and semi-cubical sets are commonly defined as presheaves over respectively, the semi-simplex or semi-cube category. Homotopy Type Theory then popularized an alternative definition, where the set of $n$-simplices or $n$-cubes are instead regrouped into the families of the fibers over their faces, leading to a characterization we call \emph{indexed}.
-
-  Moreover, it is known that semi-simplicial and semi-cubical sets are related to iterated Reynolds's parametricity, respectively in its unary and binary variants.
-
-  We exploit this correspondence to develop an original uniform indexed definition of both augmented semi-simplicial and semi-cubical sets, and fully formalize it in Coq.
+  Semi-simplicial and semi-cubical sets are commonly defined as presheaves over respectively, the semi-simplex or semi-cube category. Homotopy Type Theory then popularized an alternative definition, where the set of $n$-simplices or $n$-cubes are instead regrouped into the families of the fibers over their faces, leading to a characterization we call \emph{indexed}. Moreover, it is known that semi-simplicial and semi-cubical sets are related to iterated Reynolds's parametricity, respectively in its unary and binary variants. We exploit this correspondence to develop an original uniform indexed definition of both augmented semi-simplicial and semi-cubical sets, and fully formalize it in Coq.
 \end{abstract}
 \maketitle
 \vspace{-2em} % Remove space after abstract
@@ -421,7 +417,7 @@ \subsection*{\texorpdfstring{$\nu$}{ν}-sets}
 A $\nu$-set is thus a contravariant functor $\phi$ from the $\nu$-semi-shape category to $\Set$ and we call $n$-$\nu$-semi-shape an element of $\phi(n)$. As in the augmented semi-simplicial and semi-cubical cases, the standard $(n + 1)$-$\nu$-semi-shape is obtained by connecting together $\nu$ copies of the standard $n$-$\nu$-semi-shape with an extra copy stretched in the new dimension. We clarify in the next sections how this process of construction is similar to the parametricity translation developed for functional programming~\citep{reynolds83} and more generally for type theory~\citep{bernardy10, bernardy11, atkey14, bernardy15}.
 
 \section{Type theory}
-Martin-Löf's Type theory~\citep{martinlof75,martinlof84} is a logical formalism based on the notion of a \emph{type} rather than that of a \emph{set}. It can be seen as a foundation of mathematics alternative to set theory and is the core of several tools for the formalization of mathematics such as Agda~(\citeyear{agda23}), Coq~(\citeyear{coq22}) or Lean~(\citeyear{lean15}). In type theory, propositions are types and proofs are programs. A particularity of type theory is also that types and programs, hence propositions and proofs also, are considered modulo an equational theory called definitional equality.
+Martin-Löf's Type theory~(\citeyear{martinlof75,martinlof84}) is a logical formalism based on the notion of a \emph{type} rather than that of a \emph{set}. It can be seen as a foundation of mathematics alternative to set theory and is the core of several tools for the formalization of mathematics such as Agda~(\citeyear{agda23}), Coq~(\citeyear{coq22}) or Lean~(\citeyear{lean15}). In type theory, propositions are types and proofs are programs. A particularity of type theory is also that types and programs, hence propositions and proofs also, are considered modulo an equational theory called definitional equality.
 
 Type theory is a flexible formalism supporting different models. Some models are based on topological spaces, where equality is interpreted as path, and substitutivity of equality as transport~\citep{kapulkin21}. These models support the univalence principle stating that equality of types mimics equivalence of types, leading to the development of Homotopy Type Theory~\citep{hottbook}. In type theory, types are organized in a hierarchy of universes written $\Type_m$ for $m$ a natural number. Main types in type theory are the types of dependent pairs, written $\Sigma a : A.\,B(a)$, the types of dependent functions, written $\Pi a:A.\,B(a)$, for $A$ a type and $B(a)$ a type dependent on the inhabitant $a$ of $A$, and the type of propositional equality, written $t = u$. As a notation, the type of dependent pairs when $B$ is actually not dependent on $A$ is shortened into $A \times B$ and the type of dependent functions when $B$ is not dependent on $A$ is written $A \rightarrow B$. We assume our type theory to also include a distinguished singleton type, written $\unittype$, and with inhabitant $\unitpoint$, the type of boolean values, called $\textsf{bool}$, and the type of natural numbers. We also assume that our type theory includes the coinductive type of infinite tuples. We also write $\hd$ and $\tl$ the projections of dependent pairs, and $\refl$ for reflexivity. Logical propositions being types themselves, we use $\Pi$ to represent universal quantification and $\Sigma$ to represent existential quantification.
 
@@ -456,7 +452,7 @@ \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 binary parametricity which we consider interprets a type $A$ by a family $A_\kstar$ over $A \times A$, what can be seen as a graph whose vertices are in $A$. To each type constructor is thus associated the construction of a graph. To start with, the type of types $\U$ is interpreted as the family of type of families ${\U}_\kstar$, which takes $A_L$ and $A_R$ in $\U$ and returns the type $A_L \times A_R \rightarrow \U$ of families 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 binary parametricity which we consider interprets a closed type $A$ by a family $A_\kstar$ over $A \times A$, what can be seen as a graph whose vertices are in $A$. To each type constructor is thus associated the construction of a graph. To start with, the type of types $\U$ is interpreted as the family of type of families ${\U}_\kstar$, which takes $A_L$ and $A_R$ in $\U$ and returns the type $A_L \times A_R \rightarrow \U$ of families 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_R): (A \times A).\, (A_\kstar(a_L,a_R)\,\rightarrow B_\kstar(f_L(a_L),f_R(a_R)))
 \end{align*}
@@ -507,13 +503,13 @@ \section{Our construction}
 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 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.
+  \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:
 \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 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}.
+  \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 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}.
   \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}
 
@@ -561,9 +557,9 @@ \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 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$.
+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$ defines 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 auxiliary definitions $\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}.
+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 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 the construction builds an effective sequence of types not mentioning coherences anymore. \\
 
@@ -630,11 +626,11 @@ \subsection{Intuition for our formal construction\label{sec:intuition}}
 \renewcommandx{\cohc}[1][1]{\coh{painting}[][][][][][#1][][]}
 \renewcommandx{\coht}{\cohtwo{frame}[][][][][][][][]}
 
-To assign types to $X_0, X_1, X_2, \ldots$ in the above indexed representation, we give a recursive definition relying on the building blocks called $\framep$, $\layer$, and $\painting$. A $\framep$ is a boundary of a standard form (simplex, cube), which we decompose into $\layer$, and a $\painting$ corresponds to a filled $\framep$. Some $\framep$ are full and we call them $\fullframe$: they represent matching objects.
+To assign types to $X_0, X_1, X_2, \ldots$ in the indexed representation, we give a recursive definition relying on the building blocks called $\framep$, $\layer$, and $\painting$. A $\framep$ is a boundary of a standard form (simplex, cube), which we decompose into $\layer$, and a $\painting$ corresponds to a filled $\framep$. Some $\framep$ are full and we call them $\fullframe$: they represent matching objects.
 
-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 the isomorphisms between $A \rightarrow B \rightarrow C$ and $A \times B \rightarrow C$, or between $\Pi a: A.\, (B a \rightarrow C)$ and $(\Sigma a: A.\, B a) \rightarrow C$ to get the expected form $\fullframe[n] \rightarrow \U$. 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$. 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)$, or associativity of $\times$, etc. In particular, $\fullframe[n]$ is a ``telescope'', or a nesting of $\Sigma$-types.
 
-Let us now illustrate how we recursively build $\fullframe[n]$. To begin, let us set $\fullframe[0] = \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, we 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.
+We now illustrate how to recursively build $\fullframe[n]$. To begin, let us set $\fullframe[0] = \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}