1. Introduction
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
$T$
its dependency on
$S$
. In the former case, we call it an 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 fibered presentation. The two presentations are equivalent and the equivalence can be phrased concisely in the language of homotopy type theory (The Univalent Foundations Program 2013) as the fibered/indexed equivalence.Footnote
1
\begin{equation*} \mbox{(fibred)}\qquad (\Sigma T: {\mathsf{HSet}}. (T \rightarrow S)) \,\simeq \, (S \rightarrow {\mathsf{HSet}})\qquad \mbox{(indexed)} \end{equation*}
Here,
${\mathsf{HSet}}$
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 presheaf on a 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 discrete Grothendieck fibrations (Loregian and Riehl Reference Loregian and Riehl2020). 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 direct, or has a downwards-well-founded collection of non-identity morphisms. Let us consider, for instance, the case of a semi-cubical set (Buchholtz and Morehouse Reference Buchholtz and Morehouse2017; Grandis and Mauri Reference Grandis and Mauri2003) 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,
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}{lll} X_0 & : {\mathsf{HSet}} \\ X_1 & : X_0 \times X_0 \rightarrow {\mathsf{HSet}} \\ 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 {\mathsf{HSet}} \\ \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 2 A few constructions have been proposed since then. The first construction by Voevodsky (Reference Voevodsky2012) relies on the presentation of semi-simplicial sets as a presheaf over increasing injective maps between finite ordinals. The second, by Herbelin (Reference Herbelin2015)Footnote 3 formalized in the Coq proof assistant, relies on the presentation of semi-simplicial sets as a presheaf over face maps. Another by Part and Luo (Reference Part and Luo2015) formalized in an emulation of logic-enriched homotopy type theory in the Plastic proof assistant, and yet another by Altenkirch et al. (Reference Altenkirch, Capriotti, Kraus, Talbot and Regnier2016) formalized in an emulation of a two-level type theory in the Agda proof assistant,Footnote 4 rely, like in Voevodsky, on the presentation of the semi-simplicial category from increasing injective maps between finite ordinals. The latter constructions, besides being stated as providing semi-simplicial types (thanks to an extension of the type theory), 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 Herbelin (Reference Herbelin2015) 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 Reedy fibrancy, that is whose morphisms are projections in the set-theoretic sense. Such Reedy fibrant presheaves over a direct category have been studied, for example, Shulman (Reference Shulman2015), Kraus and Sattler (Reference Kraus and Sattler2017), and Annenkov et al., (Reference Annenkov, Capriotti and Kraus2017, Reference Annenkov, Capriotti, Kraus and Sattler2023), 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 of 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\gt 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.
Reynolds parametricity and its unary and binary variants
In the context of functional programing, Reynolds parametricity (Reference Reynolds and Mason1983) interprets types as relations characterizing the observational behavior of programs of this type. More generally, families over a product of sets, or 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 (Altenkirch and Kaposi Reference Altenkirch, Kaposi and Uustalu2015; Johann and Sojakova Reference Johann and Sojakova2017; Moeneclaey Reference Moeneclaey2021, Reference Moeneclaey2022; Moulin, Reference Moulin2016). We obtain a unary variant of Reynolds binary parametricity by using predicates or families instead of relations or correspondences, and this is a form of realizability (Bernardy and Moulin Reference Bernardy and Moulin2012; Lasson Reference Lasson2014; Moulin Reference Moulin2016). Cubical set models which differ only by the arity one (Bernardy et al. Reference Bernardy, Coquand and Moulin2015) or two (Bezem et al. Reference Bezem, Coquand, Huber, Matthes and Schubert2013a) were introduced, and this led to a general notion of affine
$\nu$
-ary cubes in Nuyts and Devriese (Reference Nuyts and Devriese2024). In parallel, it has been noted that iterated unary parametricity has the structure of an augmented simplicial set.Footnote
5
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.
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
$\nu$
-sets, of augmented semi-simplicial and semi-cubical sets.
Our work is a step in the direction of the program initiated by Altenkirch and Kaposi (Reference Altenkirch, Kaposi and Uustalu2015) to develop parametricity-based models of parametric type theory (Bernardy et al. Reference Bernardy, Coquand and Moulin2015; Cavallo and Harper Reference Cavallo, Harper, Fernández and Muscholl2020; Nuyts et al. Reference Nuyts, Vezzosi and Devriese2017) and cubical type theory (Angiuli et al. Reference Angiuli, Brunerie, Coquand, Harper, Hou (Favonia) and Licata2021; Bezem et al. Reference Bezem, Coquand, Huber, Matthes and Schubert2013a; Cohen et al. Reference Cohen, Coquand, Huber, Mörtberg and Uustalu2018), 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 (Curien et al. Reference Curien, Garner and Hofmann2014).
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 by Part and Luo (Reference Part and Luo2015) and Altenkirch et al. (Reference Altenkirch, Capriotti, Kraus, Talbot and Regnier2016) 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 github.com/artagnon/bonak. The construction was conceived in Summer of 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.
2. 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.
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 “colour.” 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.
While ordinary semi-simplicial sets are presheaves over the semi-simplex category, augmented semi-simplicial sets are presheaves over
$\boldsymbol{\Delta }_+$
. There are different ways to define
$\boldsymbol{\Delta }_+$
, up to equivalence, and we use a definition that can be extended to semi-cubical sets in a straightforward manner. In particular, we start numbering objects from
$0$
instead of
$-1$
so that there is a shift by one compared to the standard numbering of augmented semi-simplicial sets.
Notation 1 (Finite sequences). We denote finite sequences by
$i_1 \ldots i_n$
for
$i_j$
ranging over some domain. The empty sequence is written
$\epsilon$
.
Definition 2 (
$\boldsymbol{\Delta }_+$
). The definition of
$\boldsymbol{\Delta }_+$
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
$\mathsf{id}$
is neutral.
\begin{align*} \mathsf{Obj}_{{\boldsymbol{\Delta }_+}} & := \mathbb{N} \\ \mathsf{Hom}_{{\boldsymbol{\Delta }_+}}(p, n) & := \{l \in \{0, {\star }\}^n \mid \textit{number of } {\star } \textit{ in } l = p\} \\ g \circ f & := {\begin{cases} f & \textit{if } g = \epsilon \\ 0\,(g' \circ f) & \textit{if } g = 0\,g' \\ a\,(g' \circ f') & \textit{if } g = {\star }\,g', f = a\,f', \textit{ where } a = 0 \textit{ or } {\star } \\ \end{cases}} \\ \mathsf{id} & := {\star } \ldots {\star } n \textit{ times for } \mathsf{id} \in \mathsf{Hom}_{{\boldsymbol{\Delta }_+}}(n, n) \end{align*}
Definition 3 (
$\mathsf{Set}_{\boldsymbol{\Delta }_+}$
). We define the category of augmented semi-simplicial sets as the functor category:
\begin{equation*} \mathsf{Set}_{\boldsymbol{\Delta }_+} := \mathsf{Set}^{{\boldsymbol{\Delta }}_+^{\mathsf{op}}} \end{equation*}
To provide examples, we define the standard augmented
$n$
-semi-simplex, taking into account the shift by one in the numbering.
Definition 4 (
$\boldsymbol{\Delta }^n_{+}$
). The standard augmented
$(n-1)$
-semi-simplex
${\boldsymbol{\Delta }}_+^{n-1}$
is defined as the Yoneda embedding of
$n \in \mathsf{Obj}({\boldsymbol{\Delta }_+})$
:
\begin{align*} {\boldsymbol{\Delta }}_+^{n-1} & : \mathsf{Set}_{{\boldsymbol{\Delta }_+}} \\ {\boldsymbol{\Delta }}_+^{n-1}(p) & := \mathsf{Hom}(p, n) \\ {\boldsymbol{\Delta }}_+^{n-1}(f) & := \lambda g .\, g \circ f \end{align*}
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$
.
Example 5 (
$\boldsymbol{\Delta }_+^0$
). The standard augmented
$0$
-semi-simplex can be pictured as a point, colored black, corresponding to the unique morphism in
$\mathsf{Hom}(0, 1)$
. This point is the identity in
$\mathsf{Hom}(1, 1)$
; it is hence shown as a singleton
$\star$
.
$\star$
Example 6 (
${\boldsymbol{\Delta }}_+^1$
). The standard augmented
$1$
-semi-simplex is drawn as two points, given by
$\mathsf{Hom}(1, 2)$
, along with a line connecting them, given by
$\mathsf{Hom}(2, 2)$
. We use black to denote the unique morphisms in
$\mathsf{Hom}(0, 1)$
and
$\mathsf{Hom}(0, 2)$
.
Example 7 (
${\boldsymbol{\Delta }}_+^2$
).
${\boldsymbol{\Delta }}_+^2$
is drawn as three points, given by
$\mathsf{Hom}(1, 3)$
, three lines connecting them, given by
$\mathsf{Hom}(2, 3)$
, and a triangular filler given by
$\mathsf{Hom}(3, 3)$
.
More generally, the standard augmented
$(n + 1)$
-semi-simplex can be obtained by taking a copy of the standard augmented
$n$
-semi-simplex serving as a base, and gluing on top of it another copy lifted by one dimension. In the second copy, the color becomes an extra point, the points become lines connecting the points of the base to the extra point, and so on. In particular, the components of the base are those of the standard augmented
$n$
-semi-simplex postfixed by
$0$
while the components of the lifted copy are postfixed by
$\star$
. Note that the components may be oriented by letting each
$n$
-dimensional component point to the
$(n-1)$
-dimensional component obtained by replacing the leftmost
$\star$
of the
$n$
-dimensional component with
$0$
.
Semi-cubical sets
Semi-cubical sets are defined like augmented semi-simplicial sets except that
$\boldsymbol{\Delta }_+$
is replaced by
$\boldsymbol{{\square }}$
in which we take sequences of
$L$
,
$R$
, and
$\star$
, instead of sequences of
$0$
and
$\star$
.
Definition 8 (
$\boldsymbol{{\square }}$
). The definition of
$\boldsymbol{{\square }}$
is shown below. The symbols
$L$
and
$R$
indicate opposite faces of a cube.
\begin{align*} \mathsf{Obj}_{{\boldsymbol{{\square }}}} & := \mathbb{N} \\ \mathsf{Hom}_{{\boldsymbol{{\square }}}}(p, n) & := \{l \in \{L, R, {\star }\}^n \mid \textit{number of ${\star }$ in $l = p$}\} \\ g \circ f & := \begin{cases} f & \textit{if $g = \epsilon $} \\ a\,(g' \circ f) & \textit{if $g = a\,g'$}, \textit{where $a = L$ or $R$} \\ a\,(g' \circ f') & \textit{if $g = {\star }\,g'$, $f = a\,f'$, where $a = L$, $R$, or ${\star }$} \\ \end{cases} \\ \mathsf{id} & := {\star } \ldots {\star } \textit{ $n$ times} \end{align*}
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
$\mathsf{id}$
is neutral.
Definition 9 (
$\mathsf{Set}_{\boldsymbol{\square }}$
). We define the category of semi-cubical sets as the functor category:
\begin{equation*} {\mathsf{Set}_{\boldsymbol{\square }}} := \mathsf{Set}^{{\boldsymbol{{\square }}}{\mathsf{op}}} \end{equation*}
Definition 10 (
${\boldsymbol{{\square }}}^n$
). The standard semi-cube
${\boldsymbol{{\square }}}^n$
is defined as the Yoneda embedding of
$n \in \mathsf{Obj}({\boldsymbol{{\square }}})$
:
\begin{align*} {\boldsymbol{{\square }}}^n & : {\mathsf{Set}_{\boldsymbol{\square }}} \\ {\boldsymbol{{\square }}}^n(p) & := \mathsf{Hom}(p, n) \\ {\boldsymbol{{\square }}}^n(f) & := \lambda g .\, g \circ f \end{align*}
Standard
$n$
-semi-cubes have a geometric interpretation, which we illustrate for dimensions
$0$
,
$1$
, and
$2$
.
Example 11 (
${\boldsymbol{{\square }}}^0$
).
${\boldsymbol{{\square }}}^0$
is
$\mathsf{Hom}(0, 0)$
, or the singleton set of the empty sequence:
$\epsilon$
Example 12 (
${\boldsymbol{{\square }}}^1$
).
${\boldsymbol{{\square }}}^1$
consists of two points, given by
$\mathsf{Hom}(0, 1)$
, and a line, given by
$\mathsf{Hom}(1, 1)$
.
Example 13 (
${\boldsymbol{{\square }}}^2$
).
${\boldsymbol{{\square }}}^2$
consists of four points, given by
$\mathsf{Hom}(0, 2)$
, four lines connecting the four points, given by
$\mathsf{Hom}(1, 2)$
, and a filler, given by
$\mathsf{Hom}(2, 2)$
:
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
$\star$
. 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
$\star$
with
$L$
, to the one obtained by replacing the leftmost
$\star$
with
$R$
.
$\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:
To obtain this, we extend
$\boldsymbol{\Delta }_+$
and
$\boldsymbol{{\square }}$
in a straightforward manner into a category which we call
.
Definition 14 (
). 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
$\mathsf{id}$
is neutral.
A
$\nu$
-set is thus a contravariant functor
$\phi$
from the
$\nu$
-semi-shape category to
$\mathsf{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 programing (Reynolds Reference Reynolds and Mason1983) and more generally for type theory (Atkey et al., Reference Atkey, Ghani and Johann2014; Bernardy et al. Reference Bernardy, Jansson, Paterson, Hudak and Weirich2010, Reference Bernardy, Coquand and Moulin2015; Bernardy and Lasson, Reference Bernardy and Lasson2011).
3. Type Theory
Martin-Löf’s type theory (Reference Martin-Löf1975,Reference Martin-Löf1984) is a logical formalism based on the notion of a type rather than that of a 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 definitional equality, by which all propositions and proofs are quotiented.
Type theory is a flexible formalism supporting different models. Some models come from homotopy theory, and are based on simplicial sets or related structures (Bezem et al. Reference Bezem, Coquand, Huber, Matthes and Schubert2013b; Cohen et al. Reference Cohen, Coquand, Huber, Mörtberg and Uustalu2015; Hofmann and Streicher Reference Hofmann and Streicher1994; Kapulkin and Lumsdaine Reference Kapulkin and Lumsdaine2021): 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 (The Univalent Foundations Program 2013).
Types are organized in a hierarchy of universes written
${\mathsf{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
$\mathsf{unit}$
, and with inhabitant
$\ast$
, the type of boolean values, and the type of natural numbers. We write
$\mathsf{hd}$
and
$\mathsf{tl}$
the projections of dependent pairs, and
$\mathsf{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 Appendix A.
A type-theoretic notion of sets can be recovered in each universe as
${\mathsf{{HSet}}_{m}}$
, denoting the subtype of
${\mathsf{Type}}_m$
for which paths are degenerated, using Uniqueness of Identity Proofs (UIP). Technically, this is expressed as a structure equipping a domain
$\textsf {Dom}$
with the property
$\textsf {UIP}$
:
\begin{align*} {\textsf {Dom}} & : {\mathsf{Type}}_m \\ {\textsf {UIP}} & : \Pi x y: {\textsf {Dom}}.\, \Pi p q: x = y.\, p = q \end{align*}
In
${\mathsf{{HSet}}_{m}}$
, the following properties hold:
-
(1) UIP holds on the unit type, bool type, as well as all types of finite cardinal
$\nu$
. -
(2) UIP propagates to
$\Sigma$
-types. -
(3) UIP propagates to
$\Pi$
-types, with some additional functional extensionality axioms.
By notation,
${\mathsf{Type}}$
and
${\mathsf{{HSet}}}$
mean
${\mathsf{Type}}_m$
and
${\mathsf{{HSet}}_{m}}$
at some unspecified universe level
$m$
.
We are also interested in extensional type theory, a type theory with the following reflection rule, where
$=$
is propositional equality in some type and
$\equiv$
is definitional equality (Martin-Löf Reference Martin-Löf1984):
\begin{equation*} \frac {\Gamma \vdash p: t = u}{\Gamma \vdash t \equiv u} \end{equation*}
Note that the reflection rule implies UIP so that
${\mathsf{{HSet}}}$
and
${\mathsf{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 (Hofmann Reference Hofmann1995).
4. Relating to Parametricity
Recall from the introduction, the form taken by the indexed presentation of a semi-cubical set:
\begin{equation*} \begin{array}{lll} X_0 & : {\mathsf{{HSet}}} \\ X_1 & : X_0 \times X_0 \rightarrow {\mathsf{{HSet}}} \\ 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 {\mathsf{{HSet}}} \\ \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_{\star }$
over
$A \times A$
, and this can be seen as a graph whose vertices are in
$A$
. Each type of constructor is associated with the construction of a graph. To start with, the type of types
${\mathsf{{HSet}}}$
is interpreted as the family of type of families
${{\mathsf{HSet}}}_{\star }$
, which takes
$A_L$
and
$A_R$
in
${\mathsf{HSet}}$
and returns the type
$A_L \times A_R \rightarrow {\mathsf{HSet}}$
of families over
$A_L$
and
$A_R$
. Also, for
$A$
interpreted by
$A_{\star }$
and
$B(a)$
, for
$a:A$
, interpreted by
$B_{\star }((a_L,a_R),a_{\star })$
with
$a_{\star }:A_{\star }(a_L,a_R)$
, a dependent function type
$\Pi a: A.\, B(a)$
is interpreted as the graph
$(\Pi a: A.\, B(a))_{\star }$
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{equation*} \begin{array}{l} (\Pi a: A.\, B(a))_{\star }(f_L,f_R) \; {\triangleq } \\ {\qquad \Pi (a_L,a_R): (A \times A).\, \Pi a_{\star }: (A_{\star }(a_L,a_R)\, B_{\star }((a_L,a_R),a_{\star })(f_L(a_L),f_R(a_R)))} \end{array} \end{equation*}
Similarly, a product type
$A \times B$
is interpreted as the graph
$(A \times B)_{\star }$
that relates two tuples
$(a_L,b_L)$
and
$(a_R,b_R)$
in
$A \times B$
as follows:
\begin{align*} (A \times B)_{\star }((a_L,b_L),(a_R,b_R)) \; {\triangleq } \; A_{\star }(a_L,a_R) \times B_{\star }(b_L,b_R) \end{align*}
In particular, for
$X: {\mathsf{HSet}}$
, applying our parametricity translation is about associating to
$X$
an inhabitant
$X_{\star }$
of
${{\mathsf{HSet}}}_{\star }(X,X)$
that is of
$X \times X \rightarrow {\mathsf{HSet}}$
. In turn, applying the translation again to
$X_{\star }: X \times X \rightarrow {\mathsf{HSet}}$
is about associating to
$X_{\star }$
an inhabitant
$X_{{\star }{\star }}$
of
$(X \times X \rightarrow {\mathsf{HSet}})_{\star }(X_{\star },X_{\star })$
that is of:
\begin{align*} \Pi ((x_{LL},x_{LR}),(x_{RL},x_{RR})): ((X \times X) \times (X \times X)). \\ (X_{\star }(x_{LL},x_{LR}) \times X_{\star }(x_{RL},x_{RR}) \rightarrow X_{\star }(x_{LL}, x_{RL}) \times X_{\star }(x_{LR},x_{RR}) \rightarrow {\mathsf{HSet}}) \end{align*}
which hints us at how the sequence
$X_0$
,
$X_1$
,
$X_2$
can be seen as a sequence of inhabitants of the iteration of the composition of binary parametricity with the diagonal on types and type families, applied to an initial
$X: {\mathsf{HSet}}$
:
\begin{equation*} \begin{array}{lllll} X_0 & {\triangleq } & X & : & {\mathsf{HSet}} \\ X_1 & {\triangleq } & X_{\star } & : & {{\mathsf{HSet}}}_{\star }(X,X) \\ X_2 & {\triangleq } & X_{{\star }{\star }} & : & ({{\mathsf{HSet}}}_{\star }(X,X))_{{\star }}(X_{\star },X_{\star }) \\ \ldots \end{array} \end{equation*}
This tells us how the informal type given to
$X_2$
in the previous section could be rephrased so that it comes as the instance of a general recipe characterizing the type of all
$X_i$
.
Notice, however, that the recipe obtained so far,
$X_{n + 1}: ({S_n})_{\star }(X_n,X_n)$
for
$X_n: S_n$
, applies parametricity on the syntax of the type of
$X_n$
. It does not directly yield a characterization of
$S_n$
as a function from
$n$
. Reformulating the recipe as an explicit recursive construction, without requiring an interpretation of the syntax of types, is the main outcome of this work, together with the mechanization and the uniform treatment of augmented semi-simplicial and semi-cubical sets by means of the generalization to
$\nu$
-sets.
5. Our Construction
In this section, we describe our parametricity-based construction of
$\nu$
-sets in indexed form at two levels of formality.
Sections 5.1 and 5.3 describe the construction at an informal level of discourse:
-
(1) In Section 5.1, we present it in informal extensional type theory where equational reasoning is left implicit, and we give an intuition for the construction in Section 5.2.
-
(2) 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 5.3 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
${\mathsf{HSet}}$
.
Sections 5.4, 5.5, and 5.6 describe additional issues to be addressed in order to get a fully formal construction:
-
(1) The well-foundedness of the induction requires a special termination evidence, which will be discussed in Section 5.4.
-
(2) The construction is indexed over integers and holds under some constraints on the range of these integers. There is a standard formalization dilemma in this kind of situation: either the constraints on the range are embedded in the construction so that the construction makes sense only on the corresponding range, or the construction is made first on a more general domain than needed but restricted to a smaller domain at the time of use. We adopted the former approach, requiring the construction to be dependent on proofs of inequalities in natural numbers. We discuss how we deal with such dependencies in Section 5.5.
-
(3) 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 5.6.
5.1 The construction in informal type theory
A
$\nu$
-set in indexed form is a sequence of families of
${\mathsf{HSet}}$
, that is
${\mathsf{{HSet}}_{m}}$
for some universe level
$m$
. We call such sequence a
$\nu$
-set at level
$m$
, whose type thus lives in
${\mathsf{{HSet}}_{m+1}}$
.
Table 1 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 3, the recursive equation
$\boldsymbol{\nu} \mathsf{Set}^{\geq n}_{m}{D} \,{\triangleq }\, \Sigma R: \boldsymbol{\nu} \mathsf{Set}^{=n}_{m}(D).\, \boldsymbol{\nu} \mathsf{Set}^{\geq n+1}_{m}({D},{R})$
from the table formally corresponds to the stream
$Stream_{\Sigma n.\, \boldsymbol{\nu} \mathsf{Set}^{\lt n}_{m},\, \lambda (n, {D}).\, \boldsymbol{\nu} \mathsf{Set}^{=n}_{m}({D}),\,\lambda ((n, D),R).(n+1,({D},{R}))}(n, {D})$
. Therefore,
$\boldsymbol{\nu} \mathsf{Set}^{\geq n}_{m}$
denotes an infinite sequence
$X_{n}, X_{n+1}, \ldots$
dependent on a
$({\lt} n)$
-truncated
$\nu$
-set,
$\boldsymbol{\nu} \mathsf{Set}^{\lt n}_{m}$
, so that, when
$n$
is
$0$
, it denotes a full
$\nu$
-set, written
$\boldsymbol{\nu} \mathsf{Set}_{m}$
. This is made possible because the
$({\lt} 0)$
-truncated
$\nu$
-set,
$\boldsymbol{\nu} \mathsf{Set}^{\lt 0}_{m}$
, is degenerated: it is an empty family, and there is thus only one
$({\lt} 0)$
-truncated
$\nu$
-set, namely the canonical inhabitant
$\star$
of
$\mathsf{unit}$
.
Main definition
The definition of the type of a
$n$
-truncated
$\nu$
-set is in turn described in Table 2. In the infinite sequence of type families representing a
$\nu$
-set, the
$n$
-th component is a type dependent over a
$\boldsymbol{\mathsf{fullframe}}$
. It is recursively defined in Table 3, using the auxiliary definitions of
$\boldsymbol{\mathsf{frame}}$
,
$\boldsymbol{\mathsf{layer}}$
, and
$\boldsymbol{\mathsf{painting}}$
. A
$\boldsymbol{\mathsf{fullframe}}$
describes a boundary of a standard form (simplex, cube), which we decompose into
$\boldsymbol{\mathsf{layer}}$
, and a
$\boldsymbol{\mathsf{painting}}$
corresponds to a filled frame. Notice that the type
$\boldsymbol{\mathsf{layer}}$
relies on an operator of frame restriction
${{\mathsf{restr}}}_{\boldsymbol{\mathsf{frame}}}$
, which is defined in Table 4, and this restriction operator is in turn defined using auxiliary definitions
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{layer}}}$
and
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{painting}}}$
.
Truncated
$\nu$
-sets, the core
$\mathsf{frame}$
,
$\mathsf{layer}$
, and
$\mathsf{painting}$
$q$
-th projection of
$\mathsf{restr}$
, or faces
Notably, the definition of
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{layer}}}$
relies on an equality expressing the commutation of the composition of two
${{\mathsf{restr}}}_{\boldsymbol{\mathsf{frame}}}$
. The proof of this commutation is worth being made explicit, which we do in Table 5 using proof-term notations. The proof requires an induction on the dimension and on the structure of
$\boldsymbol{\mathsf{frame}}$
,
$\boldsymbol{\mathsf{layer}}$
, and
$\boldsymbol{\mathsf{painting}}$
. This is what
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
does using auxiliary proofs
${\mathsf{coh}}_{\boldsymbol{\mathsf{layer}}}$
and
${\mathsf{coh}}_{\boldsymbol{\mathsf{painting}}}$
. Even though it looks independent of the definitions from the other tables,
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
has to be proved mutually with the definitions of
$\boldsymbol{\mathsf{frame}}$
,
$\boldsymbol{\mathsf{layer}}$
,
$\boldsymbol{\mathsf{painting}}$
, and their corresponding restrictions. More precisely, for a fixed
$n$
, the block of
$\boldsymbol{\mathsf{frame}}$
,
${{\mathsf{restr}}}_{\boldsymbol{\mathsf{frame}}}$
, and
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
has to be defined in one go by induction on
$p$
. Also, each of
$\boldsymbol{\mathsf{painting}}$
,
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{painting}}}$
, and
${\mathsf{coh}}_{\boldsymbol{\mathsf{painting}}}$
is built by induction from
$p$
to
$n$
. The
$\boldsymbol{\mathsf{painting}}$
block at
$n$
relies on the
$\boldsymbol{\mathsf{frame}}$
block at
$n$
, but the converse dependency is only on lower
$n$
, so this is well-founded. Note that
$\boldsymbol{\mathsf{layer}}$
,
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{layer}}}$
, and
${\mathsf{coh}}_{\boldsymbol{\mathsf{layer}}}$
are just abbreviations. The exact way this mutual recursion is eventually formalized is explained in Section 5.4.
Commutation of
$q$
-th projection and
$r$
-th projection, or coherence conditions
Note that for a fixed constant
$n$
, relying on the evaluation rules of type theory, the coherence conditions degenerate to a reflexivity proof, so that the construction builds an effective sequence of types not mentioning coherences anymore.
5.2 Intuition for our formal construction
There is a
$\boldsymbol{\mathsf{fullframe}}$
for each dimension
$n$
, written
$\boldsymbol{\mathsf{fullframe}}^{n}$
, and every
$X_n$
is uniformly assigned a type of the form
$\boldsymbol{\mathsf{fullframe}}^{n} \rightarrow {\mathsf{HSet}}$
. Here,
$\boldsymbol{\mathsf{fullframe}}^{n}$
is a “telescope” collecting all arguments of the type of
$X_i$
in Section 4 as a nesting of
$\Sigma$
-types.
To illustrate how to recursively build
$\boldsymbol{\mathsf{fullframe}}^{n}$
, let us begin by setting
$\boldsymbol{\mathsf{fullframe}}^{0\,\triangleq } {\mathsf{unit}}$
, so that the type
${\mathsf{HSet}}$
given to
$X_0$
in Section 4 can be equivalently formulated as
${\mathsf{unit}} \rightarrow {\mathsf{HSet}}$
. Then, more generally, let each
$\boldsymbol{\mathsf{fullframe}}^{n}$
consist of
$n$
layers, written
$\boldsymbol{\mathsf{layer}}^{n,p}$
with
$p \lt n$
, that we stack in order, starting from
$\mathsf{unit}$
, and writing
$\boldsymbol{\mathsf{frame}}^{n,p}$
for the
$p$
first layers of a
$\boldsymbol{\mathsf{fullframe}}^{n}$
so that
$\boldsymbol{\mathsf{fullframe}}^{n}$
is
$\boldsymbol{\mathsf{frame}}^{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
$\mathsf{unit}$
and
$\boldsymbol{\mathsf{layer}}^{1,0}$
. Then,
$X_2$
is similarly made of two layers.
Let us now illustrate the construction of
$\boldsymbol{\mathsf{fullframe}}^{3}$
, necessary to build the type of
$X_3$
.
The figure on the left is
$\boldsymbol{\mathsf{frame}}^{3,1}$
, in the middle is
$\boldsymbol{\mathsf{frame}}^{3,2}$
, and on the right is
$\boldsymbol{\mathsf{frame}}^{3,3}$
, which is full. Further,
$\boldsymbol{\mathsf{frame}}^{3,1}$
is made of one layer,
$\boldsymbol{\mathsf{layer}}^{3,0}$
, shown as the front and back faces (blue boxes),
$\boldsymbol{\mathsf{frame}}^{3,2}$
is made of one additional layer,
$\boldsymbol{\mathsf{layer}}^{3,1}$
, shown as the left and right faces (red boxes),
$\boldsymbol{\mathsf{frame}}^{3,3}$
is made of one more layer,
$\boldsymbol{\mathsf{layer}}^{3,2}$
, shown as the top face (green box).
We illustrated here the cubical case, that is,
$\nu = 2$
; but, in general, a
$\boldsymbol{\mathsf{layer}}^{n,p}$
is a product of
$\nu$
$\boldsymbol{\mathsf{painting}}^{n-1,p}$
. A
$\boldsymbol{\mathsf{painting}}^{n,0}$
is a
$n$
-dimensional object corresponding to a filled
$\boldsymbol{\mathsf{fullframe}}^{n}$
. More generally, a
$\boldsymbol{\mathsf{painting}}^{n,p}$
is an
$n$
-dimensional object which has the form of a
$\boldsymbol{\mathsf{painting}}^{n-p,0}$
, thus of
$(n-p)$
-dimensional form, but shifted and living in dimensions
$p$
to
$n$
. Such
$\boldsymbol{\mathsf{painting}}^{n,p}$
fills a space framed by a partial
$\boldsymbol{\mathsf{frame}}^{n,p}$
so that, together, they form a filled
$\boldsymbol{\mathsf{fullframe}}^{n}$
. For instance, in the picture, each of the two
$\boldsymbol{\mathsf{painting}}^{2,0}$
of
$\boldsymbol{\mathsf{layer}}^{3,0}$
is a filled blue square, each of the two
$\boldsymbol{\mathsf{painting}}^{2,1}$
of
$\boldsymbol{\mathsf{layer}}^{3,1}$
is a line, shown as lines across the left and right faces (red lines), stretched into a partial square filling the partial frames made of respectively, the left and right border of the front-back faces (blue), and each of the two
$\boldsymbol{\mathsf{painting}}^{2,2}$
of
$\boldsymbol{\mathsf{layer}}^{3,2}$
is the point shown on the top face (green point), stretched into a partial square filling the full frames made, respectively, of the upper and lower borders of the front-back and left-right faces (blue and red squares). A
$\boldsymbol{\mathsf{painting}}^{n,p}$
complements a
$\boldsymbol{\mathsf{frame}}^{n,p}$
by adding layers needed to form a
$\boldsymbol{\mathsf{fullframe}}^{n}$
and by filling the resulting
$\boldsymbol{\mathsf{fullframe}}^{n}$
with an inhabitant of
$X_n$
. Layers are added from dimension
$n$
to dimension
$p$
, opposite to the order from
$0$
to
$p$
the
$\boldsymbol{\mathsf{frame}}^{n,p}$
are built, as shown below.
\begin{equation*} \begin{array}{lll} \boldsymbol{\mathsf{frame}}^{n,p} & {\triangleq } & \Sigma a_n: (\ldots (\Sigma {\ast }: {\mathsf{unit}} .\, \boldsymbol{\mathsf{layer}}^{n,0}) \ldots ) .\, \boldsymbol{\mathsf{layer}}^{n,p-1} \\ \boldsymbol{\mathsf{painting}}^{n,p} & {\triangleq } & \Sigma l_p: \boldsymbol{\mathsf{layer}}^{n,p}. (\ldots (\Sigma l_n: \boldsymbol{\mathsf{layer}}^{n,n-1} .\, X_n) \ldots ) \end{array} \end{equation*}
So far, we have not paid attention to the fact that we have a dependent type, shown as
$\Sigma$
. To be more precise, note that
$\boldsymbol{\mathsf{fullframe}}^{n}$
depends on all
$X_i$
up to
$n - 1$
. So, we need to package up
$X_i$
, for
$i \lt n$
, into a nesting of
$\Sigma$
-types, constituting the type of a
$n$
-truncated
$\nu$
-set, which we wrote
$\boldsymbol{\nu} \mathsf{Set}^{\lt n}$
. This allows us to give the type
$\boldsymbol{\nu} \mathsf{Set}^{\lt n} \rightarrow {\mathsf{HSet}}$
to
$\boldsymbol{\mathsf{fullframe}}^{n}$
. Then, for
$D: \boldsymbol{\nu} \mathsf{Set}^{\lt n}$
, representing an initial prefix of
$X_0, X_1, \ldots X_{n - 1}$
, the indexed set
$X_n$
has type
$\boldsymbol{\mathsf{fullframe}}^{n}(D) \rightarrow {\mathsf{HSet}}$
. Thus,
$\boldsymbol{\mathsf{frame}}^{n,p}$
,
$\boldsymbol{\mathsf{layer}}^{n,p}$
, and
$\boldsymbol{\mathsf{painting}}^{n,p}$
also depend on
$D$
. We can then reformulate the previous equation with its dependency on
$D$
. In particular,
$X_n$
is just the last component of
$D$
, that is
$D.{\mathsf{tl}}$
.
\begin{equation*} \begin{array}{lll} \boldsymbol{\mathsf{frame}}^{n,p}(D) & {\triangleq } & \Sigma a_n: (\ldots (\Sigma {\ast }: {\mathsf{unit}}.\, \boldsymbol{\mathsf{layer}}^{n,0}(D)) \ldots ) .\,\boldsymbol{\mathsf{layer}}^{n,p-1}(D) \\ \boldsymbol{\mathsf{painting}}^{n,p}(D) & {\triangleq } & \Sigma l_p: \boldsymbol{\mathsf{layer}}^{n,p}(D).\, (\ldots (\Sigma l_n: \boldsymbol{\mathsf{layer}}^{n,n-1}(D) .\, D.{\mathsf{tl}}) \ldots ) \end{array} \end{equation*}
An extra refinement arises from the fact that each new layer of a frame has to be glued onto the border of the partial frame built so far. So, each
$\boldsymbol{\mathsf{layer}}^{n,p}$
has to depend on
$\boldsymbol{\mathsf{frame}}^{n,p}$
. We also need a way to characterize the
$\nu$
borders of each
$\boldsymbol{\mathsf{painting}}^{n-1,p}$
that composes a
$\boldsymbol{\mathsf{layer}}^{n,p}$
, and this is where the restriction
${{\mathsf{restr}}}^{n,p}_{{\boldsymbol{\mathsf{frame}}},{\epsilon ,p}}$
arrives, for each
$\epsilon \lt \nu$
. For instance, in the picture, the left and right faces (red),
$\boldsymbol{\mathsf{painting}}^{2,1}$
, are laid on, respectively, the left and right borders of the front and back faces (blue), and hence need to depend on
$\boldsymbol{\mathsf{frame}}^{3,1}$
. The left and right borders of the front and back faces are then extracted as
${{\mathsf{restr}}}^{2,1}_{{\boldsymbol{\mathsf{frame}}},{L}}(D)(d)$
and
${{\mathsf{restr}}}^{2,1}_{{\boldsymbol{\mathsf{frame}}},{R}}(D)(d)$
. We can then refine again the previous equation by showing the dependencies on
$d$
, as shown below.
\begin{equation*} \begin{array}{llr} \boldsymbol{\mathsf{frame}}^{n,p}(D) & {\triangleq } & \Sigma d: (\ldots (\Sigma {\ast }: {\mathsf{unit}}.\, \boldsymbol{\mathsf{layer}}^{n,0}(D)({\ast })) \ldots ).\, \boldsymbol{\mathsf{layer}}^{n,p}(D)(d) \\ \boldsymbol{\mathsf{painting}}^{n,p}(D)(d) & {\triangleq } & \Sigma l_p: \boldsymbol{\mathsf{layer}}^{n,p}(D)(d).\, (\ldots (\Sigma l_n: \boldsymbol{\mathsf{layer}}^{n,n-1}(D)(d, l_p, \ldots , l_{n - 1}). \\ & & D.{\mathsf{tl}}(d, l_p, \ldots , l_n)) \ldots ) \\ & & \text{where } (d, l_p, \ldots , l_q) \text{ abbreviates } ((\ldots (d, l_p), \ldots ), l_q) \end{array} \end{equation*}
When
$\nu = 2$
, using
$L$
and
$R$
to represent the sides, the formation of layers from paintings amounts to:
\begin{equation*} \begin{array}{llc} \boldsymbol{\mathsf{layer}}^{n,p}(D)(d) & {\triangleq } & \boldsymbol{\mathsf{painting}}^{n-1,p}(D.{\mathsf{hd}})({{\mathsf{restr}}}^{n,p}_{{\boldsymbol{\mathsf{frame}}},{L,p}}(d)) \\ & & \times \\ & & \boldsymbol{\mathsf{painting}}^{n-1,p}(D.{\mathsf{hd}})({{\mathsf{restr}}}^{n,p}_{{\boldsymbol{\mathsf{frame}}},{R,p}}(d)) \end{array} \end{equation*}
The operation
${{\mathsf{restr}}}^{n,p}_{{\boldsymbol{\mathsf{frame}}},{\epsilon ,q}}$
restricts the
$p$
first layers of a frame, and the construction is by recursion on the structure of a frame
$d$
. This necessitates the definitions
${{\mathsf{restr}}}^{n,p}_{{\boldsymbol{\mathsf{layer}}},{\epsilon ,q}}(d)(l)$
and
${{{\mathsf{restr}}}}^{n,p}_{\boldsymbol{\mathsf{painting}},{\epsilon ,q}}(d)(c)$
, for
$l$
a
$\boldsymbol{\mathsf{layer}}$
, and
$c$
a
$\boldsymbol{\mathsf{painting}}$
. The key case is
${{{\mathsf{restr}}}}^{n,p}_{\boldsymbol{\mathsf{painting}},{\epsilon ,p}}(d)(c)$
, where
$c$
, a
$\boldsymbol{\mathsf{painting}}^{n,p}$
, necessarily has the form of
$((c_L, c_R), \_)$
. Here,
${{{\mathsf{restr}}}}^{n,p}_{\boldsymbol{\mathsf{painting}},{L,p}}$
picks out
$c_L$
, a
$\boldsymbol{\mathsf{painting}}^{n-1,p}$
,
${{{\mathsf{restr}}}}^{n,p}_{\boldsymbol{\mathsf{painting}},{R,p}}$
picks out the
$c_R$
, also a
$\boldsymbol{\mathsf{painting}}^{n-1,p}$
, and the last component, shown as
$\_$
, a
$\boldsymbol{\mathsf{painting}}^{n,p+1}$
, is discarded. There is one last difficulty, which we illustrate by writing down expected and actual types.
Given
$c_\omega$
of type
\begin{align*} c_\omega & : \boldsymbol{\mathsf{painting}}^{n,p}(D.{\mathsf{hd}})({{\mathsf{restr}}}^{n-1,p}_{{\boldsymbol{\mathsf{frame}}},{\omega ,p}}(d)) \end{align*}
${{{\mathsf{restr}}}}^{n,p}_{\boldsymbol{\mathsf{layer}},{\epsilon, q}}(d)(c_L, c_R)$
produces a layer in which the
$\omega$
-component has the type
\begin{equation*} \boldsymbol{\mathsf{painting}}^{n-2,p}(D.{\mathsf{hd}}.{\mathsf{hd}})({{\mathsf{restr}}}^{n-1,p}_{{\boldsymbol{\mathsf{frame}}},{\epsilon ,q}}({{\mathsf{restr}}}^{n,p}_{{\boldsymbol{\mathsf{frame}}},{\omega ,p}}(d))) \end{equation*}
while we expect a component of type
\begin{equation*} \boldsymbol{\mathsf{painting}}^{n-2,p}(D.{\mathsf{hd}}.{\mathsf{hd}})({{\mathsf{restr}}}^{n-1,p}_{{\boldsymbol{\mathsf{frame}}},{\omega ,p}}({{\mathsf{restr}}}^{n,p}_{{\boldsymbol{\mathsf{frame}}},{\epsilon ,q+1}}(d))) \end{equation*}
Hence, we need a coherence condition to commute the restrictions. Coherence conditions similar to this necessitate what are shown as,
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
,
${\mathsf{coh}}_{\boldsymbol{\mathsf{layer}}}$
, and
${\mathsf{coh}}_{\boldsymbol{\mathsf{painting}}}$
in Table 5. These are by induction on the structure of
$\boldsymbol{\mathsf{frame}}$
,
$\boldsymbol{\mathsf{layer}}$
, and
$\boldsymbol{\mathsf{painting}}$
. Note that, for the construction in intensional type theory, we further need a
$2$
-dimensional coherence condition,
${\mathsf{coh2}}_{\boldsymbol{\mathsf{frame}}}$
, for
${\mathsf{coh}}_{\boldsymbol{\mathsf{layer}}}$
, which is explained in the next section.
5.3 From extensional to intensional type theory
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 5.6 for the details.
The need for transport along a proof of commutation of
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{frame}}}$
in the definition of
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{layer}}}$
is made explicit in Table 6, where the arrow over
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
indicates the direction of rewrite.
$q$
-th projection of
$\mathsf{restr}$
, or faces
The proof of
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
itself requires making explicit several rewrites which were invisible in extensional type theory. The commutation of
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{layer}}}$
lives in a type referring to
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
, so we need a transport along the commutation of
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{frame}}}$
in the statement of
${\mathsf{coh}}_{\boldsymbol{\mathsf{layer}}}$
. The proof of
${\mathsf{coh}}_{\boldsymbol{\mathsf{layer}}}$
is the most involved proof of the construction, as it requires a higher-dimensional coherence condition,
${\mathsf{coh2}}_{\boldsymbol{\mathsf{frame}}}$
, whose exact formulation is as follows.
\begin{align*} \mathsf{coh}^{n-1,p}_{\boldsymbol{\mathsf{frame}},{\omega ,\theta ,r,p}}( {{{\mathsf{restr}}}^{n,p}_{\boldsymbol{\mathsf{frame}},{\epsilon ,q+2}}}(d))\;\bullet \\ {\mathsf{ap}\;} {{{\mathsf{restr}}}^{n-2,p}_{\boldsymbol{\mathsf{frame}},{\omega ,r}}}\;(\mathsf{coh}^{n,p}_{\boldsymbol{\mathsf{frame}},{\epsilon ,\theta ,q+1,p}}(d))\;\bullet \\ \mathsf{coh}^{n-1,p}_{\boldsymbol{\mathsf{frame}},{\epsilon ,\omega ,q,r}}({{{\mathsf{restr}}}^{n,p}_{\boldsymbol{\mathsf{frame}},{\theta ,p}}}(d)) = \\ {\mathsf{ap}\;} {{{\mathsf{restr}}}^{n-2,p}_{\boldsymbol{\mathsf{frame}},{\theta ,p}}}\;(\mathsf{coh}^{n,p}_{\boldsymbol{\mathsf{frame}},{\epsilon ,\omega ,q+1,r+1}}(d))\;\bullet \\ \mathsf{coh}^{n-1,p}_{\boldsymbol{\mathsf{frame}},{\epsilon ,\theta ,q,p}}({{{\mathsf{restr}}}^{n,p}_{\boldsymbol{\mathsf{frame}},{\omega ,r+1}}}(d))\;\bullet \\ {\mathsf{ap}\;} {{{\mathsf{restr}}}^{n-2,p}_{\boldsymbol{\mathsf{frame}},{\epsilon ,q}}}\;(\mathsf{coh}^{n,p}_{\boldsymbol{\mathsf{frame}},{\omega ,\theta ,r,p}}(d)) \end{align*}
where
$\mathsf{ap}$
applies a function on two sides of an equality, and
$\bullet$
is transitivity of equality. This property of equality proofs holds in
${\mathsf{HSet}}$
, and since our construction is done in
${\mathsf{HSet}}$
, the term is trivially discharged.
Notice that each
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{layer}}}$
in the type of
${\mathsf{coh}}_{\boldsymbol{\mathsf{layer}}}$
is hiding a
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
rewrite: this makes a sum total of three
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
rewrites on the left-hand side, and two
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
rewrites on the right-hand side. In the proof term of
${\mathsf{coh}}_{\boldsymbol{\mathsf{layer}}}$
,
${\mathsf{coh}}_{\boldsymbol{\mathsf{painting}}}$
has one
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
rewrite on its left-hand side. This, combined with the two terms of the form
${\mathsf{ap}\;} {\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
, matches our expectation of three
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
on the left-hand side, and two
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
on the right-hand side. Then,
${\mathsf{coh2}}_{\boldsymbol{\mathsf{frame}}}$
can be seen as expressing the commutation of these
${\mathsf{coh}}_{\boldsymbol{\mathsf{frame}}}$
terms.
Finally, let us explain
${\mathsf{coh}}_{\boldsymbol{\mathsf{painting}}}$
. The base case
$p = r$
is the key case of the commutation of
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{frame}}}$
, when one of the
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{painting}}}$
collapses, and the remaining equation holds trivially. The case of
$p \lt r$
follows the structure of
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{painting}}}$
by induction.
If we were not working in
${\mathsf{HSet}}$
, but in
${\mathsf{HGpd}}$
we would need to prove one more higher-dimensional coherence, and if we were working in
${\mathsf{Type}}$
, we would need to prove arbitrarily many higher-dimensional coherences. Here,
${\mathsf{HGpd}}$
is the subset of types
$A$
such that for all
$x$
and
$y$
in
$A$
,
$x = y$
is in
${\mathsf{HSet}}$
. See Herbelin (Reference Herbelin2015), Altenkirch et al. (Reference Altenkirch, Capriotti, Kraus, Talbot and Regnier2016), Kraus (Reference Kraus2021) for a discussion on the need for recursive higher-dimensional coherence conditions in formulating higher-dimensional structures in type theory.
5.4 Well-foundedness of the construction
Since the construction shown in the previous sections is by induction on
$n$
, and dependencies are on lower
$n$
and
$p \lt 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' \lt 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
${{{\mathsf{restr}}}}^{n}_{\boldsymbol{\mathsf{frame}}}$
depends on
$\boldsymbol{\mathsf{frame}}^{n}$
and
$\boldsymbol{\mathsf{frame}}^{n-1}$
, while
${\mathsf{coh}}^{n}_{\boldsymbol{\mathsf{frame}}}$
depends on
$\boldsymbol{\mathsf{frame}}^{n}$
,
$\boldsymbol{\mathsf{frame}}^{n-1}$
, and
$\boldsymbol{\mathsf{frame}}^{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 3, 6, and 7 but also of
$\boldsymbol{\mathsf{frame}}$
,
$\boldsymbol{\mathsf{layer}}$
,
$\boldsymbol{\mathsf{painting}}$
at levels
$n - 1$
and
$n - 2$
, as well as
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{frame}}}$
,
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{layer}}}$
, and
${{{\mathsf{restr}}}}_{\boldsymbol{\mathsf{painting}}}$
at level
$n - 1$
, together with helper equations.
5.5 Dependencies in inequality proofs
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:
Fixpoint leR (n m : nat) : SProp :=
match n, m with
| O, _ => STrue
| S n, O => SFalse
| S n, S m => leR n m
end.
Here,
${\mathsf{SProp}}$
is a definitionally proof-irrelevant impredicative universe morallyFootnote
6
living at the bottom of the universe hierarchy (Gilbert et al. Reference Gilbert, Cockx, Sozeau and Tabareau2019). By placing the definition in
${\mathsf{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:
leR_trans ?p leR_refl = ?p
leR_trans leR_refl ?p = ?p
where leR_trans is transitivity, leR_refl is reflexivity, and ?p is an existential variable. These two problems definitionally hold in
${\mathsf{SProp}}$
, but equating them does not solve the existential variable. For unification to be useful in solving existential variables, we present our first variant of
$\leq$
, which we dub as the “Yoneda variant”:
Definition leY n m :=
forall p, leR p n -> leR p m.
This definition is an improvement over leR since reflexivity is now definitionally the neutral element of transitivity, and associativity of transitivity also holds definitionally. Although it significantly eases our proof, there are some instances where unification is unable to solve the existential variables, and we have to provide them explicitly.
The second variant of
$\leq$
, the “inductive variant,” is phrased as:
Inductive leI : nat -> nat -> Type :=
| leI_refl n : n
$\texttt{<}$
~ n
| leI_down {n p} : p.+1
$\texttt{<}$
~ n -
$\texttt{>}$
p
$\texttt{<}$
~ n
where "n
$\texttt{<}$
~ m" := (leI n m) : nat_scope.
Compared to leY, leI has no proof-irrelevance properties. This definition is specially crafted for
$\boldsymbol{\mathsf{painting}}$
, where we have to reason inductively from
$p \leq n$
to
$n$
. In our usage, we have lemmas leY_of_leI and leI_of_leY in order to equip leY with the induction scheme of leI. The resulting induction scheme has computational rules holding propositionally.
5.6 Groupoid properties of equality and basic type isomorphisms
The construction relies on groupoid properties of equality, which are left implicit in Table 7. The use of the equivalence between
$u = v$
and
$\Sigma (p:u.{\mathsf{hd}} = v.{\mathsf{hd}}). (u.{\mathsf{tl}} = v.{\mathsf{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.
Commutation of
$q$
-th projection and
$r$
-th projection, or coherence conditions
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 )$
.
6. Future Work
The construction could be extended with degeneracies as well as with permutations (Grandis and Mauri Reference Grandis and Mauri2003). Dependent
$\nu$
-sets could also be defined, opening the way to construct
$\Pi$
-types and
$\Sigma$
-types of
$\nu$
-sets. A
$\nu$
-set of
$\nu$
-sets representing a universe could also be defined as sketched in a talk at the HoTT-UF workshop for the bridge case (2020). More generally, we believe these lines of work would eventually provide alternative models to parametric type theories (Cavallo and Harper, Reference Cavallo, Harper, Fernández and Muscholl2020; Nuyts et al., Reference Nuyts, Vezzosi and Devriese2017) where equality of types, now a family rather than the total space of a fibration, is not only definitionally isomorphic to bridges (Bernardy et al. Reference Bernardy, Coquand and Moulin2015), but definitionally the same as bridges.
By equipping the universe construction with a structure of equivalences, as suggested along the lines of Altenkirch and Kaposi (Reference Altenkirch, Kaposi and Uustalu2015), we also suspect the construction to be able to serve as a basis for syntactic models of various versions of cubical type theory (Angiuli et al. Reference Angiuli, Brunerie, Coquand, Harper, Hou (Favonia) and Licata2021; Bezem et al. Reference Bezem, Coquand, Huber, Matthes and Schubert2013a; Cohen et al. Reference Cohen, Coquand, Huber, Mörtberg and Uustalu2018), saving the detour via the fibered approach inherent to usual presheaf models. In particular, we conjecture being able to justify univalence holding definitionally. Our approach would also firmly ground cubical type theory in iterated parametricity.
Although prior approaches to constructing the indexed presentation of a presheaf over a direct category rely on it being evident by inspection that the fibered and indexed presentations are equivalent, no formal proof has been given, and this is a direction for future work. In our construction, we can check by computation of the first levels that it indeed computes the expected sets.
Competing interests
The authors declare none.
Appendix A. Definition of dependent stream
\begin{align*} \textit {type formation} \\ \frac {\Gamma \vdash A : {\mathsf{Type}}_m \qquad \Gamma , a:A \vdash B(a) : {\mathsf{Type}}_m \qquad \Gamma , a:A, b:B(a) \vdash f(a,b):A \qquad \Gamma \vdash u:A}{\Gamma \vdash Stream_{A,B,f}\, u : {\mathsf{Type}}_m} \\ \textit {introduction and eliminations} \\ \frac {\!\!\!\begin{array}{l}\Gamma \vdash A : {\mathsf{Type}}_m \qquad \Gamma , a:A \vdash B(a) : {\mathsf{Type}}_m \qquad \Gamma , a:A, b:B(a) \vdash f(a,b):A \qquad \Gamma \vdash u : A \\ \Gamma , a:A \vdash D(a) : {\mathsf{Type}}_m \qquad \Gamma \vdash w : D(u) \\ \Gamma , a:A, d:D(a) \vdash v(a,d) : B(a) \qquad \Gamma , a:A, d:D(a) \vdash s(a,d) : D(f(a,v(a,d))) \end{array}}{\Gamma \vdash \textsf {cofix}_{a,d,g}^{u,w}\{this:=v(a,d); next:=g(f(a,v(a,d)),s(a,d))\} : Stream_{A,B,f}\, u}\\ \frac {\Gamma \vdash t : Stream_{A,B,f}\, u}{\Gamma \vdash t.this : B(u)}\\ \frac {\Gamma \vdash t : Stream_{A,B,f}\, u}{\Gamma \vdash t.next : Stream_{A,B,f}\, f(u,t.this)} \\ \textit {computation} \\ \frac {\!\!\!\begin{array}{l}\Gamma \vdash A : {\mathsf{Type}}_m \qquad \Gamma , a:A \vdash B(a) : {\mathsf{Type}}_m \qquad \Gamma , a:A, b:B(a) \vdash f(a,b):A \qquad \Gamma \vdash u : A \\ \Gamma , a:A \vdash D(a) : {\mathsf{Type}}_m \qquad \Gamma \vdash w : D(u) \\ \Gamma , a:A, d:D(a) \vdash v(a,d) : B(a) \qquad \Gamma , a:A, d:D(a) \vdash s(a,d) : D(f(a,v(a,d))) \end{array}}{\Gamma \vdash \textsf {cofix}_{a,d,g}^{u,w}\{this:=v(a,d); next:=g(f(a,v(a,d)),s(a,d))\}.this \equiv v(u,w) : B(u)} \\ \frac {\!\!\!\begin{array}{l}\Gamma \vdash A : {\mathsf{Type}}_m \qquad \Gamma , a:A \vdash B(a) : {\mathsf{Type}}_m \qquad \Gamma , a:A, b:B(a) \vdash f(a,b):A \qquad \Gamma \vdash u : A \\ \Gamma , a:A \vdash D(a) : {\mathsf{Type}}_m \qquad \Gamma \vdash w : D(u) \\ \Gamma , a:A, d:D(a) \vdash v(a,d) : B(a) \qquad \Gamma , a:A, d:D(a) \vdash s(a,d) : D(f(a,v(a,d)))\end{array} }{\begin{array}{r}\Gamma \vdash \textsf {cofix}_{a,d,g}^{u,w}\{this:=v(a,d); next:=g(f(a,v(a,d)),s(a,d))\}.next \equiv \\ \textsf {cofix}_{a,d,g}^{f(u,v(u,w)),s(u,w)\left .\right )}\{this:=v(a,d); next:=g(f(a,v(a,d)),s(a,d))\} \\ : Stream_{A,B,f}\,f(u,v(u,w))\end{array}} \end{align*}
where
$\textsf {cofix}_{a,d,g}^{u,w}\{this:=v(a,d); next:=g(f(a,v(a,d)),s(a,d))\}$
is a notation for the instantiation on parameter
$u$
and internal value
$w$
of the corecursive definition of a stream over an arbitrary
$a$
generated by a recipe dependent on an arbitrary internal value
$d:D(a)$
with first component given by
$v(a,d)$
and second component given by
$g(f(a,v(a,d)),s(a,d))$
where
$g$
, typed as
$\Gamma , a:A, d:D(a) \vdash g(a,d): Stream_{A,B,f}\, (f(a,d))$
, formally represents the recursive call, and where
$s(a,d)$
tells how the internal value evolves.
