From b534ae9908b87f4b3a6c02e30b1cdc7a3dcce30d Mon Sep 17 00:00:00 2001 From: Ramkumar Ramachandra Date: Sun, 31 Dec 2023 11:40:50 +0000 Subject: [PATCH] paper: final polish --- paper/paper.tex | 60 +++++++++++++++++++++++++------------------------ 1 file changed, 31 insertions(+), 29 deletions(-) diff --git a/paper/paper.tex b/paper/paper.tex index 7682408..c2d86e0 100644 --- a/paper/paper.tex +++ b/paper/paper.tex @@ -192,13 +192,13 @@ \section{Introduction} \subsection*{Fibered vs indexed presentation of semi-simplicial and semi-cubical sets} -A family of sets can commonly be represented in two ways: as a family properly speaking, indexed by the elements of a given set $S$, or as a set $T$ together with a map from $T$ to $S$, which specifies for each element of set $T$ its dependency on $S$. In the former case, we call it an \emph{indexed} presentation. In the latter case, the set associated to a given element of $S$ is the fiber of this element, so we call it a \emph{fibered} presentation. The two presentations are equivalent and the equivalence can be phrased concisely in the language of homotopy type theory~\citep{hottbook} as the fibered/indexed equivalence\footnote{In an informal discussion, alternative nomenclatures were proposed: fibration/family equivalence and unbundled/bundled equivalence. The fibered/indexed nomenclature echoes the Grothendieck construction of fibered categories from indexed categories. The most elementary instance of the equivalence, with $\Type$ instead of $\U$, is sometimes called ``Grothendieck construction for dummies'', and its proof requires univalence~\citep{hottbook}.}. +A family of sets can commonly be represented in two ways: as a family properly speaking, indexed by the elements of a given set $S$, or as a set $T$ together with a map from $T$ to $S$, which specifies for each element of $T$ its dependency on $S$. In the former case, we call it an \emph{indexed} presentation. In the latter case, the set associated to a given element of $S$ is the fiber of this element, so we call it a \emph{fibered} presentation. The two presentations are equivalent and the equivalence can be phrased concisely in the language of homotopy type theory~\citep{hottbook} as the fibered/indexed equivalence\footnote{In an informal discussion, alternative nomenclatures were proposed: fibration/family equivalence and unbundled/bundled equivalence. The fibered/indexed nomenclature echoes the Grothendieck construction of fibered categories from indexed categories. The most elementary instance of the equivalence, with $\Type$ instead of $\U$, is sometimes called ``Grothendieck construction for dummies'', and its proof requires univalence~\citep{hottbook}.}. \begin{equation*} \mbox{(fibered)}\qquad(\Sigma T: \U. (T \rightarrow S)) ~\simeq~ (S \rightarrow \U)\qquad \mbox{(indexed)} \end{equation*} Here, $\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 indexed by the object of the category with maps indexed by the morphisms. As such, it lives on the indexed side of the equivalence, 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 equivalence. This happens when the indexing category is \emph{direct}, or has a downwards-well-founded collection of non-identity morphisms. 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. +A \emph{presheaf} on an category is a family of sets indexed by the object of the category with maps indexed by the morphisms. As such, it lives on the indexed side of the equivalence, contrasting with the fibered side, where we have \emph{discrete Grothendieck fibrations}~\citep{LoregianRiehl20}. However, there are situations where a presheaf can also be seen as living on the fibered side of the equivalence. This happens when the indexing category is \emph{direct}, or has a downwards-well-founded collection of non-identity morphisms. 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} @@ -206,19 +206,21 @@ \subsection*{Fibered vs indexed presentation of semi-simplicial and semi-cubical \end{tikzcd} \end{equation*} up to cubical faces identities. Here, $X_1$ can be seen as a family over $X_0 \times X_0$, and $X_2$ can be seen as a family over $X_1 \times X_1 \times X_1 \times X_1$, in the fibered presentation. This suggests an alternative indexed presentation of the presheaf as a stratified sequence of families indexed by 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 \times X_0 \rightarrow \U \\ - X_2 & : \Pi a b c d. & X_1(a)(b) \times X_1 (c)(d) \times X_1(a)(c) \times X_1 (b)(d) \rightarrow \U \\ - \ldots -\end{align*} +\begin{equation*} + \begin{array}{llr} + X_0 & : & \U \\ + X_1 & : & X_0 \times X_0 \rightarrow \U \\ + X_2 & : \Pi a b c d. & X_1(a,b) \times X_1 (c,d) \times X_1(a,c) \times X_1 (b,d) \rightarrow \U \\ + \ldots + \end{array} +\end{equation*} -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{\href{https://ncatlab.org/nlab/show/semi-simplicial+types+in+homotopy+type+theory}{ncatlab.org/nlab/show/semi-simplicial+types+in+homotopy+type+theory}}. A few constructions have been proposed since then. The first construction by \cite{voevodsky12} relies on the presentation of semi-simplicial sets as a presheaf over increasing injective maps between finite ordinals. The second, by \cite{herbelin15}\footnote{In hindsight, the title of the paper ``A dependently-typed construction of semi-simplicial types'' is somewhat confusing: it claimed to construct semi-simplicial types, but the construction was done in a type theory with Unicity of Identity Proofs. Consequentially, what was really obtained was an indexed presentation of semi-simplicial sets. The confusion was however, common at the time.} 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{\href{https://github.com/nicolaikraus/HoTT-Agda/blob/master/nicolai/SemiSimp/SStypes.agda}{github.com/nicolaikraus/HoTT-Agda/blob/master/nicolai/SemiSimp/SStypes.agda}}, 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{\href{https://ncatlab.org/nlab/show/semi-simplicial+types+in+homotopy+type+theory}{ncatlab.org/nlab/show/semi-simplicial+types+in+homotopy+type+theory}}. A few constructions have been proposed since then. The first construction by \cite{voevodsky12} relies on the presentation of semi-simplicial sets as a presheaf over increasing injective maps between finite ordinals. The second, by \cite{herbelin15}\footnote{In hindsight, the title of the paper ``A dependently-typed construction of semi-simplicial types'' is somewhat confusing: it implicitly claimed to construct semi-simplicial types, but the construction was done in a type theory with Unicity of Identity Proofs. Consequentially, what was really obtained was an indexed presentation of semi-simplicial sets. The confusion was however, common at the time.} 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{\href{https://github.com/nicolaikraus/HoTT-Agda/blob/master/nicolai/SemiSimp/SStypes.agda}{github.com/nicolaikraus/HoTT-Agda/blob/master/nicolai/SemiSimp/SStypes.agda}}, 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$). However, exhibiting a concrete instance of a presheaf in indexed form only requires providing the families, since the responsibility of defining maps and showing the coherence conditions is already accounted for in the definition of the structure. \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, families over a product of sets, or \emph{correspondences}, can be used in place of relations. Parametricity can then be iterated, and relying on the fibered presentation 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, and this is 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 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, families over a product of sets, or \emph{correspondences}, can be used in place of relations. Parametricity can then be iterated, and relying on the fibered presentation of correspondences as spans, it has been noted that iterated Reynolds parametricity has the structure of a cubical set~\citep{altenkirch15,moulin16,johann17,moeneclaey21,moeneclaey22phd}. We obtain a \emph{unary} variant of Reynolds \emph{binary} parametricity by using predicates or families instead of relations or correspondences, and this is 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 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 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. @@ -412,7 +414,7 @@ \section{Type theory} 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}. -Types are organized in a hierarchy of universes written $\Type_m$ for $m$ a natural number. The 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 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 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. +Types are organized in a hierarchy of universes written $\Type_m$ for $m$ a natural number. The main types in type theory are the type of dependent pairs, written $\Sigma a : A.\,B(a)$, the type 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 equalities, written $t = u$. As a notation, the type of dependent pairs when $B$ is 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, and the type of natural numbers. We also assume that our type theory includes the coinductive type of infinite dependent tuples. We 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. A type-theoretic notion of sets can be recovered in each universe as $\U[m]$, denoting the subtype of $\Type_m$ for which paths are degenerated, using Uniqueness of Identity Proofs (UIP). Technically, this is expressed as a structure equipping a domain $\Dom$ with the property $\UIP$: \begin{align*} @@ -438,12 +440,14 @@ \section{Type theory} \section{Relating to parametricity\label{sec:rel-param}} 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 \times X_0 \rightarrow \U \\ - X_2 & : \Pi a b c d. & X_1(a)(b) \times X_1 (c)(d) \times X_1(a)(c) \times X_1 (b)(d) \rightarrow \U \\ - \ldots -\end{align*} +\begin{equation*} + \begin{array}{llr} + X_0 & : & \U \\ + X_1 & : & X_0 \times X_0 \rightarrow \U \\ + X_2 & : \Pi a b c d. & X_1(a,b) \times X_1 (c,d) \times X_1(a,c) \times X_1 (b,d) \rightarrow \U \\ + \ldots + \end{array} +\end{equation*} Here, the process of construction of the type of $X_1$ from that of $X_0$, and of the type of $X_2$ from that of $X_1$, 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$, and this can be seen as a graph whose vertices are in $A$. Each type constructor is associated with 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*} @@ -457,7 +461,7 @@ \section{Relating to parametricity\label{sec:rel-param}} In particular, for $X: \U$, applying our parametricity translation is about associating to $X$ an inhabitant $X_\kstar$ of ${\U}_\kstar(X,X)$ i.e. of $X \times X \rightarrow \U$. In turn, applying the translation again to $X_\kstar: X \times X \rightarrow \U$ is about associating to $X_\kstar$ an inhabitant $X_{\kstar\kstar}$ of $(X \times X \rightarrow \U)_\kstar(X_\kstar,X_\kstar)$ i.e. of: \begin{align*} - \Pi ((x_{LL},x_{lR}),(x_{RL},x_{RR})): ((X \times X) \times (X \times X)). \\ + \Pi ((x_{LL},x_{LR}),(x_{RL},x_{RR})): ((X \times X) \times (X \times X)). \\ (X_\kstar(x_{LL},x_{LR}) \times X_\kstar(x_{RL},x_{RR}) \rightarrow X_\kstar(x_{LL}, x_{RL}) \times X_\kstar(x_{LR},x_{RR}) \rightarrow \U) \end{align*} @@ -480,7 +484,7 @@ \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 In~\ref{sec:ett}, we present it in informal extensional type theory where equational reasoning is left implicit, and we give an intuition for the construction in~\ref{sec:intuition}. \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} @@ -531,13 +535,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]} -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]$. +A $\nu$-set in indexed form 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$. 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 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. \\ @@ -604,8 +608,7 @@ \subsection{Intuition for our formal construction\label{sec:intuition}} \renewcommandx{\cohc}[1][1]{\coh{painting}[][][][][][#1][][]} \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$. 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. +There is a $\fullframe$ for each dimension $n$, written $\fullframe[n]$, and every $X_n$ is uniformly assigned a type of the form $\fullframe[n] \rightarrow \U$. Here, $\fullframe[n]$ is 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. @@ -742,9 +745,9 @@ \subsection{Intuition for our formal construction\label{sec:intuition}} 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}} +\subsection{From extensional to intensional type theory\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 the equational reasoning step needed to rephrase the construction in intensional type theory. For readability purposes, we make only explicit in this section 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. \\ @@ -809,7 +812,7 @@ \subsection{Well-foundedness of the construction\label{sec:wf}} \renewcommandx{\cohl}[1][1]{\coh{layer}[][][][][][#1][][]} \renewcommandx{\cohc}[1][1]{\coh{painting}[][][][][][#1][][]} -Since the construction shown in the previous sections is by induction on $n$, and dependencies are on lower $n$ and $p < n$, one would imagine formalizing this using well-founded induction in dependent type theory. We initially tried this approach, and had terms dependent on the proofs of the case distinction that $n' \leq n$ implies $n' < n$ or $n' = n$, but these proofs did not come with enough definitional properties to be usable in practice. Hence, we chose a different route: in practice, since $\restrf[n]$ depends on $\framep[n]$ and $\framep[n-1]$, while $\cohf[n]$ depends on $\framep[n]$, $\framep[n-1]$, and $\framep[n-2]$, we only need to keep track of three ``levels''; hence, we built separate data structures for the levels, with dependencies. More concretely, we build the ten definitions shown in the tables by induction, and this is part of the definition of a larger record. The other fields of the record are $\framep$, $\layer$, $\painting$ at levels $n - 1$ and $n - 2$, $\restrf$, $\restrl$, and $\restrc$ at level $n - 1$, and equations to recall the definitions of these objects at lower levels. +Since the construction shown in the previous sections is by induction on $n$, and dependencies are on lower $n$ and $p < n$, one would imagine formalizing this using well-founded induction in dependent type theory. We initially tried this approach, and had terms dependent on the proofs of the case distinction that $n' \leq n$ implies $n' < n$ or $n' = n$, but these proofs did not come with enough definitional properties to be usable in practice. Hence, we chose a different route: in practice, since $\restrf[n]$ depends on $\framep[n]$ and $\framep[n-1]$, while $\cohf[n]$ depends on $\framep[n]$, $\framep[n-1]$, and $\framep[n-2]$, we only need to keep track of three consecutive dimensions. Hence, what we build by induction at level $n$, is a structure made not only of the definitions shown in the tables~\ref{tab:frames},~\ref{fulltab:faces}, and~\ref{fulltab:coh}, but also of $\framep$, $\layer$, $\painting$ at levels $n - 1$ and $n - 2$, as well as $\restrf$, $\restrl$, and $\restrc$ at level $n - 1$, together with helper equations. \subsection{Dependencies in inequality proofs\label{sec:le}} The entire construction relies on inequalities over natural numbers, and we use two different definitions of $\leq$ addressing different concerns in our formalization. In order to build our first variant, we use an intermediate ``recursive definition'' phrased as: @@ -823,13 +826,12 @@ \subsection{Dependencies in inequality proofs\label{sec:le}} end. \end{minted} -Here $\SProp$ is a definitionally proof-irrelevant impredicative universe morally\footnote{In Coq~(\citeyear{coq23}), it is however a stand-alone universe unrelated to the universe hierarchy.} living at the bottom of the universe hierarchy~\citep{gilbert19}. By placing the definition in \SProp, we have definitional equality of inequality proofs. However, for the purpose of unification, this definition does not go far enough. Consider the unification problems: +Here, $\SProp$ is a definitionally proof-irrelevant impredicative universe morally\footnote{In Coq~(\citeyear{coq23}), it is however a stand-alone universe unrelated to the universe hierarchy.} living at the bottom of the universe hierarchy~\citep{gilbert19}. By placing the definition in \SProp, we have definitional equality of inequality proofs. However, for the purpose of unification, this definition does not go far enough. Consider the unification problems: \begin{minted}{coq} leR_trans ?p leR_refl = ?p leR_trans leR_refl ?p = ?p \end{minted} - where \texttt{leR\_trans} is transitivity, \texttt{leR\_refl} is reflexivity, and \texttt{?p} is an existential variable. These two problems definitionally hold in \SProp, but equating them does not solve the existential. For unification to be useful in inferring existentials, we present our first variant of $\leq$, which we dub as the ``Yoneda variant'': \begin{minted}{coq} @@ -851,7 +853,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 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)$.