From a53c1312d14d5d891037e50a6c8b5daea4b9e15a Mon Sep 17 00:00:00 2001 From: Ramkumar Ramachandra Date: Sat, 12 Oct 2024 12:11:19 +0100 Subject: [PATCH] paper: update after mscs review --- paper/depstream.v | 53 ++++++++++++++++++++ paper/paper.bib | 87 +++++++++++++++++---------------- paper/paper.tex | 120 +++++++++++++++++++++++++++------------------- 3 files changed, 170 insertions(+), 90 deletions(-) create mode 100644 paper/depstream.v diff --git a/paper/depstream.v b/paper/depstream.v new file mode 100644 index 0000000..eace56b --- /dev/null +++ b/paper/depstream.v @@ -0,0 +1,53 @@ +(** The interpretation of dependent streams as a coinductive type in Coq *) + +Section DepStream. + +Context {A} (B: A -> Type) (f: forall a, B a -> A). + +CoInductive DepStream (a: A): Type := + { this : B a ; next : DepStream (f a this) }. + +Check this: forall a, DepStream a -> B a. +Check next: forall a (x: DepStream a), DepStream (f a x.(this a)). + +Context (D: A -> Type) (v: forall a, D a -> B a) + (s: forall a d, D (f a (v a d))). + +CoFixpoint make a (d: D a) : DepStream a := + {| this := v a d; next := make (f a (v a d)) (s a d) |}. + +Check fun a d => eq_refl: (make a d).(this a) = v a d. +Check fun a d => eq_refl: (make a d).(next a) = + make (f a (make a d).(this a)) (s a d). + +End DepStream. + +(** Over propositions, we can also give a second-order interpretation *) + +Section DepStreamProp. + +Context {A: Prop} (B: A->Prop) (f: forall a, B a -> A). + +Definition DepStreamProp (a: A): Prop := + exists D: A -> Prop, (D a /\ exists (v: forall a, D a -> B a), + (forall a d, D (f a (v a d)))). + +Definition this_prop a (x: DepStreamProp a): B a := + let '(ex_intro _ D (conj d (ex_intro _ v s))) := x in v a d. + +Definition next_prop a (x: DepStreamProp a): + DepStreamProp (f a (this_prop a x)) := + let '(ex_intro _ D (conj d (ex_intro _ v s))) := x in + ex_intro _ D (conj (s a d) (ex_intro _ v s)). + +Context (D: A -> Prop) (v: forall a, D a -> B a) + (s: forall a d, D (f a (v a d))). + +Definition make_prop a (d: D a): DepStreamProp a := + ex_intro _ D (conj d (ex_intro _ v s)). + +Check fun a d => eq_refl: this_prop a (make_prop a d) = v a d. +Check fun a d => eq_refl: next_prop a (make_prop a d) = + make_prop (f a (this_prop a (make_prop a d))) (s a d). + +End DepStreamProp. diff --git a/paper/paper.bib b/paper/paper.bib index 6d918e9..ccc1607 100644 --- a/paper/paper.bib +++ b/paper/paper.bib @@ -186,37 +186,6 @@ @phdthesis{moeneclaey22phd school = {Universit\'e Paris Cit\'e} } -@manual{coq23, - author = {{The Coq Development Team}}, - title = {The {Coq} Reference Manual, version 8.18.0}, - month = {Jul}, - year = {2023}, - url = {https://coq.inria.fr/distrib/current/refman/} -} - -@inproceedings{lean15, - author = {Leonardo Mendon{\c{c}}a de Moura and - Soonho Kong and - Jeremy Avigad and - Floris van Doorn and - Jakob von Raumer}, - editor = {Amy P. Felty and - Aart Middeldorp}, - title = {The Lean Theorem Prover (System Description)}, - booktitle = {Automated Deduction - {CADE-25} - 25th International Conference on - Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings}, - series = {Lecture Notes in Computer Science}, - volume = {9195}, - pages = {378--388}, - publisher = {Springer}, - year = {2015}, - url = {https://doi.org/10.1007/978-3-319-21401-6\_26}, - doi = {10.1007/978-3-319-21401-6\_26}, - timestamp = {Tue, 14 May 2019 10:00:39 +0200}, - biburl = {https://dblp.org/rec/conf/cade/MouraKADR15.bib}, - bibsource = {dblp computer science bibliography, https://dblp.org} -} - @misc{voevodsky12, author = {Vladimir Voevodsky}, title = {Semi-simplicial types}, @@ -381,14 +350,6 @@ @inproceedings{kraus21 bibsource = {dblp computer science bibliography, https://dblp.org} } -@manual{agda23, - author = {{The Agda Team}}, - title = {Agda User Manual, Release 2.6.4}, - month = {Jan}, - year = {2023}, - url = {https://readthedocs.org/projects/agda/downloads/pdf/latest} -} - @inproceedings{cohen16, author = {Cyril Cohen and Thierry Coquand and Simon Huber and Anders M{\"{o}}rtberg}, title = {{Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom}}, @@ -464,7 +425,7 @@ @article{shulman15 number = {5}, journal = {Mathematical Structures in Computer Science}, publisher = {Cambridge University Press}, - author = {SHULMAN, MICHAEL}, + author = {Shulman, Michael}, year = {2015}, pages = {1203–1277} } @@ -531,6 +492,15 @@ @article{annenkovCK17 bibsource = {dblp computer science bibliography, https://dblp.org} } +@article{AnnenkovCKS2023, + author={Annenkov, Danil and Capriotti, Paolo and Kraus, Nicolai and Sattler, Christian}, + title={Two-level type theory and applications}, + volume={33}, DOI={10.1017/S0960129523000130}, + number={8}, journal={Mathematical Structures in Computer Science}, + year={2023}, + pages={688–743} +} + @article{shulman_2014, doi = {10.1017/s0960129514000565}, url = {https://doi.org/10.1017%2Fs0960129514000565}, @@ -553,6 +523,31 @@ @PhDThesis{HofmannPhd year = 1995 } +@inproceedings{HofmannStreicher94, + author = {Martin Hofmann and Thomas Streicher}, + title = {The Groupoid Model Refutes Uniqueness of Identity Proofs}, + booktitle = {Proceedings of the Ninth Annual Symposium on Logic in Computer Science + {(LICS} '94), Paris, France, July 4-7, 1994}, + pages = {208--212}, + year = {1994}, + publisher = {{IEEE} Computer Society}, +} + +@inproceedings{BezemCoquandHuber13, + author = {Marc Bezem and Thierry Coquand and Simon Huber}, + title = {A Model of Type Theory in Cubical Sets}, + booktitle = {19th International Conference on Types for Proofs and Programs, {TYPES} + 2013, April 22-26, 2013, Toulouse, France}, + pages = {107--128}, + year = {2013}, + url = {https://doi.org/10.4230/LIPIcs.TYPES.2013.107}, + doi = {10.4230/LIPIcs.TYPES.2013.107}, + editor = {Ralph Matthes and Aleksy Schubert}, + series = {LIPIcs}, + volume = {26}, + publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik}, +} + @article{LoregianRiehl20, title = {Categorical notions of fibration}, journal = {Expositiones Mathematicae}, @@ -565,3 +560,15 @@ @article{LoregianRiehl20 author = {Fosco Loregian and Emily Riehl}, keywords = {Grothendieck fibration, Two-sided fibration, Profunctor}, } + +@article{nuytsdevriese24, + TITLE = {{Transpension: The Right Adjoint to the Pi-type}}, + AUTHOR = {Andreas Nuyts and Dominique Devriese}, + URL = {https://lmcs.episciences.org/13798}, + DOI = {10.46298/lmcs-20(2:16)2024}, + JOURNAL = {{Logical Methods in Computer Science}}, + VOLUME = {{Volume 20, Issue 2}}, + YEAR = {2024}, + MONTH = Jun, + KEYWORDS = {Computer Science - Logic in Computer Science}, +} diff --git a/paper/paper.tex b/paper/paper.tex index 2988753..2c0bf72 100644 --- a/paper/paper.tex +++ b/paper/paper.tex @@ -209,35 +209,39 @@ \subsection*{Fibered vs indexed presentation of semi-simplicial and semi-cubical 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*} -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: +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, together with coherence conditions between the $X_1$ seen as families over $X_0 \times X_0$. This suggests an alternative indexed presentation of the presheaf as a stratified sequence of families indexed by families of lower rank, taking into account those coherence conditions to prevent duplications. Formulated in type theory, it takes the form: \begin{equation*} \begin{array}{llr} - X_0 & : & \U \\ - X_1 & : & X_0 \times X_0 \rightarrow \U \\ + 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 implicitly claimed to construct semi-simplicial types, but the construction was done in a type theory with Uniqueness 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 Uniqueness 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{altenkirch16} 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, like in Voevodsky, on the presentation of the semi-simplicial category from increasing injective maps between finite ordinals. The latter constructions are particularly concise, taking advantage of a definition of increasing injective maps between finite ordinals as type-theoretic functions to inherit the associativity of composition directly from it holding in type theory. This contrasts with the combinatorial construction in \cite{herbelin15} where equations over face maps have to be proved by induction. + +By taking the sum of each component of an indexed presentation over the indexing set of this component, one obtains back a presheaf in the ordinary sense that has a property of \emph{Reedy fibrancy}, that is whose morphisms are projections in the set-theoretic sense. Such Reedy fibrant presheaves over a direct category have been studied in e.g. \cite{shulman15}, \cite{kraus17} and \cite{annenkovCK17,AnnenkovCKS2023}, presenting generic constructions over such presheaves. 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{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. +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}. Cubical set models which differ only by the arity one~\citep{bernardy15} or two~\citep{bezem13} were introduced, and this led to a general notion of affine $\nu$-ary cubes in \cite{nuytsdevriese24}. In parallel, it has 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 in turn be seen as particular instances of the restriction of Nuyts-Devriese's $\nu$-ary cubes to only faces, 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. 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 are likely to better reflect the definitional properties of type theory than presheaf-based cubical sets would. For example, consider 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 construction has the unique property of reflecting the structure of parametricity and of yielding both augmented semi-simplicial and semi-cubical sets from the same construction. The approach taken in \cite{part15} and \cite{altenkirch16} takes benefit of the definitional compositionality of increasing injective maps, but we do not see how they could be generalized to yield semi-cubical sets. + 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 $\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 a fixed color. Let us associate dimension $0$ to colors; then, points are dimension $1$, lines are dimension $2$, and so on. There is hence a shift by one when compared to 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 a fixed color. Let us associate dimension $-1$ to colors; then, points are dimension $0$, lines are dimension $1$, and so on. There is hence a shift by one when compared to semi-simplicial sets. While ordinary semi-simplicial sets are presheaves over the semi-simplex category, augmented semi-simplicial sets are presheaves over \DeltaPlus. There are different ways to define \DeltaPlus, up to equivalence, and we use a definition that can be extended to semi-cubical sets in a straightforward manner. @@ -246,16 +250,16 @@ \subsection*{Augmented semi-simplicial sets} \end{notation} \begin{definition}[$\DeltaPlus$] - The definition of $\DeltaPlus$ is shown below. Note that, if $g \circ f$ is well-defined, then the length of $f$ is less than that of $g$. It can be shown that composition is associative and that $\id$ is neutral. + The definition of $\DeltaPlus$ is shown below. Note that, if $g \circ f$ is well-defined, then the length of $f$ is less than or equal to that of $g$. It can be shown that composition is associative and that $\id$ is neutral. \begin{align*} - \Obj_{\DeltaPlus} & := \Nat \\ - \Hom_{\DeltaPlus}(p, n) & := \{l \in \{0, \kstar\}^n \mid \text{number of $\kstar$ in $l = p$}\} \\ + \Obj_{\DeltaPlus} & := \Nat \\ + \Hom_{\DeltaPlus}(p, n) & := \{l \in \{0, \kstar\}^n \mid \text{number of $\kstar$ in $l = p$}\} \\ g \circ f & := \begin{cases} - f & \text{if $g = \epsilon$} \\ - 0\,(g' \circ f) & \text{if $g = 0\,g'$} \\ + f & \text{if $g = \epsilon$} \\ + 0\,(g' \circ f) & \text{if $g = 0\,g'$} \\ a\,(g' \circ f') & \text{if $g = \kstar\,g'$, $f = a\,f'$, where $a = 0$ or $\kstar$} \\ - \end{cases} \\ + \end{cases} \\ \id & := \kstar \ldots \kstar \text{ $n$ times for $\id \in \Hom_{\DeltaPlus}(n, n)$} \end{align*} \end{definition} @@ -278,10 +282,10 @@ \subsection*{Augmented semi-simplicial sets} \end{align*} \end{definition} -The standard augmented $0$-semi-simplex is a singleton made of one color (in this case, black). Standard augmented $n$-semi-simplices for $n \geq 1$ have a geometric interpretation, and we illustrate them for dimensions $1$, $2$, and $3$. +The standard augmented $(-1)$-semi-simplex is a singleton made of one color (in this case, black). Standard augmented $n$-semi-simplices for $n \geq 0$ have a geometric interpretation, and we illustrate them for dimensions $0$, $1$, and $2$. -\begin{example}[$\DeltaPlus^1$] - The standard augmented $1$-semi-simplex can be pictured as a point, colored black, corresponding to the unique morphism in $\Hom(0, 1)$. This point is the identity in $\Hom(1, 1)$; it is hence shown as a singleton $\kstar$. +\begin{example}[$\DeltaPlus^0$] + The standard augmented $0$-semi-simplex can be pictured as a point, colored black, corresponding to the unique morphism in $\Hom(0, 1)$. This point is the identity in $\Hom(1, 1)$; it is hence shown as a singleton $\kstar$. \begin{equation*} \begin{tikzcd} \kstar @@ -289,8 +293,8 @@ \subsection*{Augmented semi-simplicial sets} \end{equation*} \end{example} -\begin{example}[$\DeltaPlus^2$] - The standard augmented $2$-semi-simplex is drawn as two points, given by $\Hom(1, 2)$, along with a line connecting them, given by $\Hom(2, 2)$. We use black to denote the unique morphisms in $\Hom(0, 1)$ and $\Hom(0, 2)$. +\begin{example}[$\DeltaPlus^1$] + The standard augmented $1$-semi-simplex is drawn as two points, given by $\Hom(1, 2)$, along with a line connecting them, given by $\Hom(2, 2)$. We use black to denote the unique morphisms in $\Hom(0, 1)$ and $\Hom(0, 2)$. \begin{equation*} \begin{tikzcd} \kstar0 \arrow[r, dash, "\kstar\kstar"] & 0\kstar @@ -298,8 +302,8 @@ \subsection*{Augmented semi-simplicial sets} \end{equation*} \end{example} -\begin{example}[$\DeltaPlus^3$] - $\DeltaPlus^3$ is drawn as three points, given by $\Hom(1, 3)$, three lines connecting them, given by $\Hom(2, 3)$, and a triangular filler given by $\Hom(3, 3)$. +\begin{example}[$\DeltaPlus^2$] + $\DeltaPlus^2$ is drawn as three points, given by $\Hom(1, 3)$, three lines connecting them, given by $\Hom(2, 3)$, and a triangular filler given by $\Hom(3, 3)$. \begin{equation*} \begin{tikzcd} & |[alias=F]|00\kstar \arrow[ddr, dash, "0\kstar\kstar"] & \\\\ @@ -318,18 +322,18 @@ \subsection*{Semi-cubical sets} The definition of $\Cube$ is shown below. The symbols $L$ and $R$ indicate opposite faces of a cube. \begin{align*} - \Obj_{\Cube} & := \Nat \\ - \Hom_{\Cube}(p, n) & := \{l \in \{L, R, \kstar\}^n \mid \text{number of $\kstar$ in $l = p$}\} \\ + \Obj_{\Cube} & := \Nat \\ + \Hom_{\Cube}(p, n) & := \{l \in \{L, R, \kstar\}^n \mid \text{number of $\kstar$ in $l = p$}\} \\ g \circ f & := \begin{cases} - f & \text{if $g = \epsilon$} \\ - a\,(g' \circ f) & \text{if $g = a\,g'$}, \text{where $a = L$ or $R$} \\ + f & \text{if $g = \epsilon$} \\ + a\,(g' \circ f) & \text{if $g = a\,g'$}, \text{where $a = L$ or $R$} \\ a\,(g' \circ f') & \text{if $g = \kstar\,g'$, $f = a\,f'$, where $a = L$, $R$, or $\kstar$} \\ - \end{cases} \\ + \end{cases} \\ \id & := \kstar \ldots \kstar \text{ $n$ times} \end{align*} - Again, if $g \circ f$ is well-defined, then the length of $f$ is less than that of $g$. It can be shown that composition is associative and that $\id$ is neutral. + Again, if $g \circ f$ is well-defined, then the length of $f$ is less than or equal to that of $g$. It can be shown that composition is associative and that $\id$ is neutral. \end{definition} \begin{definition}[\CSet] @@ -379,7 +383,7 @@ \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 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 prism 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 prism is obtained by postfixing with $\kstar$. Note that the components can 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: @@ -387,9 +391,9 @@ \subsection*{\texorpdfstring{$\nu$}{ν}-sets} \begin{center} \begin{tabularx}{0.7\linewidth}{X|X|X} \toprule - Cardinal of $\nu$ & 1 & 2 \\ + Cardinal of $\nu$ & 1 & 2 \\ \graymidrule - Interpretation & Augmented semi-simplicial types & Semi-cubical types \\ + Interpretation & Augmented semi-simplicial sets & Semi-cubical sets \\ \bottomrule \end{tabularx} \end{center} @@ -397,28 +401,28 @@ \subsection*{\texorpdfstring{$\nu$}{ν}-sets} To obtain this, we extend $\DeltaPlus$ and $\Cube$ in a straightforward manner into a category which we call $\hexagon$. \begin{definition}[$\hexagon$] - The definition of $\nu$-semi-shape category is shown below. Note that, if $g \circ f$ is well-defined, then the length of $f$ is less than that of $g$. It can be shown that composition is associative and that $\id$ is neutral. + The definition of $\nu$-semi-shape category is shown below. Note that, if $g \circ f$ is well-defined, then the length of $f$ is less than or equal to that of $g$. It can be shown that composition is associative and that $\id$ is neutral. \begin{align*} - \Obj_{\hexagon} & := \Nat \\ - \Hom_{\hexagon}(p, n) & := \{l \in (\nu \sqcup \{\kstar\})^n \mid \text{number of $\kstar$ in $l = p$}\} \\ + \Obj_{\hexagon} & := \Nat \\ + \Hom_{\hexagon}(p, n) & := \{l \in (\nu \sqcup \{\kstar\})^n \mid \text{number of $\kstar$ in $l = p$}\} \\ g \circ f & := \begin{cases} - f & \text{if $g = \epsilon$} \\ - a\,(g' \circ f) & \text{if $g = a\,g'$}, \text{where $a \in \nu$} \\ + f & \text{if $g = \epsilon$} \\ + a\,(g' \circ f) & \text{if $g = a\,g'$}, \text{where $a \in \nu$} \\ a\,(g' \circ f') & \text{if $g = \kstar\,g'$, $f = a\,f'$, where $a \in \nu$ or $a = \kstar$} \\ - \end{cases} \\ + \end{cases} \\ \id & := \kstar \ldots \kstar \text{ $n$ times for $\id \in \Hom_{\hexagon}(n, n)$} \end{align*} \end{definition} 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~(\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{coq23}) and Lean~(\citeyear{lean15}). In type theory, propositions are types and proofs are programs. Type theory includes \emph{definitional equality}, by which all propositions and proofs are quotiented. +\section{Type theory\label{sec:tt}} +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, Coq and Lean. In type theory, propositions are types and proofs are programs. Type theory includes \emph{definitional equality}, by which all propositions and proofs are quotiented. -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}. +Type theory is a flexible formalism supporting different models. Some models come from homotopy theory, and are based on simplicial sets or related structures~\citep{HofmannStreicher94,kapulkin21,BezemCoquandHuber13,cchm}: in these models, equality is interpreted as paths, and they 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 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. +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 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. We also assume that our type theory includes a coinductively-defined notion of dependent streams described in \ref{app:depstream}. 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*} @@ -440,22 +444,22 @@ \section{Type theory} \seqr{}{\Gamma \vdash p: t = u}{\Gamma \vdash t \equiv u} \end{equation*} -Note that the reflection rule implies UIP so that $\U$ and $\Type$ are equivalent in extensional type theory. The reflection rules also implies functional extensionality. Extensional type theory is logically equivalent to intensional type theory extended with UIP and functional extensionality~\citep{HofmannPhd}. +Note that the reflection rule implies UIP so that $\U$ and $\Type$ are equivalent in extensional type theory. The rule also implies functional extensionality. Extensional type theory is logically equivalent to intensional type theory extended with UIP and functional extensionality~\citep{HofmannPhd}. \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{equation*} \begin{array}{llr} - X_0 & : & \U \\ - X_1 & : & X_0 \times X_0 \rightarrow \U \\ + 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$: +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(a)$, for $a:A$, interpreted by $B_\kstar((a_L,a_R),a_\kstar)$ with $a_\kstar:A_\kstar(a_L,a_R)$, a dependent function type $\Pi a: A.\, B(a)$ is interpreted as the graph $(\Pi a: A.\, B(a))_\kstar$ that takes two functions $f_L$ and $f_R$ of type $\Pi a: A.\, B(a)$, 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))) + (\Pi a: A.\, B(a))_\kstar(f_L,f_R) \; \defeq \; \Pi (a_L,a_R): (A \times A).\, \Pi a_\kstar: (A_\kstar(a_L,a_R)\, B_\kstar((a_L,a_R),a_\kstar)(f_L(a_L),f_R(a_R))) \end{align*} Similarly, a product type $A \times B$ is interpreted as the graph $(A \times B)_\kstar$ that relates two tuples $(a_L,b_L)$ and $(a_R,b_R)$ in $A \times B$ as follows: @@ -489,7 +493,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, 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. + \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. Since $\nu$-sets are $0$-truncated types, we compensate for the absence of UIP by assuming a ``local UIP'', requiring types to be \U. \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: @@ -541,7 +545,7 @@ \subsection{The construction in informal type theory\label{sec:ett}} 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, and there is thus only one $0$-truncated $\nu$-set, namely the canonical inhabitant $\kstar$ of $\unittype$. +Table~\ref{tab:coind} describes the type of a $\nu$-set at level $m$ as a dependent stream of type families representing the limit of $n$-truncated $\nu$-sets: using the notations of Section~\ref{sec:tt}, the recursive equation $\Xfrom{m}{n}{D} \,\defeq\, \Sigma R: \Xcomp{m}{n}[D=\D].\, \Xfrom{m}{n+1}[D=\pair{D}{R}]$ from the table formally corresponds to the stream $Stream_{\Sigma n.\, \Xto{m}{n},\, \lambda (n, \D).\, \Xcomp{m}{n}[D=\D],\,\lambda ((n, D),R).(n+1,(\pair{D}{R}))}(n, \D)$. Therefore, $\Xfrom{m}{n}$ denotes an infinite sequence $X_{n}, X_{n+1}, \ldots$ dependent on a $(