paper: minor consistency update; polish

paper/paper.tex

@@ -227,7 +227,7 @@ \subsection*{Fibered vs indexed presentation of semi-simplicial and semi-cubical
 In category-theoretic terms, the indexing set of the family $X_n$ in the indexed presentation is a \emph{matching object} of the presheaf at $n$. The indexed presentation of presheaves over a direct category can then be identified with a subclass of ordinary presheaves known as Reedy fibrant, where Reedy fibrancy precisely expresses that the set $X_n$ in the fibered presentation is a $\Sigma$-type over a representative of the class of equivalence of matching objects at level $n$~\citep{shulman14,kraus17}.
 
 \subsection*{Reynolds' parametricity and its unary and binary variants}
-In the context of functional programming, Reynolds' parametricity~(\citeyear{reynolds83}) interprets types as relations characterizing the observational behavior of programs of this type. More generally, correspondences, in the sense of ``relevant'' relation, that is of a family over a product of sets, can be used in place of relations. Parametricity can then be iterated, and relying on the fibered representation of correspondences as spans, it has been noted that iterated Reynolds' parametricity has the structure of a cubical set~\citep{johann17,altenkirch15,moulin16,moeneclaey21,moeneclaey22phd}. We obtain a \emph{unary} variant of Reynolds' \emph{binary} parametricity by using predicates or families instead of relations or correspondences, in which case, we obtain a form of realizability~\citep{bernardy12,lasson12,moulin16}. It has then been noted that iterated unary parametricity has the structure of an augmented simplicial set~\footnote{Private communication with Hugo Moeneclaey and Thorsten Altenkirch.}. This similarity suggests that the definition of augmented semi-simplicial sets and semi-cubical sets can both be seen as instances of a more general construction which we call $\nu$-sets of presheaves over a $\nu$-semi-shape category made of words of some cardinal $\nu$+1, where $\nu=1$ gives augmented semi-simplicial sets and $\nu=2$ gives semi-cubical sets.
+In the context of functional programming, Reynolds' parametricity~(\citeyear{reynolds83}) interprets types as relations characterizing the observational behavior of programs of this type. More generally, \emph{correspondences}, in the sense of ``relevant'' relation, that is of a family over a product of sets, can be used in place of relations. Parametricity can then be iterated, and relying on the fibered representation of correspondences as spans, it has been noted that iterated Reynolds' parametricity has the structure of a cubical set~\citep{johann17,altenkirch15,moulin16,moeneclaey21,moeneclaey22phd}. We obtain a \emph{unary} variant of Reynolds' \emph{binary} parametricity by using predicates or families instead of relations or correspondences, in which case, we obtain a form of realizability~\citep{bernardy12,lasson12,moulin16}. It has then been noted that iterated unary parametricity has the structure of an augmented simplicial set~\footnote{Private communication with Hugo Moeneclaey and Thorsten Altenkirch.}. This similarity suggests that the definition of augmented semi-simplicial sets and semi-cubical sets can both be seen as instances of a more general construction, which we call $\nu$-sets, of presheaves over a $\nu$-semi-shape category made of words of some cardinal $\nu$+1, where $\nu=1$ gives augmented semi-simplicial sets and $\nu=2$ gives semi-cubical sets.
 
 \subsection*{Contribution}
 The main contribution of the paper is to describe in full, the details of a recipe that uniformly characterizes unary and binary iterated parametricity in indexed form, and to derive from it a new indexed presentation, called indexed \emph{$\nu$-sets}, of augmented semi-simplicial and semi-cubical sets. Alternatively, from a category-theory perspective, we are characterizing, among the class of matching objects up to isomorphism for augmented semi-simplicial and cubical sets, a particular instance that reflects the structure of iterated parametricity.
@@ -466,8 +466,8 @@ \section{Relating to parametricity\label{sec:rel-param}}
 Let us recall from the introduction, the form taken by the indexed presentation of a semi-cubical set:
 \begin{align*}
   X_0 & :              & \U                                                                                           \\
-  X_1 & :              & X_0 \rightarrow X_0 \rightarrow \U                                                           \\
-  X_2 & : \Pi a b c d. & X_1(a)(b) \rightarrow X_1(a)(c) \rightarrow X_1 (b)(d) \rightarrow X_1 (c)(d) \rightarrow \U \\
+  X_1 & :              & X_0 \times X_0 \rightarrow \U                                                           \\
+  X_2 & : \Pi a b c d. & X_1(a)(b) \times X_1(a)(c) \times X_1 (b)(d) \times X_1 (c)(d) \rightarrow \U \\
   \ldots
 \end{align*}