From cd0dac6377acbdc0cbcbca29b495301015afe88c Mon Sep 17 00:00:00 2001 From: Ramkumar Ramachandra Date: Sun, 5 Nov 2023 11:55:33 +0000 Subject: [PATCH] paper: major polish; remove some ugly itemize --- paper/paper.tex | 66 ++++++++++++++++++++++++------------------------- 1 file changed, 33 insertions(+), 33 deletions(-) diff --git a/paper/paper.tex b/paper/paper.tex index 0c5e4ae..94afd34 100644 --- a/paper/paper.tex +++ b/paper/paper.tex @@ -201,46 +201,45 @@ \subsection*{Fibered vs indexed presentation of semi-simplicial and semi-cubical \end{equation*} where $\U$ represents in homotopy type theory the subset of types within a given universe where equality of any two elements has at most one proof. -A \emph{presheaf} on an category is a family of sets connected with maps indexed over the morphisms of the category. As such, it lives on the indexed side of the correspondence, contrasting with the fibered side, where we have \emph{discrete Grothendieck fibrations}~\cite{LoregianRiehl20}. However, there are situations where a presheaf $F$ can also be seen as living on the fibered side of the correspondence. This happens when the indexing category is \emph{direct}, or has a downwards-well-founded collection of non-identity morphisms. This is the case in semi-simplicial and semi-cubical sets, where each $F(X)$ serving as source of a map $F(X) \stackrel{F(f)}{\rightarrow} F(Y)$ can be turned into a family $F(X)$ indexed on $F(Y)$. Since the maps are well-founded downward, this can be iterated from below, eventually producing a collection of families which we call an indexed presentation of the presheaf over the direct category. +A \emph{presheaf} on an category is a family of sets connected with maps indexed over the morphisms of the category. As such, it lives on the indexed side of the correspondence, contrasting with the fibered side, where we have \emph{discrete Grothendieck fibrations}~\citep{LoregianRiehl20}. However, there are situations where a presheaf $F$ can also be seen as living on the fibered side of the correspondence. This happens when the indexing category is \emph{direct}, or has a downwards-well-founded collection of non-identity morphisms. This is the case in semi-simplicial and semi-cubical sets, where each $F(X)$ serving as source of a map $F(X) \stackrel{F(f)}{\rightarrow} F(Y)$ can be turned into a family $F(X)$ indexed on $F(Y)$. Since the maps are well-founded downward, this can be iterated from below, eventually producing a collection of families which we call an indexed presentation of the presheaf over the direct category. -For instance, in the case of a semi-cubical set~\citep{grandis03,buchholtz17} presented with $2n$ face maps from the set of $n$-cubes to the set of $(n-1)$-cubes, the standard presheaf approach prescribes a family of sets fibered the ones over the others (up to cubical faces identities). Formulated in type theory, it corresponds to: +Let us consider, for instance, the case of a semi-cubical set~\citep{grandis03,buchholtz17} presented with $2n$ face maps from the set of $n$-cubes to the set of $(n-1)$-cubes. Formulated in type theory, the corresponding presheaf definition of a semi-cubical set prescribes a family of sets and face +maps between them as follows: \begin{equation*} \begin{tikzcd} X_0: \U & X_1: \U \arrow[l, "\partial^L" description, shift left=2] \arrow[l, "\partial^R" description, shift right=2] & X_2: \U \arrow[l, "\partial^{L\kstar}" description, shift left=6] \arrow[l, "\partial^{R\kstar}" description, shift left=2] \arrow[l, "\partial^{\kstar L}" description, shift right=2] \arrow[l, "\partial^{\kstar R}" description, shift right=6] & \ldots \end{tikzcd} \end{equation*} - -On the other side, the indexed presentation of the same presheaf is a stratified sequence of families indexed on elements of families of lower rank, taking into account the coherence conditions to prevent duplications. Formulated in type theory, it takes the form: +up to cubical faces identities. In it, $X_1$ can be seen as a family over $X_0 \times X_0$ presented in a fibered form, $X_2$ can be seen as a family of $X_1 \times X_1 \times X_1 \times X_1$, and so on. This suggests an alternative indexed presentation of the same presheaf as a stratified sequence of families indexed on elements of families of lower rank, taking into account the coherence conditions to prevent duplications. Formulated in type theory, it takes the form: \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*} -The idea for such indexed presentation of presheaves over a direct category was mentioned at the Univalent Foundations year in the context of defining semi-simplicial types~\footnote{See e.g. \url{https://ncatlab.org/nlab/show/semi-simplicial+types+in+homotopy+type+theory}.}. A couple of constructions were proposed since then. One, by \cite{voevodsky12}, relies on the presentation of semi-simplicial sets as a presheaf over increasing injective maps between finite ordinals. Another, by \cite{herbelin15}\footnote{In hindsight, the title of the paper ``A dependently-typed construction of semi-simplicial types'' is somewhat confusing: it was part of a project for defining semi-simplicial types, but, in practice, the definition is done in a type theory with Unicity of Identity Proofs (UIP), meaning in a type theory where types (intended to represent arbitrary $\infty$-groupoids) are actually sets ($0$-truncated $\infty$-groupoids, that is, morally, $0$-groupoids). The confusion between the question of moving from semi-simplicial sets to semi-simplicial types and the question of moving from a presheaf to an indexed presentation of it was however common at the time.}, and fully formalized in the Coq proof assistant, relies on the presentation of semi-simplicial sets as a presheaf over face maps. Another by \cite{part15}, formalized in (an emulation of logic-enriched homotopy type theory in) the Plastic proof assistant, and yet another by \cite{annenkovCK17}, formalized in (an emulation of a two-level type theory in) the Agda proof assistant~\footnote{\url{https://github.com/nicolaikraus/HoTT-Agda/blob/master/nicolai/SemiSimp/SStypes.agda}}, also rely on the presentation of the semi-simplicial category from increasing injective functions over finite ordinals. +The idea for such an indexed presentation of presheaves over a direct category was mentioned at the Univalent Foundations year in the context of defining semi-simplicial types~\footnote{See e.g. \url{https://ncatlab.org/nlab/show/semi-simplicial+types+in+homotopy+type+theory}.}. A couple of constructions were proposed since then. One, by \cite{voevodsky12}, relies on the presentation of semi-simplicial sets as a presheaf over increasing injective maps between finite ordinals. Another, by \cite{herbelin15}\footnote{In hindsight, the title of the paper ``A dependently-typed construction of semi-simplicial types'' is somewhat confusing: it was part of a project for defining semi-simplicial types, but, in practice, the definition is done in a type theory with Unicity of Identity Proofs, meaning, in a type theory where types (intended to represent arbitrary $\infty$-groupoids) are actually sets ($0$-truncated $\infty$-groupoids or $0$-groupoids). The confusion between the question of moving from semi-simplicial sets to semi-simplicial types, and moving from a presheaf to an indexed presentation was, however, common at the time.}, and fully formalized in the Coq proof assistant, relies on the presentation of semi-simplicial sets as a presheaf over face maps. Another by \cite{part15}, formalized in (an emulation of logic-enriched homotopy type theory in) the Plastic proof assistant, and yet another by \cite{annenkovCK17}, formalized in (an emulation of a two-level type theory in) the Agda proof assistant~\footnote{\url{https://github.com/nicolaikraus/HoTT-Agda/blob/master/nicolai/SemiSimp/SStypes.agda}}, also rely on the presentation of the semi-simplicial category from increasing injective functions over finite ordinals. -The indexed definition of a presheaf over a direct category is technically more involved than the presheaf definition as it requires hard-wiring in the structure the dependencies between elements of the sets of the presheaf, including the coherence conditions between these dependencies, such as taking the $i$-th face of the $j$-th face of a $n$-simplex being the same as taking the $(j-1)$-th face of the $i$-th face (when $j>i$). On the other side, defining a concrete presheaf in indexed form only requires to provide the family since the responsibility of defining maps and showing the coherence conditions is already accounted for in the definition, what is not the case by default in the (ordinary) presheaf presentation. +The indexed definition of a presheaf over a direct category is technically more involved than the presheaf definition, as it requires hard-wiring in the structure the dependencies between elements of the sets of the presheaf, including the coherence conditions between these dependencies, such as taking the $i$-th face of the $j$-th face of a $n$-simplex being the same as taking the $(j-1)$-th face of the $i$-th face (when $j>i$). However, defining a concrete presheaf in indexed form only requires providing the family, since the responsibility of defining maps and showing the coherence conditions is already accounted for in the definition. -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}. +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 to join the definition of augmented semi-simplicial sets and cubical sets and to see both of them 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, 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 details a recipe uniformly characterizing unary and binary iterated parametricity in indexed form and to derive from it a new indexed presentation, called indexed \emph{$\nu$-sets}, uniformly 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. Additionally, +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. -\begin{itemize} - \item This new construction is useful in the direction of better understanding the technicality of coherence issues in defining ``semi-simplicial types''~\citep{part15,shulman14,altenkirch16,kraus17}, as well as the dialectic between reasoning in Extensional Type Theory and Intensional Type Theory (as will be discussed in Section~\ref{sec:ett}). - \item Our work is a step in the direction of the program initiated in \cite{altenkirch15} to develop parametricity-based models of parametric type theory~\citep{bernardy15,nuyts17,cavallo19} and cubical type theory~\citep{bezem13,cohen16,angiuli21} which are closer to the syntax of type theory and thus more liable to reflect definitional properties of type theory than presheaf-based cubical sets would do; compare, for example, the loss of definitional properties when interpreting ``indexed'' dependent types of type theory as ``fibrations'' in models such as locally cartesian closed categories~\citep{curien14}. -\end{itemize} +This new construction is useful in the direction of better understanding the technicality of coherence issues in defining ``semi-simplicial types''~\citep{part15,shulman14,altenkirch16,kraus17}, as well as the dialectic between reasoning in Extensional Type Theory and Intensional Type Theory (as will be discussed in Section~\ref{sec:ett}). -See \href{https://github.com/artagnon/bonak}{github.com/artagnon/bonak} for our mechanization. The construction was conceived in Summer 2019, and the mechanization began in late 2019. A sketch of the construction was presented at the 2020 HoTT-UF workshop and the completion of the mechanization was reported at the TYPES 2022 conference. +Our work is a step in the direction of the program initiated in \cite{altenkirch15} to develop parametricity-based models of parametric type theory~\citep{bernardy15,nuyts17,cavallo19} and cubical type theory~\citep{bezem13,cohen16,angiuli21} which are closer to the syntax of type theory, and is likely to better reflect the definitional properties of type theory than presheaf-based cubical sets would do. Compare, for example, the loss of definitional properties when interpreting ``indexed'' dependent types of type theory as ``fibrations'' in models such as locally cartesian closed categories~\citep{curien14}. + +Our mechanization can be found at \href{https://github.com/artagnon/bonak}{github.com/artagnon/bonak}. The construction was conceived in Summer 2019, and the mechanization began in late 2019. A sketch of the construction was presented at the 2020 HoTT-UF workshop and the completion of the mechanization was reported at the TYPES 2022 conference. \section{Semi-simplicial and semi-cubical sets\label{sec:nu}} -In this section, we generalize semi-simplicial and semi-cubical sets to, what we call, $\nu$-sets, subsuming the earlier definitions. We start by first explicitly working out the cases of semi-simplicial and semi-cubical sets. +In this section, we generalize semi-simplicial and semi-cubical sets to $\nu$-sets, subsuming the earlier definitions. We start with some introductory material on semi-simplicial and semi-cubical sets. \subsection*{Augmented semi-simplicial sets} Augmented semi-simplicial sets are defined similarly to semi-simplicial sets, except that the connected components are additionally dependent on a ``color''. Conversely, semi-simplicial sets can be seen as augmented semi-simplicial sets over the singleton set of one fixed color. @@ -394,7 +393,9 @@ \subsection*{Semi-cubical sets} \end{equation*} \end{example} -More generally, the standard $(n + 1)$-semi-cube can be obtained by taking two copies of the standard $n$-semi-cube serving as bottom and top face and connecting them on their border by a cylinder obtained as a third copy stretched in the new dimension. The bottom and top faces are obtained from the standard $n$-semi-cube by postfixing with respectively $L$ and $R$ while the cylinder is obtained by postfixing with $\kstar$. Note that the components can this time be oriented by letting each $n$-dimensional component go from the $(n-1)$-dimensional component obtained by replacing the leftmost $\kstar$ with $L$ to the one obtained by replacing the leftmost $\kstar$ with $R$. +More generally, the standard $(n + 1)$-semi-cube can be obtained by taking two copies of the standard $n$-semi-cube serving as bottom and top face and connecting them on their border by a cylinder obtained as a third copy stretched in the new dimension. The bottom and top faces are obtained from the standard $n$-semi-cube by postfixing with respectively $L$ and $R$ while the cylinder is obtained by postfixing with $\kstar$. Note that the components can + +time be oriented by letting each $n$-dimensional component go from the $(n-1)$-dimensional component obtained by replacing the leftmost $\kstar$ with $L$ to the one obtained by replacing the leftmost $\kstar$ with $R$. \subsection*{\texorpdfstring{$\nu$}{ν}-sets} Let us call $\nu$-sets, the generalization of augmented semi-simplicial sets and semi-cubical sets obtained by building on an arbitrary alphabet $\nu$, so that the following holds: @@ -510,21 +511,20 @@ \section{Relating to parametricity\label{sec:rel-param}} % - refine-style vs tactic-style \section{Our construction} -In this section, we describe our parametricity-based construction of $\nu$-sets in indexed form at different levels of formality: - -\begin{itemize} - \item Sections~\ref{sec:ett} and~\ref{sec:itt} describe the construction at an informal level of discourse: - \begin{itemize} - \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 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}. - \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{itemize} -\end{itemize} +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: +\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. +\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 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}} % Abbreviated tables in this section