1. Introduction
Čubrić et al. (Reference Čubrić, Dybjer and Scott1998) propose a categorical framework using partial equivalence relations (PERs), which they termed p-category theory, to overcome obstacles of quotienting in type theory, specifically in the context of normalization for the simply typed
$\lambda$
-calculus (STLC).
The word problem for STLC is a, if not the, main problem in simple type theory. It asks when two terms are
$\beta \eta$
-convertible: that is, when does the following hold?
\begin{equation*} \Gamma \vdash t \cong _{\beta \eta } t' : \tau \end{equation*}
The well-known, and standard, solution normalizes the terms so that they may be compared (decidably) using
$\alpha$
-equivalence, reducing the problem to the following one.
\begin{equation*} \Gamma \vdash \mathsf{nf}(t) \equiv _\alpha \mathsf{nf}(t') : \tau \end{equation*}
Such a normalization function needs to produce a unique representative from the
$\beta \eta$
-conversion class; that is, a term
$\beta \eta$
-convertible with the original term. It must satisfy the following two properties, which we, respectively, call strong completeness and soundness.
\begin{equation*} \frac {\Gamma \vdash t \cong _{\beta \eta } t' : \tau }{\Gamma \vdash \mathsf{nf}(t) \equiv _\alpha \mathsf{nf}(t') : \tau } \quad \quad \frac { }{\Gamma \vdash \mathsf{nf}(t) \cong _{\beta \eta } t : \tau } \end{equation*}
Note that strong completeness only demands a canonical form for each
$\beta \eta$
-conversion class that may not necessarily be normal in any conventional sense.
The above creates a challenge for any semantical analysis of normalization functions: extensionally normalization is simply the identity, but intensionally, it needs to compute normal forms. Syntactic categorical models of the simply typed
$\lambda$
-calculus all too readily quotient the set of terms by the equivalence relation of
$\beta \eta$
-conversion, resulting in a normalization function being extensionally (a form of) the identity function and thereby being extensionally indistinguishable from the intensional identity function.
Čubrić et al. (Reference Čubrić, Dybjer and Scott1998) note that their p-category theory framework “is constructive and thus permits extraction of programs from proofs” and that it is “fundamental to extracting a normalization algorithm.” They further suggest that p-category theory “may be the appropriate way to develop category theory inside a constructive framework such as Martin-Löf type theory.” Finally, they stress “that the p-category theory we use can be formalized (programmed) in Martin-Löf type theory is one way of ensuring that our normalization function is indeed an algorithm.” We realize, as well as extend, their vision by formalizing p-category theory in Rocq and reproducing their normalization algorithm in this computational setting.
1.1 Contributions
We present a complete formalization of the normalization function of Čubrić et al. (Reference Čubrić, Dybjer and Scott1998) in Rocq. Moreover, we have formalized the full categorical freeness two-dimensional universal property for Cartesian closure (though not required for normalization) given in their work. Čubrić et al. (Reference Čubrić, Dybjer and Scott1998) prove that their normalization function is strongly complete by non-categorical means. We present here a novel universal property of unquotiented syntax that allows for a new categorical proof of strong completeness by way of Artin-Wraith gluing. Informally and intuitively, this gluing construction sits between the gluing construction of Fiore (Reference Fiore2002, Reference Fiore2022) and the work of Čubrić et al. (Reference Čubrić, Dybjer and Scott1998). All our work has been formalized in Rocq, and we present concrete Rocq definitions alongside abstract mathematical definitions.
1.2 Related work
Our work covers both category theory and normalization by evaluation for the simply typed
$\lambda$
-calculus, together with formalizations thereof. Hence, we divide our comparison and contrast with related work across these two aspects.
1.2.1 Category theory
There have been many formalizations of category theory for many proof assistants, each with their own peculiarities. We summarize a few here for some brief comparisons and contrasts.
The formalization of category theory in Rocq dates back to at least the work of Huet and Saïbi (Reference Huet, Saïbi, Plotkin, Stirling and Tofte2000), who use setoids for homs implementing e-category theory. They remark that subsetoids (for which they use the term “partial setoid”) could be used instead, thereby implementing p-category theory. However, no further observations about this direction are made.
Gross et al. (Reference Gross, Chlipala, Spivak, Klein and Gamboa2014) report on their experience formalizing category theory in Rocq. They use a variety of techniques for their library, namely, dependently typed morphisms, bundled records, and duality-centric design. We follow them by using dependently typed morphisms and bundled records.
More recently, Hu and Carette (Reference Hu and Carette2021) have implemented a category theory library for Agda. In their library, they use universe polymorphism, proof-relevant setoids, and duality-centric design. We follow them by using the universe polymorphism available in Rocq (which post-dates the work of Gross et al. (Reference Gross, Chlipala, Spivak, Klein and Gamboa2014)). Our work differs from theirs in two respects: by using proof-irrelevant subsetoids and p-category theory.
The use of these techniques in Hu and Carette (Reference Hu and Carette2021) allows for the double opposite of a category to be judgmentally equivalent with the original category rather than simply canonically categorically equivalent. Our adoption of strict propositions in Rocq provides this judgmental equivalence (and many others) for “free,” and as such, we do not extensively use duality-centric design.
Univalent category theory has also seen formalization efforts in both Rocq and Agda such as the work of Bauer et al. (Reference Bauer, Gross, Lumsdaine, Shulman, Sozeau and Spitters2017). These formalizations, embracing the homotopical interpretation of type theory, allow for the assertion of axioms that are validated in their intended models when these principles are not provided by the respective proof assistant. For example, function extensionality follows from the univalent setting, and thus, Bauer et al. (Reference Bauer, Gross, Lumsdaine, Shulman, Sozeau and Spitters2017) assume it as an axiom. Our approach avoids the assumption of such axioms by explicitly tracking the uses of extensionality locally instead of assuming it as a global principle.
Category theory has also been formalized by The Mathlib Community (2020) in a nonconstructive setting making use of quotients. Their use of quotients rather than setoids contrasts heavily with our work.
1.2.2 Normalization
Normalization of STLC terms has two varieties: reduction-free and reductional. The latter arises from the perspective of viewing STLC as a rewrite system, with a rewriting theory. This work focuses on the former, which has been studied most successfully using Normalization by Evaluation (NbE). We consider here only other work on simple type theories, rather than non-simple type theories containing polymorphism, type constructors, or dependent types.
NbE has its roots in the work of Berger and Schwichtenberg (Reference Berger and Schwichtenberg1991). Their work was partially categorified by Altenkirch et al. (Reference Altenkirch, Hofmann, Streicher, Pitt, Rydeheard and Johnstone1995); however, that work still made use of ad hoc non-categorical techniques in order to overcome the intension versus extension problem: “the […] normalization function only works on equivalence classes and is hence extensionally equal to the identity. We introduce normal form objects to overcome this problem.” Fiore (Reference Fiore2002, Reference Fiore2022) further categorified NbE to fully use Artin-Wraith gluing, rather than the ad hoc twisted gluing technique of Altenkirch et al. (Reference Altenkirch, Hofmann, Streicher, Pitt, Rydeheard and Johnstone1995). These categorifications, ultimately, relied upon the syntactic notions of neutral and normal forms in order to state the algorithm and prove its correctness. The use of p-category theory in the work of Čubrić et al. (Reference Čubrić, Dybjer and Scott1998) partially obviates the need for such syntactic considerations, since characterizing the resultant forms as normal inevitably requires the notions of normal and neutral forms. They only prove some of the correctness properties given in Fiore (Reference Fiore2002, Reference Fiore2022) categorically and resort to non-categorical techniques for other proofs.
Kovács (Reference Kovács2017) formalizes and proves correctness properties of NbE in Agda, although minimally connecting to category theory. In discussion on formalizing strong completeness, Kovács (Reference Kovács2017) notes that PERs could be used in the formalization but that this was found to be too inconvenient. This contrasts with the work of Čubrić et al. (Reference Čubrić, Dybjer and Scott1998) and our work, which centers on the use of PERs. In fact, we believe that the categorical nature of Čubrić et al. (Reference Čubrić, Dybjer and Scott1998), which we inherit, overcomes to a certain extent the inconvenience experienced by Kovács (Reference Kovács2017). The structured framework of our categorical development guides precisely all that needs to be formalized and provides an interface for abstract reasoning: once a categorical structure has been instantiated, all general properties of the categorical structure are available at once, and instantiating the categorical structure is often much easier than proving the desired properties for specific concrete instances.
1.3 Organization
In Section 2, we present basic definitions in p-category theory from both a pen-and-paper perspective and the perspective of the Rocq formalization. Moreover, in Section 3, we present definitions of p-category theory relevant for the p-categorical analysis of the simply typed
$\lambda$
-calculus. In Section 4, we describe our formalization of the simply typed
$\lambda$
-calculus. In Section 5, we connect the p-categorical definitions with the simply typed
$\lambda$
-calculus, and in Section 6, we define the normalization function with two correctness properties. Finally, in Section 7, we summarize our work and results and suggest avenues for further work.
2. p-Category Theory
p-Category theory is a form of category theory first proposed in the work of Čubrić et al. (Reference Čubrić, Dybjer and Scott1998) to allow the separation of intensional and extensional behavior for the extraction of a normalization algorithm. Their choice of p-category theory over e-category theory was motivated by a separation of “data parts” from “property parts.” Interestingly, this separation has some profound implications when comparing and contrasting completeness with cocompleteness. In e-category theory, completeness and cocompleteness in the e-category of e-sets are achieved by distinct strategies: the former by
$\Sigma$
-types and the latter by the equivalence relations associated to setoids. However, in p-category theory, completeness and cocompleteness in the p-category of p-sets are both achieved by the same strategy, namely, by that of the PERs associated with subsetoids.
Although p-category theory can be given a formal categorical foundation by considering a form of enrichment, in this paper, we follow a direct, and more practical and applied, presentation.
2.1 p-Sets
We give some definitions for the PER setting. These basic constructions provide a flavor of the theory of p-sets.
Definition 2.1.1 (PER). A PER is a symmetric and transitive relation.
We use the addition of strict propositions by Gilbert et al. (Reference Gilbert, Cockx, Sozeau and Tabareau2019) to Rocq for the valuation of our PERs: this amounts to the Rocq definition in Listing 2.1.1 .
PER Rocq Definition.
Definition 2.1.2 (PType). In the Rocq formalization, we define a record PType that bundles together a (carrier/underlying) type with a PER over the given type.
By abuse of notation facilitated in Rocq by a coercion, we will identify any given PType with its underlying carrier type. However, when we wish to emphasize that we are referring to the underlying carrier type (rather than the whole PType structure), we will use vertical bars around the name of the PType. Furthermore, we will denote the associated PER by
$\sim$
, sometimes with a disambiguating subscript.
Construction 2.1.3 (Discrete PType). Any Rocq type,
$A$
, has an associated discrete PType,
$A_=$
, where:
-
•
$|A_=| \triangleq A$
; and -
•
$a \sim a' \triangleq a = a'$
.
Construction 2.1.4 (PUnit). The unit PType has a single, self-related element. This is implemented by using the unit type for the underlying type and the terminal strict proposition for the associated PER.
Construction 2.1.5 (PProd). The product of two PTypes,
$A$
and
$B$
, is given by the following data:
-
•
$| A \times B | \triangleq |A| \times |B|$
; and -
•
$(a, b) \sim _{A \times B} (a', b') \triangleq a \sim _A a' \wedge b \sim _B b'$
.
Construction 2.1.6 (PArr). The exponential of two PTypes,
$A$
and
$B$
, is given by the following data:
-
•
$| A \rightarrow B | \triangleq |A| \rightarrow |B|$
; and -
•
$f \sim _{A \rightarrow B} f' \triangleq \forall {a\, a'}. \, a \sim _A a' \Rightarrow f \, a \sim _B f' \, a'$
.
Note that partiality lends itself to using the logical definition of when two functions are related. Such a definition dates as far back as Gandy (Reference Gandy1956); see also Hyland (Reference Hyland, Cooper and Hodges2016).
Remark. The partiality afforded by omitting reflexivity offers some advantages over the setting with equivalence relations. To appreciate why this is the case, consider that when using setoids/equivalence relations, subtypes can only be formed by changing the underlying type to an appropriate
$\Sigma$
-type to restrict by the desired property. This mixes computational data (the base of the
$\Sigma$
-type) with a formalization property (the fiber of the
$\Sigma$
-type). This lack of separation was already noticed by Salvesen and Smith (Reference Salvesen and Smith1988). On the other hand, when using subsetoids/PERs, subtypes are trivially achieved by restricting both sides of the relation by the desired property. This leaves the representing type of the computational data unmodified: a fact not true in the setoid and univalent settings. This also ensures that proofs of logical properties have no bearing on the construction of computational data and not by a restriction on the elimination of inductively defined strict propositions but by the very structure of the formalization.
Construction 2.1.7 (Sub-p-Sets). Given a p-set,
$A$
, and a predicate on the elements of the underlying type of
$A$
,
$P : |A| \rightarrow \Omega$
, where
$\Omega$
in the Rocq formalization is SProp, one can form the sub-p-set,
$A\!\!\restriction _P$
, where self-related elements must also satisfy
$P$
, by the following:
-
•
$|\,A\!\!\restriction _P| \triangleq |A|$
; and -
•
$a \sim _{A\restriction _P} a' \triangleq$
-
–
$a \sim _A a' \quad \wedge$
-
–
$P\, a \hphantom {a \sim _A a'}\! \wedge$
-
–
$P\, a'$
.
-
2.2 Basic p-categorical definitions
We give a number of basic definitions for p-category theory. These largely replicate the definitions found in e-category theory and standard mathematical accounts of category theory; however, there are a few deviations to account for the PER setting used for p-category theory.
Definition 2.2.1 (PCat). The definition of p -categories, found in Listing 2.2.1 , is much the same as standard definitions found in the literature.
There are a few key differences due to the p-setting, which we bring to the attention of the reader:
-
• the type of homs is valued in PType;
-
• the identity arrow must be self-related; and
-
• the associativity and unit laws are phrased logically so as not to assume reflexivity.
Note that the latter two are particular to the p-setting; that is, they have no analogue in the e-setting.
p-Category Rocq Definition.
Construction 2.2.2 (Opposite p-Category). The definition of a p-category admits the standard construction of taking the opposite of a category.
Construction 2.2.3 (Product p-Category). The definition of a p-category admits the standard construction of taking the product of two categories.
Construction 2.2.4 (PSet). The p-category, PSet, has as objects PTypes and has as homs the PArr of the domain and codomain PTypes.
Definition 2.2.5 (IsPIso). A morphism,
$f : c \rightarrow d$
, is a p
-isomorphism when there exists another morphism,
$f^{-1} : d \rightarrow c$
, such that:
-
•
$f \sim f$
; -
•
$f^{-1} \sim f^{-1}$
; -
•
$f \circ f^{-1} \sim \operatorname{id}_d$
; and
-
•
$f^{-1} \circ f \sim \operatorname{id}_c$
.
The Rocq definition can be found in Listing A.1 .
Definition 2.2.6 (PFun). The definition of p -functors, found in Listing 2.2.2 , proceeds almost as straightforwardly as the definition of a p -category.
Much like the associativity and unit laws for p-categories, the composition law for p-functors requires extra hypotheses in order to account for the logical nature of the p-setting.
p-Functor Rocq Definition.
Definition 2.2.7.
-
• (p -Functor Fullness) A p -functor,
$F : \mathbb{C} \rightarrow \mathbb{D}$
, is p
-full when it supports:
\begin{equation*} \textstyle \prod _{x\,y : \mathbb{C}}\prod _{f : F\,x \rightarrow F\,y}\,f \sim f \Rightarrow \sum _{g : x \rightarrow y}\, g \sim g \wedge F\,g \sim f . \end{equation*}
-
• ( p -Functor Essential Surjectivity) A p -functor,
$F : \mathbb{C} \rightarrow \mathbb{D}$
, is p
-essentially surjective when it supports:
\begin{equation*} \textstyle \prod _{d : \mathbb{D}}\sum _{c : \mathbb{C}}\, F\,c \cong d . \end{equation*}
Note that we use a proof-relevant
$\Sigma$
-type rather than a proof-irrelevant mere existence quantification.
Construction 2.2.8 (PHomFun). Every p-category,
$\mathbb{C}$
, has a p-functor mapping two objects to the p-set of morphisms there between:
\begin{equation*} \operatorname{Hom}_{\mathbb{C}} : \mathbb{C}^{\mathsf{op}} \times \mathbb{C} \rightarrow \mathsf{PSet} . \end{equation*}
Definition 2.2.9 (IsPNatural). A transformation,
\begin{equation*}\textstyle \alpha : \prod _{c : \mathbb{C}} \operatorname{Hom}_{\mathbb{D}}(F \, c, G \, c) , \end{equation*}
is p -natural precisely when:
\begin{equation*}\textstyle \forall {x \, y : \mathbb{C}}. \, \forall {f \, f' : x \rightarrow y}. \, f \sim f' \Rightarrow (\alpha _y \circ F \, f) \sim (G \, f' \circ \alpha _x) . \end{equation*}
Definition 2.2.10 (PNatTrans). The definition of p -natural transformations, found in Listing 2.2.3 , is again a relatively mechanical translation of the ordinary definition into the p -setting.
p-Natural Transformation Rocq Definition.
2.3 p-Functor categories
It would seem that we are now able to define easily the notion of p-functor category: the objects are p-functors and the morphisms are p-natural transformations. However, the situation for p-functor categories is not as straightforward as the other p-categorical definitions we have seen hitherto. Indeed, here we find the first opportunity for the p-setting to show its utility, rather than its encumbrances. As with any p-category, to define p-functor categories, we have to consider how to relate the elements of the hom p-sets. Embracing partiality sheds new light on how to define p-functor categories.
Definition 2.3.1 (p-Functor Categories). p -Functor categories have p -functors as objects. The hom p -sets have all transformations as the underlying type, but relating only those transformations that are p -natural.
Two morphisms,
$\alpha$
and
$\beta$
, in a p
-functor category are related precisely when:
-
•
$\alpha$
and
$\beta$
are both p
-natural; and
-
•
$\alpha$
and
$\beta$
are componentwise related:
$\forall x. \, \alpha _x \sim \beta _x$
.
Remark. The above definition is the same as that given by Čubrić et al. (Reference Čubrić, Dybjer and Scott1998). We note that the first two conjuncts imply each other in the presence of the third one. Nevertheless, there is a simpler, and in our experience superior, equivalent definition. Transformations,
$\alpha$
and
$\beta$
of type
$F \Rightarrow G$
, are related precisely when:
-
•
$\forall x\, y\, f\, f'. \, f \sim f' \Rightarrow \alpha _y \circ F \, f \sim G \, f' \circ \beta _x$
; and -
•
$\forall x. \, \alpha _x \sim \beta _x$
This definition, having fewer constituent parts, simplifies the formalization and diminishes some of the inconvenience of using PERs, while maintaining the elegance of an unbiased symmetric definition.
Construction 2.3.2 (Presheaf p-Categories). The presheaf p-category,
$\widehat {\mathbb{C}}$
, of a p-category,
$\mathbb{C}$
, is the p-functor category,
$[\mathbb{C}^{\mathsf{op}}, \mathsf{PSet}]$
, from the opposite of
$\mathbb{C}$
to PSet.
Construction 2.3.3 (Sub-p-Presheaves). Construction 2.1.7 can be extended to form sub-p-presheaves. Given the following data:
-
•
$F : \widehat {\mathbb{C}}$
; and -
•
$P : \prod _{c : \mathbb{C}^{\mathsf{op}}}{F\,c \rightarrow \Omega }$
; such that -
•
$\forall \, x\, y\, f\, f'\, a\, a'. P_y\, a \wedge P_y\, a' \wedge a \sim _{F_y} a' \wedge f \sim f' \Rightarrow P_x\, (F_1\, f\, a) \wedge P_x\, (F_1\, f'\, a')$
;
one may form the sub-p-presheaf
$F\!\restriction _P : \widehat {\mathbb{C}}$
so that
$(F\!\restriction _P)(c) \equiv (F\,c)\!\!\restriction _{P\,c}$
.
Construction 2.3.4 (Nerve p-Functors). Any p-functor,
$F : \mathbb{C} \rightarrow \mathbb{D}$
, induces a p-functor:
\begin{equation*} \langle F \rangle : \mathbb{D} \rightarrow \widehat {\mathbb{C}} ; \end{equation*}
where
\begin{equation*} \langle F \rangle (d)(c) \triangleq \operatorname{Hom}_{\mathbb{D}}(F(c), d) . \end{equation*}
Construction 2.3.5 (Yoneda p-Functor). The Yoneda p-functor embeds a p-category,
$\mathbb{C}$
, into its p-category of presheaves:
\begin{equation*} y : \mathbb{C} \rightarrow \widehat {\mathbb{C}} . \end{equation*}
It is the nerve of the identity p-functor.
2.4 p-Comma categories
We define comma p-categories. Their definition requires careful adaptation for the p-setting. Partiality has a subtle effect on the definition of comma p-categories. Since not all morphisms are self-related, one needs to ensure that the morphism contained within the objects of comma p-categories is self-related.
Definition 2.4.1 (Comma p-Categories). The objects of the comma p
-category,
$F \downarrow G$
, for
$F : \mathbb{B} \rightarrow \mathbb{D}$
and
$G : \mathbb{C} \rightarrow \mathbb{D}$
, contain the following:
-
•
$b : \mathbb{B}$
; -
•
$c : \mathbb{C}$
; -
•
$f : F\,b \rightarrow G\,c$
; such that
-
•
$f \sim f$
.
The underlying type of the morphisms of the comma p
-category,
$(b_1, c_1, f_1) \rightarrow (b_2, c_2, f_2)$
, contains the following:
-
•
$g : b_1 \rightarrow b_2$
; and
-
•
$h : c_1 \rightarrow c_2$
.
The PER on these morphisms relates
$(g, h) \sim (g', h')$
precisely when the following holds:
-
•
$g \sim g' : b_1 \rightarrow b_2$
; -
•
$h \sim h' : c_1 \rightarrow c_2$
; and
-
•
$f_2 \circ F(g) \sim G(h') \circ f_1 : F\,b_1 \rightarrow G\,c_2$
.
Construction 2.4.2 (Comma p-Category Projection p-Functors). Comma p-categories,
$F \downarrow G$
, for
$F : \mathbb{B} \rightarrow \mathbb{D}$
and
$G : \mathbb{C} \rightarrow \mathbb{D}$
, have two projection p-functors:
-
•
$\operatorname{Dom} : F \downarrow G \rightarrow \mathbb{B}$
; and -
•
$\operatorname{Cod} : F \downarrow G \rightarrow \mathbb{C}$
.
Construction 2.4.3 (Induced p-Functors into p-Comma Categories). One may induce a p-functor from a p-category,
$\mathbb{B}$
, into a p-comma category,
$(F \downarrow G)$
, where
$F : \mathbb{C} \rightarrow \mathbb{E}$
and
$G : \mathbb{D} \rightarrow \mathbb{E}$
, by the following data:
-
• a p-functor,
$H : \mathbb{B} \rightarrow \mathbb{C}$
; -
• a p-functor,
$K : \mathbb{B} \rightarrow \mathbb{D}$
; and -
• a p-natural transformation,
$\alpha : F \circ H \Rightarrow G \circ K$
.
We denote such induced p-functors by
$\langle H \downarrow _\alpha K \rangle$
; we may drop the subscript
$\alpha$
if it is evident from the context.
2.5 p-Set-valued (Co)Ends
We define how to construct (p-)ends and (p-)coends over the p-category of p-sets. The p-setting is crucial for producing definitions that will exhibit good computational behavior.
Definition 2.5.1 (p-Set-Valued End). The end of a p
-functor,
$F : \mathbb{C}^{\mathsf{op}} \times \mathbb{C} \rightarrow \mathsf{PSet}$
, is given by
-
•
$\left | \int _{c : \mathbb{C}}{ F (c, c) } \right | \triangleq \prod _{c : \mathbb{C}}{ F (c, c) }$
; and
-
•
$w \sim w' \triangleq$
-
–
$\forall {x\, y}.\, \forall {f\, f' : x \rightarrow y}.\,{ f \sim f' \Rightarrow F \, (\,f, \mathsf{id}) \, (w\hphantom {{}'} \, y) \sim F \, (\mathsf{id}, f') \, (w\hphantom {{}'} \, x)} \quad \wedge$
-
–
$\forall {x\, y}.\, \forall {f\, f' : x \rightarrow y}.\,{ f \sim f' \Rightarrow F \, (\,f, \mathsf{id}) \, (w' \, y) \sim F \, (\mathsf{id}, f') \, (w' \, x)} \quad \wedge$
-
–
$\forall {z}.\,{w \, z \sim w' \, z}$
.
-
Remark. The definition of ends for p-sets uses well the partiality afforded by PERs. Indeed, it was in defining ends for p p-sets that we first began to appreciate the importance of using partiality. The first two conjuncts in the definition of the PER specify that the two wedges should be dinatural, and the third conjunct requires that the two wedges agree up to the relevant PER. Similarly to the definition of the PER for p-functor category homs, note that the first two conjuncts imply each other in the presence of the third one.
Definition 2.5.2 (p-Set-Valued Coend). The coend of a p
-functor,
$F : \mathbb{C}^{\mathsf{op}} \times \mathbb{C} \rightarrow \mathsf{PSet}$
, is given by
-
•
$\left | \int ^{c : \mathbb{C}}{ F (c, c) } \right | \triangleq \sum _{c : \mathbb{C}}{ F (c, c) }$
; and
-
•
$w \sim w'$
is inductively generated by the following:
-
–
$\forall {z}.\, \forall {s\, s' : F \, (z, z)}.\,{ s \sim s' \Rightarrow (z;\; s) \sim (z;\; s') }$
; -
–
$\forall {x\, y}.\, \forall {f\, f' : y \rightarrow x}.\, \forall {s\, s' : F \, (x, y)}.\,{f \sim f' \Rightarrow s \sim s' \Rightarrow (y;\; F\,(\,f, \mathsf{id}) \, s) \sim (x;\; F\,(\mathsf{id}, f') \, s')}$
; -
–
$\forall {x\, y}.\, \forall {f\, f' : y \rightarrow x}.\, \forall {s\, s' : F \, (x, y)}.\,{f \sim f' \Rightarrow s \sim s' \Rightarrow (x;\; F\,(\mathsf{id}, f) \, s) \sim (y;\; F\,(\,f', \mathsf{id}) \, s')}$
; and
-
–
$w_1 \sim w_2 \wedge w_2 \sim w_3 \Rightarrow w_1 \sim w_3$
.
-
Remark. The definition of ends and coends for p-sets emphasizes the advantage that p-sets have over e-sets, and even quotient inductive types in univalent foundations: they leave the underlying computational structure unmodified. They therefore offer a cleaner setting for distinguishing computational data from logical properties. We believe that such a clean distinction is likely to have advantages for the extraction of algorithms in proof-relevant settings.
3. p-Categorical Structure
We now define p-categorical structure required for describing simply typed syntax p-categorically. We cover this in three subsections: the definition of finite limits, the definition of Cartesian-closed structure, and the definition of Cartesian-pre-closed structure. This latter structure is a novel definition needed for our p-categorical analysis of unquotiented STLC syntax.
Čubrić et al. (Reference Čubrić, Dybjer and Scott1998) define the categorical notions of p-terminal object, p-Cartesian product, and p-Cartesian exponential in an equational style: they specify the object-forming and morphism-forming operations and the p-equations that they should satisfy. We adopt a different approach by only asking for an object-forming operation together with an adjointness property that it should satisfy. This category-theoretic approach gives further confidence in the correctness of the p-categorical definition; indeed, we recover all of the properties given by Čubrić et al. (Reference Čubrić, Dybjer and Scott1998), thus connecting their definition with ours.
3.1 Finite p-limits
We define the following limits in p-category theory, thus defining all finite limits: terminal objects, Cartesian products, and equalizers.
Definition 3.1.1 (Terminal Object). A terminal object in a p
-category is an object
$\top$
such that the following p
-isomorphism is p
-natural in
$x$
.
\begin{equation*} \operatorname{Hom}_{\mathbb{C}}(x, \top ) \cong \Delta _{\texttt {PUnit}} \end{equation*}
That is, the p -set of morphisms into the terminal object is a terminal p -set (up to p -equivalence). This is straightforwardly phrased in Rocq in Listing 3.1.1 , where PBiFunPartialRight constructs a p -functor from a p -functor out of a product p -category by fixing the second argument to be the specified object, PConstFun produces a constant p -functor out of the terminal category, and PTermFun is the unique p -functor into the terminal category.
p-Terminal Object Rocq Definition.
Definition 3.1.2 (Cartesian Product). A p
-category has Cartesian products when it has a binary operation on objects
$- \, \times =$
such that the following family of p
-isomorphisms are p
-natural in
$x$
.
\begin{equation*} \operatorname{Hom}_{\mathbb{C}}(x, a \times b) \cong \operatorname{Hom}_{\mathbb{C}\times \mathbb{C}}((x, x), (a, b)) : \langle - , = \rangle \end{equation*}
Moreover, we denote the projection maps as follows:
\begin{align*} \pi _1 : a \times b \rightarrow a , \quad \pi _2 : a \times b \rightarrow b . \end{align*}
This is translated into Rocq in Listing 3.1.2 .
p-Cartesian Product Rocq Definition.
Definition 3.1.3 (Cartesian p-Category). A p -category is a Cartesian p -category when it has both a terminal object and Cartesian products. This is rendered in Rocq in Listing A.2 .
Definition 3.1.4 (Cartesian p-Functor). A p -functor between Cartesian p -categories is a Cartesian p -functor when it preserves, up to p -isomorphism, both the terminal object and the Cartesian products. We denote the inverse to the canonical map for products by the following:
\begin{equation*} p : \left ( F\,a \times F\,b \right ) \stackrel {{\scriptsize \sim }}{\rightleftarrows } F(a \times b) : \langle F\,\pi _1, F\,\pi _2 \rangle . \end{equation*}
This is rendered in Rocq in Listing A.3 .
Lemma 3.1.5 (Cartesian Comma p-Categories). Comma p
-categories,
$(F \downarrow G)$
, where
$F : \mathbb{B} \rightarrow \mathbb{D}$
and
$G : \mathbb{C} \rightarrow \mathbb{D}$
, are p
-Cartesian whenever
$\mathbb{B}$
,
$\mathbb{C}$
, and
$\mathbb{D}$
are Cartesian p
-categories, and
$G$
is a Cartesian p
-functor.
Definition 3.1.6 (p-Equalizers). A p -category has p -equalizers when it has an operation
\begin{equation*} \textstyle \operatorname{eq}\{-, =\} : \prod _{a\, b : \mathbb{C}} \prod _{f\, g : a \rightarrow b} f \sim f \rightarrow g \sim g \rightarrow \mathbb{C} \end{equation*}
such that the following family of p
-isomorphisms are p
-natural in
$x$
.
\begin{equation*} \textstyle \operatorname{Hom}_{\mathbb{C}}(x, \operatorname{eq}\{f, g\}) \cong \{h : \operatorname{Hom}_{\mathbb{C}}(x, a) \,|\, f \circ h \sim g \circ h\} \end{equation*}
The p
-functor defined on the right is a sub-
p
-presheaf of the p
-presheaf
$y(a)$
. We therefore use the machinery of construction 2.3.3 for defining sub-
p
-presheaves to define this p
-functor. This definition is rendered in Rocq in Listing 3.1.3
, where PSubSetFun implements construction 2.3.3 and requires an argument establishing the well-definedness of the subset predicate which we omit.
p-Equalizers Rocq Definition.
Remark. Note that the object-forming operation for p-equalizers requires that the two p-morphisms are self-related. This is required so that the operation extends to a p-functor out of a certain p-comma category. Since we use SProp in our Rocq formalization, these proofs of self-relation have no computational content, and so we omit them by abuse of notation.
Definition 3.1.7 (Lex p-Category). A Cartesian p -category is a lex p -category when it has equalizers.
3.2 p-Cartesian-closed structure
We define Cartesian closure in the p-categorical setting.
Definition 3.2.1 (Cartesian Exponential). A Cartesian p
-category has Cartesian exponentials when it has a binary operation on objects
$(-)^{(=)}$
such that the following family of p
-isomorphisms are p
-natural in
$x$
.
\begin{equation*} \operatorname{Hom}_{\mathbb{C}}(x, b^a) \cong \operatorname{Hom}_{\mathbb{C}}(x \times a, b) : (-)^\ast \end{equation*}
The notation
$a \Rightarrow b$
may also be used instead of
$b^a$
. Moreover, we denote the evaluation map as follows:
\begin{equation*} \varepsilon : b^a \times a \rightarrow b . \end{equation*}
This definition is translated into Rocq in Listing 3.2.1 .
p-Cartesian Exponential Rocq Definition.
Definition 3.2.2 (Cartesian-Closed p-Category). A Cartesian p -category is a Cartesian-closed p -category when it has Cartesian exponentials. This is rendered in Rocq in Listing A.4 .
Definition 3.2.3 (Lex-Closed p-Category). A Cartesian p -category is a lex-closed p -category when it has equalizers and Cartesian exponentials.
Lemma 3.2.4 (PSet Cartesian Closure). The p -category PSet is Cartesian-closed with the terminal object being given by PUnit, with the Cartesian product being given by PProd, and with the Cartesian exponential being given by PArr.
Lemma 3.2.5 (p-Presheaves Cartesian Closure). The p -category of presheaves is Cartesian-closed with the terminal object being the constant presheaf on PUnit and the Cartesian product being given pointwise. The Cartesian exponential in presheaves is involved but standard.
Definition 3.2.6 (Cartesian-Closed p-Functor). A Cartesian p -functor between Cartesian-closed p -categories is a Cartesian-closed p -functor when it preserves, up to p -isomorphism, the Cartesian exponentials. We denote the inverse to the canonical map by the following:
\begin{equation*} e : \left ( F\,a \Rightarrow F\,b \right ) \stackrel {{\scriptsize \sim }}{\rightleftarrows } F(a \Rightarrow b) : (F\,\varepsilon \circ p)^\ast . \end{equation*}
This is rendered in Rocq in Listing A.5 .
Lemma 3.2.7 (Nerve Cartesian-Closed p-Functor). Any nerve p -functor from a Cartesian p -category is a Cartesian p -functor, and the nerve of any Cartesian, essentially surjective, and full p -functor is a Cartesian-closed p -functor. In particular, the Yoneda p -functor is a Cartesian-closed p -functor.
Lemma 3.2.8 (Cartesian-Closed Gluing p-Categories). Gluing p
-categories, which are comma p
-categories
$(\operatorname{Id}_{\mathbb{D}} \downarrow F)$
for
$F : \mathbb{C} \rightarrow \mathbb{D}$
, are Cartesian-closed whenever
$\mathbb{C}$
is a Cartesian-closed p
-category,
$\mathbb{D}$
is a lex-closed p
-category, and
$F$
is a Cartesian p
-functor.
3.3 p-Cartesian-pre-closed structure
We define Cartesian-pre-closure in the p-categorical setting. This definition accounts for the structure of unquotiented syntax with its lack of equations for exponential-like structure. We give a number of constructions, based on Cartesian-pre-closed structure, that we shall need for our normalization algorithms.
Definition 3.3.1 (Cartesian Pre-Exponential). A Cartesian p
-category has Cartesian pre-exponentials when it has a binary operation on objects
$(-)^{(=)}$
together with a chosen pair of maps p
-natural in
$x$
as follows:
\begin{equation*} \operatorname{Hom}_{\mathbb{C}}(x, b^a) \mathrel {\rightleftarrows } \operatorname{Hom}_{\mathbb{C}}(x \times a, b) : (-)^\ast . \end{equation*}
The notation
$a \Rightarrow b$
may also be used instead of
$b^a$
. Moreover, we denote the pre-evaluation map as follows:
\begin{equation*} \tilde {\varepsilon } : b^a \times a \rightarrow b . \end{equation*}
Remark. The definition of Cartesian pre-exponentials is an extreme weakening of the definition of Cartesian exponentials that does not require the two maps to be inverses of each other. This allows one to replicate the object-forming and morphism-forming structure of Cartesian exponentials in the absence of any of the equations establishing the
$\beta$
-laws and
$\eta$
-laws.
Definition 3.3.2 (Cartesian-Pre-Closed p-Category). A Cartesian p -category is a Cartesian-pre-closed p -category when it has Cartesian pre-exponentials.
Definition 3.3.3 (Cartesian-Pre-Closed p-Functor). A Cartesian p -functor from a Cartesian-pre-closed p -category to a Cartesian-closed p -category is a Cartesian-pre-closed p -functor when it has the following structure and properties:
-
•
$\tilde {e} : (F\,b)^{(F\,a)} \rightarrow F\,(b^a)$
; such that
-
•
$\tilde {e} \sim \tilde {e}$
; and
-
•
$ (\,f \sim g : x \times a \to b) \Rightarrow (\tilde {e} \circ (F\,f \circ p)^\ast \sim F\,(g^\ast ) : F\,x\to F\,(b^a))$
.
Remark. The notion of Cartesian-pre-closed p-functor is an appropriate weakening of the notion of Cartesian-closed p-functor to the setting of having a Cartesian pre-closed domain category.
Note that the definition of Cartesian-pre-closed p-functors is heterogeneous: the structure of the domain and codomain p-categories are different. They are therefore not composable. Although we do have the following lemma.
Lemma 3.3.4. The composition of a Cartesian-closed p -functor after a Cartesian-pre-closed p -functor is a Cartesian-pre-closed p -functor.
Lemma 3.3.5 (Nerve Cartesian-Pre-Closed p-Functor). The nerve of any Cartesian and essentially surjective p -functor is a Cartesian-pre-closed p -functor. In particular, the Yoneda Cartesian p -functor is a Cartesian-pre-closed p -functor.
Lemma 3.3.6.
For
$\mathbb{B}$
a Cartesian-pre-closed p
-category,
$\mathbb{C}$
a Cartesian-closed p
-category,
$\mathbb{D}$
a lex-closed p
-category,
$H : \mathbb B \to \mathbb D$
and
$K : \mathbb{B} \rightarrow \mathbb{C}$
Cartesian-pre-closed p
-functors, and
$F : \mathbb{C} \rightarrow \mathbb{D}$
a Cartesian p
-functor, if
$\alpha : H \Rightarrow F \circ K$
lifts the Cartesian-pre-closure of
$H$
and
$K$
as in Figure
1
, then the p
-functor
$\langle H \downarrow _\alpha K \rangle : \mathbb{B} \to (\operatorname{Id}_{\mathbb{D}} \downarrow F)$
induced following construction 2.4.3 is Cartesian-pre-closed.
Lifting of Cartesian-pre-closure to induced p-functors into comma p-categories.
4. Simply Typed Syntax
We formalize the syntax of STLC in the well-scoped and well-typed style afforded by inductive families in Rocq. There have been many expositions on the formalization of syntax in proof-assistants for simply typed calculi. We mainly follow the work of Benton et al. (Reference Benton, Hur, Kennedy and McBride2012) by using renamings and substitutions. In their work, they use functional representations for renamings and substitutions and are forced to assume the axiom of function extensionality in Rocq – forfeiting canonicity of their formalization – to prove many properties about their representation. An alternative approach to using a functional representation is to use explicit lists to represent renamings and substitutions. This representation has the advantage that it permits inductive reasoning more straightforwardly, at the cost of complicating the definitions of composition and proof of associativity which the functional representation gives “for free.” We use the list representation for the sake of inductive reasoning; however, had we adopted the functional approach, we would not have been required to assume function extensionality as working in the p-setting allows us to choose our (partial) equivalence relation for which we could have selected extensional equality.
4.1 Types and syntax
We work in the simply typed setting with a single base type.
Definition 4.1.1 (Ty). The set of types is given by the grammar
\begin{equation*} T ::= \iota \mid T\to T , \end{equation*}
and inductively defined in the Rocq Listing A.6 .
Contexts are lists of types. We denote the empty context as
$\bullet$
, and context extension with a comma, for example,
$\Gamma , T$
. Such extended contexts may also be surrounded with parentheses, for example,
$(\Gamma , T)$
. We introduce contexts as an inductive type so that we can name the constructors in the Rocq formalization.
Definition 4.1.2 (Ctxt). Contexts are finite sequences of types. The Rocq definition is in Listing A.7 .
We abuse notation and embed the set of types into the set of contexts by the following shorthand:
\begin{equation*} (T) \triangleq (\bullet , T) . \end{equation*}
A typed variable in context is represented by a well-scoped and well-typed de Bruijn index.
Definition 4.1.3 (Idx). We define the type of indices, Idx, as the inductive family in Rocq given in Listing 4.1.1 .
De Bruijn Index Rocq Definition.
Well-scoped and well-typed STLC terms are given next.
Definition 4.1.4 (Tm). We define the type of terms, Tm, as the inductive family in Rocq in Listing 4.1.2 .
STLC Term Rocq Definition.
4.2 Renaming
We equip our syntax of terms with a renaming structure: a substitution restricted to variables. We emphasize, again, that we represent renamings with an explicit list rather than a type-preserving function from the variables in one context to the variables in another.
A context renaming is a list of variables taken from a given context. The list of variables induces a second context given by its sequence of types. We denote context renamings as arrows with a subscript
$\operatorname{ren}$
, for example,
$\rho : \Gamma \rightarrow _{\operatorname{ren}} \Delta$
.
Definition 4.2.1 (CtxtRnm). We define the type of context renamings, CtxtRnm, as the inductive family in Rocq in Listing 4.2.1 .
Context Renaming Rocq Definition.
Construction 4.2.2.
-
• (Context Renaming Weakening) Any context renaming
$\rho : \Gamma \rightarrow _{\operatorname{ren}} \Delta$
may be weakened to
$\rho _T : (\Gamma , T) \rightarrow _{\operatorname{ren}} \Delta$
. -
• (Context Identity Renaming) For any context,
$\Gamma$
, there is an identity renaming,
$\operatorname{id} : \Gamma \rightarrow _{\operatorname{ren}} \Gamma$
. -
• (Context Renaming Composition) Two context renamings,
$\rho : \Delta \rightarrow _{\operatorname{ren}} \Theta$
and
$\phi : {\Gamma \rightarrow _{\operatorname{ren}} \Delta }$
, may be composed resulting in
\begin{equation*} (\rho \circ \phi ) : \Gamma \rightarrow _{\operatorname{ren}} \Theta . \end{equation*}
Remark. For all contexts,
$\Gamma$
, and types,
$T$
, there is a weakening renaming
$(\operatorname{id})_T : (\Gamma ,T) \to \Gamma$
.
Lemma 4.2.3. Composing with the identity renaming is a neutral operation, and composition is associative.
Construction 4.2.4 (Term Renaming). Any term,
$\Delta \vdash t : T$
, may be renamed by
$\rho : \Gamma \rightarrow _{\operatorname{ren}} \Delta$
resulting in
\begin{equation*} \Gamma \vdash t[\rho ] : T . \end{equation*}
Theorem 4.2.5 (Term Renaming Action). Term renaming is an action: for all terms
$t$
,
\begin{equation*} t[\operatorname{id}] = t , \quad t[\rho \circ \phi ] = t[\rho ][\phi ] . \end{equation*}
4.3 Substitution
We equip the syntax of terms with a substitution structure. Again, we represent substitutions with an explicit list rather than a type-preserving function from the variables in one context to the terms in another.
A substitution is a list of terms taken from a given context. The list of terms induces a second context given by its sequence of types. We denote context substitutions as arrows with a subscript
$\operatorname{sub}$
, for example,
$\sigma : \Gamma \rightarrow _{\operatorname{sub}} \Delta$
.
Definition 4.3.1 (CtxtSubst). We define the type of context substitutions, CtxtSubst, as the inductive family in Rocq in Listing 4.3.1 .
Context Substitution Rocq Definition.
Construction 4.3.2.
-
• (Context Substitution Weakening) Any context substitution
$\Gamma \rightarrow _{\operatorname{sub}} \Delta$
may be weakened so that it maps
$(\Gamma , T) \rightarrow _{\operatorname{sub}} \Delta$
. -
• (Context Identity Substitution) For any context,
$\Gamma$
, there is an identity substitution,
$\operatorname{id} : \Gamma \rightarrow _{\operatorname{sub}} \Gamma$
. -
• (Context Substitution Composition) Two context substitutions,
$\sigma : \Delta \rightarrow _{\operatorname{sub}} \Theta$
and
$\psi : \Gamma \rightarrow _{\operatorname{sub}} \Delta$
, may be composed resulting in
\begin{equation*} (\sigma \circ \psi ) : \Gamma \rightarrow _{\operatorname{sub}} \Theta . \end{equation*}
Lemma 4.3.3. Composing with the identity substitution is a neutral operation, and composition is associative.
Construction 4.3.4 (Term Substituting). Any term,
$\Delta \vdash t : T$
, may be substituted using
$\sigma : \Gamma \rightarrow _{\operatorname{sub}} \Delta$
resulting in
\begin{equation*} \Gamma \vdash t[\sigma ] : T . \end{equation*}
Theorem 4.3.5 (Term Substituting Action). Term substituting is an action: for all terms
$t$
,
\begin{equation*} t[\operatorname{id}] = t , \quad t[\sigma \circ \psi ] = t[\sigma ][\psi ] . \end{equation*}
Remark. Any context renaming may be transformed into an equivalent context substitution by a lifting operation. The lifting operation respects the identity and composition of renamings. Moreover, the action of a lifted renaming on a term is the same as the action of the original renaming. This prevents any ambiguity in notation arising from, for example,
$t[(\operatorname{id})_T]$
where it is ambiguous if the
$(\operatorname{id})_T$
is a weakened renaming or a weakened substitution. Additionally, we formalize what may be referred to as “hetero-compositions”: mixed compositions of renamings and substitutions. These hetero-compositions satisfy the appropriate unitality and correctness conditions. We also formalized some, but not all, of the “associativity” conditions for hetero-compositions as required by our development.
4.4
$\beta \eta$
-Conversion
Hitherto, we have introduced the syntax of STLC. By using de Bruijn indices, we have that
$\alpha$
-equivalence of terms and of substitutions is just the standard identity strict proposition in Rocq. We now proceed to define
$\beta \eta$
-conversion for both terms and substitutions.
Definition 4.4.1 (BetaEtaConv). We adopt the definition of
$\beta \eta$
-conversion as the least symmetric, transitive, and congruent relation over
$\beta$
-reduction and
$\eta$
-expansion. The Rocq definition is given in Listing A.8
. There, we use two helper functions: BetaSubst, which substitutes the second argument for the de Bruijn index zero in the first argument, thereby decreasing the length of the context, and Shift, which introduces a new free variable at de Bruijn index zero, thereby increasing the length of the context.
Remark. We omit a constructor for reflexivity opting to prove it as a corollary of variables being self-convertible – which we include as part of the definition of being a congruence over the nullary (with respect to terms) variable constructor – and
$\beta \eta$
-conversion being a congruence.
Definition 4.4.2 (CtxtSubstConv). The extension of
$\beta \eta$
-conversion of terms to substitutions via a list construction is in the Rocq code in Listing A.9
.
5. Categorical Structure of Simply Typed Syntax
We give a number of definitions of p-categories and p-functors that arise out of the structure of syntax. Thereafter, we proceed to give these emergent structures universal characterizations firmly placing them within the context of (p-)categorical analysis.
5.1 Definitions
We define three p-categories that we shall use to examine the universal structure of syntax p-categorically. Each of these p-categories will have contexts for their objects but will have different families of hom p-sets.
Construction 5.1.1 (Rnm). The p-category of contexts and context renamings Rnm has as objects contexts and as morphisms context renamings considered as a discrete PType.
Rnm is a Cartesian p-category with the terminal object being the empty context and the Cartesian product being context concatenation.
Remark. Although not required for our development and so left unformalized, Rnm is the free Cartesian p-category over the set of types Ty; that is, up to p-isomorphism, there is a unique interpretation Cartesian p-functor from Rnm into any other Cartesian p-category given an interpretation of Ty in it. This is a simpler form of the result in Theorem 5.2.2.
Construction 5.1.2 (Subst
$_{\alpha }$
). The p-category of contexts and context substitutions, Subst
$_{\alpha }$
, has as objects contexts and as morphisms context substitutions related by
$\alpha$
-equivalence.
Subst
$_{\alpha }$
is a Cartesian-pre-closed p-category with the terminal object being given by the empty context, and the Cartesian product being given by context concatenation, which we denote by
$\Gamma \mathbin {+\!\!+} \Delta$
. The pre-exponential is given by the following recursive definitions:
\begin{align} {\Gamma ^T} &\triangleq {\begin{cases} (\!\bullet\!) & \Gamma = (\!\bullet\!) \\ ( {\Gamma '}^T, T \rightarrow T' ) & \Gamma = ( \Gamma ' , T' ) \end{cases}} \end{align}
\begin{align} {\Gamma ^\Delta } &\triangleq {\begin{cases} \Gamma & \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\Delta = (\!\bullet\!) \\ \left ( \Gamma ^T \right )^{\Delta '} \hphantom {( {\Gamma '}^T, T \rightarrow T' )} & \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\! \Delta = ( \Delta ' , T ) \end{cases}} \end{align}
where Definition (5.1.2.1) defines pre-exponentiation of a context by a type and Definition (5.1.2.2) defines context pre-exponentiation. The pre-abstraction and pre-evaluation maps,
\begin{equation*} \mathsf{Subst}_\alpha \left (\Gamma \mathbin {+\!\!+} \Delta , \Theta \right ) \mathrel {\rightleftarrows }\mathsf{Subst}_\alpha \left (\Gamma , \Theta ^\Delta \right ) . \end{equation*}
are defined by induction from the basic maps
\begin{equation*} \mathsf{Subst}_\alpha \left ((\Gamma , T), (S)\right ) \mathrel {\rightleftarrows } \mathsf{Subst}_\alpha \left (\Gamma , (T \rightarrow S)\right ) \end{equation*}
given by
Both of these constructions follow a two-step process where they are first constructed with respect to pre-exponentiation by types and thereafter constructed with respect to pre-exponentiation by contexts.
Construction 5.1.3 (Subst
$_{\beta \eta }$
). The p-category of contexts and context substitutions, Subst
$_{\beta \eta }$
, has as objects contexts and as morphisms context substitutions related by
$\beta \eta$
-conversion.
Subst
$_{\beta \eta }$
is a Cartesian-closed p-category with the terminal object being given by the empty context and the Cartesian product being given by context concatenation. The Cartesian exponential is given as in Construction 5.1.2.
Construction 5.1.4 (Inclusion and Quotient p-Functors). We have the following identity-on-objects and Cartesian p-functors:
-
•
$i : \mathsf{Rnm} \rightarrow \mathsf{Subst}_\alpha$
, and -
•
$j : \mathsf{Subst}_\alpha \rightarrow \mathsf{Subst}_{\beta \eta }$
.
Moreover, the latter p-functor is Cartesian-pre-closed and full.
5.2 Universal characterizations
Definition 5.2.1 (Free Cartesian-Closed p-Category). A p
-category,
$\mathscr{F}$
, is a free Cartesian-closed p
-category over a base type when it supports the following structure and properties: for all Cartesian-closed p
-categories
$\mathbb{C}$
,
-
(1)
$ \forall \, (c : \mathbb{C}).\, \exists \, ([\![ - ]\!]_c : \mathscr{F} \rightarrow _{\operatorname{CC}} \, \mathbb{C}).\, [\![ (\iota ) ]\!]_c \equiv c$
; -
(2)
$ \forall \, (c\, c' : \mathbb{C})\, (\,f : c \cong c').\, \exists \, ([\![ - ]\!]_f : [\![ - ]\!]_c \cong [\![ - ]\!]_{c'}). \, [\![ (\iota ) ]\!]_f \equiv f$
; -
(3)
$ \forall \, (c : \mathbb{C}).\, [\![ - ]\!]_{\operatorname{id}_c} \sim \operatorname{id}_{[\![ - ]\!]_c}$
; -
(4)
$ \forall \, (c\, c'\, c'' : \mathbb{C})\, (\,f : c \cong c') \, (g : c' \cong c'').\, [\![ - ]\!]_{g \circ f} \sim [\![ - ]\!]_g \circ [\![ - ]\!]_f$
; and
-
(5)
$ \forall \, (I : \mathscr{F} \rightarrow _{\operatorname{CC}} \mathbb{C}). \, \exists \, (q : [\![ - ]\!]_{I_0(\iota )} \cong I : u).$
-
–
$q_{\left (\iota \right )} \equiv \operatorname{id} \qquad \wedge$
-
–
$u_{\left (\iota \right )} \equiv \operatorname{id} \qquad \wedge$
-
–
$\forall \, (\alpha : [\![ - ]\!]_{I_0(\iota )} \overset {\!\!\sim }{\Rightarrow } I : \beta ). \, \alpha _{\left (\iota \right )} \sim \operatorname{id} \wedge \beta _{\left (\iota \right )} \sim \operatorname{id} \Rightarrow q \sim \alpha \wedge u \sim \beta$
.
-
Where “
$\rightarrow _{\operatorname{CC}}\!$
” above means a Cartesian-closed p
-functor.
The first condition provides existence of a Cartesian-closed interpretation p-functor into any pointed Cartesian-closed p-category. The second, third, and fourth conditions ensure that the interpretation p-functor is coherently invariant under p-isomorphisms of the pointing of the target Cartesian-closed p-category. Finally, the fifth condition ensures that the interpretation p-functor is unique up to unique p-isomorphism. This is informally summarized in Figure 2.
Freeness property for a free Cartesian-closed p-category.
Remark. Definition 5.2.1 is equivalent with
$\mathscr{F}$
being bicategorically p-initial in the locally groupoidal p-bicategory of pointed Cartesian-closed p-categories, pointed Cartesian-closed p-functors, and pointed p-natural isomorphisms. We have however chosen to use the elementary phrasing to emphasize the rôle of arbitrary Cartesian-closed interpretations,
$I : \mathscr{F} \rightarrow _{\operatorname{CC}} \mathbb{C}$
, in inducing specific interpretations,
$[\![ - ]\!]_{I_0(\iota )} : \mathscr{F} \rightarrow _{\operatorname{CC}} \, \mathbb{C}$
, and the associated
$q$
/
$u$
p-natural isomorphisms therebetween.
Theorem 5.2.2.
Subst
$_{\beta \eta }$
is a free Cartesian-closed p
-category over a single base type.
Importantly, the p-functor
$j : \mathsf{Subst}_\alpha \rightarrow \mathsf{Subst}_{\beta \eta }$
satisfies the two-dimensional universal property informally summarized in Figure 3.
Universal property for subst
$_{\alpha }$
relative to subst
$_{\beta \eta }$
.
Theorem 5.2.3.
The p
-functor
$j : \mathsf{Subst}_\alpha \rightarrow \mathsf{Subst}_{\beta \eta }$
satisfies the property that for all Cartesian-closed p
-categories,
$\mathbb{C}$
, and for all Cartesian-pre-closed p
-functors,
$I : \mathsf{Subst}_\alpha \to \mathbb{C}$
,
$ \exists \, (\tilde {q} : [\![ - ]\!]_{I_0(\iota )} \circ j \circ i \Rightarrow I \circ i) \, (\tilde {u} : I \circ i \Rightarrow [\![ - ]\!]_{I_0(\iota )} \circ j \circ i).$
-
(1)
$\tilde {q}_{\left (\iota \right )} \equiv \operatorname{id} \qquad \wedge$
-
(2)
$\tilde {u}_{\left (\iota \right )} \equiv \operatorname{id} \qquad \wedge$
-
(3)
$\forall \, (\alpha : [\![ - ]\!]_{I_0(\iota )} \circ j \circ i \Rightarrow I \circ i) \, (\beta : I \circ i \Rightarrow [\![ - ]\!]_{I_0(\iota )} \circ j \circ i).$
${\begin{array}{@{\quad}lll} & \alpha _{\left (\iota \right )} \sim \operatorname{id} & \wedge \\ & \beta _{\left (\iota \right )} \sim \operatorname{id} & \wedge \\ & \forall \, \Gamma \, \Delta . \, \alpha _{\Gamma \Rightarrow \Delta } \circ e_{[\![ - ]\!]} \sim \tilde {e}_I \circ (\beta _\Gamma \Rightarrow \alpha _\Delta ) & \wedge\\ & \forall \, \Gamma \, \Delta . \, ([\![ \varepsilon ]\!]_{I_0(\iota )} \circ p)^\ast \circ \beta _{\Gamma \Rightarrow \Delta } \sim (\alpha _\Gamma \Rightarrow \beta _\Delta ) \circ (I_1(\tilde {\varepsilon }) \circ p)^\ast & \Rightarrow \\ & \tilde {q} \sim \alpha \wedge \tilde {u} \sim \beta & \\ \end{array}}$
.
This property is a variation of the final property of Definition 5.2.1 to account for the Cartesian-pre-closed structure of Subst
$_{\alpha }$
. The first and second subconditions describe the strictness of the p-natural transformations
$\tilde {q}$
and
$\tilde {u}$
at the base type. The third subcondition is a uniqueness condition of
$\tilde {q}$
and
$\tilde {u}$
and thus a quasi-uniqueness condition on
$[\![ - ]\!]_{I_0(\iota )}$
with respect to the Cartesian-pre-closed structure
$\tilde {e}_I$
of
$I$
.
6. Computational Application: Normalization by Evaluation
We are finally in a position to state our p-categorical normalization functions for simply typed
$\lambda$
-calculus terms.
6.1 Soundness
As described in Figure 4, there are two (intensionally different) canonical p-functors from Subst
$_{\beta \eta }$
into presheaves thereover: the Yoneda embedding and the interpretation p-functor.
Interpretation of subst
$_{\beta \eta }$
into its p-category of presheaves.
This induces p-natural isomorphisms:
\begin{equation*} q : [\![ - ]\!] \Rightarrow y \textrm { with inverse } u : y \Rightarrow [\![ - ]\!] . \end{equation*}
These p-isomorphisms establish that the Yoneda embedding and the interpretation p-functor are extensionally the same. From these two perspectives, one can normalize any context substitution.
Definition 6.1.1 (nf
$_{1}$
). Following Čubrić et al. (Reference Čubrić, Dybjer and Scott1998), we define a normalization function, thus:
\begin{equation*} \mathsf{nf}_1(\sigma : \Gamma \rightarrow _{\operatorname{sub}} \Delta ) \triangleq q_{\Delta , \Gamma }([\![ \sigma ]\!]_{\Gamma }(u_{\Gamma ,\Gamma }(\operatorname{id}_{\Gamma }))) , \end{equation*}
based on Figure 4 .
Definition 6.1.2 (nf
$_{2}$
). Alternatively, using the Cartesian closure of
$\langle\, j \rangle$
, one may define a normalization function, thus:
\begin{equation*} \mathsf{nf}_2(\sigma : \Gamma \rightarrow _{\operatorname{sub}} \Delta ) \triangleq q_{\Delta , \Gamma }([\![ \sigma ]\!]_{\Gamma }(u_{\Gamma ,\Gamma }(\operatorname{id}_{\Gamma }))) , \end{equation*}
based on Figure 5 .
Interpretation of subst
$_{\beta \eta }$
into the p-category of presheaves over subst
$_{\alpha }$
.
Theorem 6.1.3 (Soundness). The normalization functions
$\mathsf{nf}_1$
and
$\mathsf{nf}_2$
are sound.
Proof. The result follows by equational reasoning: abstracting
$\mathsf{nf}_i$
as
$\mathsf{nf}$
, and
$y$
and
$\langle\, j \rangle$
as
$I$
, we have:
\begin{align*} \mathsf{nf}(\sigma ) &\equiv q_{\Delta , \Gamma }([\![ \sigma ]\!]_{\Gamma }(u_{\Gamma ,\Gamma }(\operatorname{id}_{\Gamma }))) & \operatorname{def} \\ &\sim _{\beta \eta } q_{\Delta , \Gamma }(u_{\Delta ,\Gamma }(I(\sigma )_{\Gamma }(\operatorname{id}_{\Gamma }))) & \operatorname{nat} \\ &\sim _{\beta \eta } q_{\Delta , \Gamma }(u_{\Delta ,\Gamma }(\sigma )) & \operatorname{yon/nerve} \\ &\sim _{\beta \eta } \sigma . & \operatorname{iso} \end{align*}
Remark. The Rocq formalization of Theorem 6.1.3 gives a program for computing a derivation of the
$\beta \eta$
-conversion of a term with its normal form as an element of the type in Listing A.8. We leave the analysis of these to further work.
The normalization function and category theory formalized provide the following.
Corollary 6.1.4 (Weak Completeness). The normalization functions
$\mathsf{nf}_1$
and
$\mathsf{nf}_2$
are weakly complete:
\begin{equation*} \sigma \sim _{\beta \eta } \sigma ' \ \Rightarrow \ \mathsf{nf}_1(\sigma ) \sim _{\beta \eta } \mathsf{nf}_1(\sigma ') \,\wedge \, \mathsf{nf}_2(\sigma ) \sim _{\beta \eta } \mathsf{nf}_2(\sigma ') . \end{equation*}
Remark. Although Corollary 6.1.4 is, by symmetry and transitivity of
$\sim _{\beta \eta }$
, a straightforward consequence of Theorem 6.1.3, a more direct proof can be given by observing that the normalization functions
$\mathsf{nf}_1$
and
$\mathsf{nf}_2$
are morphisms in PSet and therefore respect the appropriate PERs.
The normalization functions
$\mathsf{nf}_1$
and
$\mathsf{nf}_2$
do not obviously satisfy strong completeness. However, by example computations, one can observe that neither is the identity function intensionally, we have no proof that they are canonicalization functions reducing
$\beta \eta$
-conversion to
$\alpha$
-equivalence. We overcome this shortcoming by using the universal property of Subst
$_{\alpha }$
relative to Subst
$_{\beta \eta }$
to construct strongly complete normalization functions.
6.2 Strong completeness
We use the structure of Cartesian-pre-closure to derive a strongly complete normalization algorithm.
Definition 6.2.1 (nf
$_{3}$
). Using the Cartesian-pre-closure of
$y$
, we define a normalization function, thus:
\begin{equation*} \mathsf{nf}_3(\sigma : \Gamma \rightarrow _{\operatorname{sub}} \Delta ) \triangleq \tilde {q}_{\Delta , \Gamma }([\![ \sigma ]\!]_{\Gamma }(\tilde {u}_{\Gamma ,\Gamma }(\operatorname{id}_{\Gamma }))) , \end{equation*}
based on Figure 6 .
Interpretation of subst
$_{\beta \eta }$
into the p-category of presheaves over subst
$_{\alpha }$
.
Theorem 6.2.2 (Strong Completeness). The normalization function
$\mathsf{nf}_3$
is strongly complete:
\begin{equation*} \sigma \sim _{\beta \eta } \sigma ' \Rightarrow \mathsf{nf}_3(\sigma ) \equiv _\alpha \mathsf{nf}_3(\sigma ') . \end{equation*}
The normalization function
$\mathsf{nf}_3$
is strongly complete, but it is not obviously sound as the
$\tilde {q}$
and
$\tilde {u}$
associated to the universal property of Subst
$_{\alpha }$
relative to Subst
$_{\beta \eta }$
are not p-natural with respect to substitutions, but only renamings, and so our former proof of soundness cannot be translated across to the new setting. However, by example computations, one can observe that it seems to be the identity function extensionally, we have no proof that its output is
$\beta \eta$
-convertible with its input. We overcome this shortcoming by gluing together two normalization functions, one sound and one strongly complete, and establishing that the two produce outputs
$\beta \eta$
-convertible with each other. Then, the observation that a strongly complete normalization function that is
$\beta \eta$
-convertible with a sound normalization function is necessarily sound and strongly complete will allow us to conclude the correctness of our final normalization function.
6.3 Sound and strongly complete normalization
We glue together a sound normalization algorithm and a strongly complete normalization algorithm to establish full correctness for the strongly complete normalization algorithm.
Construction 6.3.1. The gluing p-category
$\widehat {\mathsf{Subst}}_{\alpha } \downarrow \widehat {\mathsf{Subst}}_{\alpha }$
is a Cartesian-closed p-category. We may therefore induce a Cartesian-pre-closed p-functor:
\begin{equation*} \langle y \downarrow \langle\, j \rangle j \rangle : \mathsf{Subst}_\alpha \rightarrow \widehat {\mathsf{Subst}}_{\alpha } \downarrow \widehat {\mathsf{Subst}}_{\alpha } , \end{equation*}
where the domain component is the Yoneda embedding,
$y : \mathsf{Subst}_\alpha \rightarrow \widehat {\mathsf{Subst}}_{\alpha }$
, and the codomain component is the nerve of
$j$
after
$j$
,
$\langle\, j \rangle \, j : \mathsf{Subst}_\alpha \rightarrow \widehat {\mathsf{Subst}}_{\alpha }$
. There is a canonical p-natural transformation,
$y \Rightarrow \langle\, j \rangle j$
, by reflexivity of
$\beta \eta$
-conversion.
Definition 6.3.2 (nf
$_{4}$
). We define two normalization functions, thus:
-
•
$\mathsf{nf}^{\operatorname{D}}_4(\sigma : \Gamma \rightarrow _{\operatorname{sub}} \Delta ) \triangleq \operatorname{Dom}(\tilde {q}_{\Delta })_{\Gamma }(\operatorname{Dom}([\![ \Gamma \vdash _{\operatorname{sub}} \sigma : \Delta ]\!])_\Gamma (\operatorname{Dom}(\tilde {u}_{\Gamma })_{\Gamma }(\operatorname{id}_\Gamma )))$
; and
-
•
$\mathsf{nf}^{\operatorname{C}}_4(\sigma : \Gamma \rightarrow _{\operatorname{sub}} \Delta ) \triangleq \operatorname{Cod}(\tilde {q}_{\Delta })_{\Gamma }(\operatorname{Cod}([\![ \Gamma \vdash _{\operatorname{sub}} \sigma : \Delta ]\!])_\Gamma (\operatorname{Cod}(\tilde {u}_{\Gamma })_{\Gamma }(\operatorname{id}_\Gamma )))$
.
based on Figure 7 .
Interpretation of subst
$_{\beta \eta }$
into the gluing p-category
$\widehat {\mathsf{Subst}}_{\alpha } \downarrow \widehat {\mathsf{Subst}}_{\alpha }$
.
Theorem 6.3.3 (Soundness). The normalization function
$\mathsf{nf}^{\operatorname{C}}_4$
is sound:
\begin{equation*} \sigma \sim _{\beta \eta } \mathsf{nf}^{\operatorname{C}}_4(\sigma ) . \end{equation*}
Theorem 6.3.4 (Strong Completeness). The normalization function
$\mathsf{nf}^{\operatorname{D}}_4$
is strongly complete:
\begin{equation*} \sigma \sim _{\beta \eta } \sigma ' \Rightarrow \mathsf{nf}^{\operatorname{D}}_4(\sigma ) \equiv _\alpha \mathsf{nf}^{\operatorname{D}}_4(\sigma ') . \end{equation*}
Lemma 6.3.5.
The normalization functions
$\mathsf{nf}^{\operatorname{D}}_4$
and
$\mathsf{nf}^{\operatorname{C}}_4$
agree extensionally:
\begin{equation*} j(\mathsf{nf}^{\operatorname{D}}_4(\sigma )) \sim _{\beta \eta } \mathsf{nf}^{\operatorname{C}}_4(\sigma ) . \end{equation*}
Theorem 6.3.6 (Correctness). The normalization function
$\mathsf{nf}^{\operatorname{D}}_4$
is sound and strongly complete:
-
•
$\sigma \sim _{\beta \eta } j(\mathsf{nf}^{\operatorname{D}}_4(\sigma ))$
; and
-
•
$\sigma \sim _{\beta \eta } \sigma ' \Rightarrow \mathsf{nf}^{\operatorname{D}}_4(\sigma ) \equiv _\alpha \mathsf{nf}^{\operatorname{D}}_4(\sigma ')$
.
We have therefore succeeded in categorically constructing a sound and strongly complete normalization function. That these properties have been induced purely by categorical universal property relies strongly on our novel definitions of Cartesian-pre-closure and the universal property of Subst
$_{\alpha }$
relative to Subst
$_{\beta \eta }$
.
Remark. For presentational simplicity, in Construction 6.3.1 and Definition 6.3.2, we used
$\widehat {\mathsf{Subst}}_{\alpha } \downarrow \widehat {\mathsf{Subst}}_{\alpha }$
as our gluing p-category, which is simply the arrow category over
$\widehat {\mathsf{Subst}}_{\alpha }$
(and therefore also a presheaf p-category). In fact, it suffices to use any appropriate gluing p-category of the form
$\widehat {\mathbb{C}} \downarrow F$
, where
$\mathbb{C}$
is a p-category of contexts supporting normalization and
$F$
is an appropriate p-functor from any Cartesian-closed p-category, supporting soundness, into
$\widehat {\mathbb{C}}$
. Thus, instead, one may use
$\widehat {\mathsf{Rnm}} \downarrow \langle\, j \circ i \rangle$
and induce the interpretation by
$\langle \langle i \rangle \downarrow j \rangle$
. This, and related choices, brings our construction closer into connection with the gluing construction of Fiore (Reference Fiore2002, Reference Fiore2022).
6.4 Examples
To demonstrate the normalization algorithm synthesized, we give a few examples of the computation of
$\mathsf{nf}$
on sample terms.
Definition 6.4.1 (one). Define
$\mathsf{one}$
as a Church numeral:
\begin{align*} \mathsf{one} \triangleq & \, \mathsf{Abs\,(Var\,IdxZero)} \ : \mathsf{Tm\,Nil\,(Arr\,(Arr\,Iota\,Iota)\,(Arr\,Iota\,Iota))} . \end{align*}
Example 6.4.2 (
$\eta$
-Expansion of one). The definition of
$\mathsf{one}$
is not in
$\eta$
-long form. The normalization algorithm
$\eta$
-expands it, thus:
\begin{equation*} \mathsf{nf}(\mathsf{one}) \,\equiv \, \mathsf{(Abs\,(Abs\,(App} \mathsf{(Var\,(IdxSucc\,IdxZero))} \mathsf{(Var\,IdxZero))))} . \end{equation*}
Definition 6.4.3 (succ). Define
$\mathsf{succ}$
as the successor Church numeral:
\begin{align*} \mathsf{succ} \triangleq & \, \mathsf{Abs\,(Abs\,(Abs\,(App} \\ & \qquad \,\, \mathsf{(Var\,(IdxSucc\,IdxZero))} \\ & \qquad \,\, \mathsf{(App\,(App} \\ & \qquad \qquad \mathsf{(Var\,(IdxSucc\,(IdxSucc\,IdxZero)))} \\ & \qquad \qquad \mathsf{(Var\,(IdxSucc\,IdxZero)))} \\ & \qquad \quad \, \, \mathsf{(Var\,IdxZero)))))} . \end{align*}
Example 6.4.4 (Normalization of two). The definition of
$\mathsf{two}$
as the successor of
$\mathsf{one}$
is not a
$\beta$
-normal form. It is normalized, thus:
\begin{align*} \mathsf{nf}(\mathsf{App\,succ\,one}) \equiv \; & \mathsf{(Abs\,(Abs\,(App} \\ & \quad \mathsf{(Var\,(IdxSucc\,IdxZero))} \\ & \quad \mathsf{(App\,(Var\,(IdxSucc\,IdxZero))\,(Var\,IdxZero)))))} . \end{align*}
7. Conclusions
We conclude by summarizing our results and proposing some directions of future work.
7.1 Summary of results
We have taken the pen-and-paper argument of Čubrić et al. (Reference Čubrić, Dybjer and Scott1998) and have formalized it in the computational setting of the Rocq proof assistant. The facility of this being achieved was stressed in their paper, and we have demonstrated it. We have bypassed their non-categorical proof of strong completeness and instead provided a categorical one by way of a new universal property for unquotiented syntax and categorical gluing.
Our formalization of their work has resulted in the formalization of both p-category theory and the simply typed
$\lambda$
-calculus. We have formalized results not known to have been formalized before connecting syntax with both categorical and computational semantics.
Our work fully connects the normalization of simply typed
$\lambda$
-calculus terms with the categorical semantics of the simply typed
$\lambda$
-calculus. It differs from much other work in that it successfully uses the formalization of abstract category theory for a concrete computational purpose: the normalization of simply typed
$\lambda$
-calculus terms.
7.2 Further work
We suggest a few avenues of further work, not remarked upon throughout the course of the paper.
We wonder whether the universal property of Subst
$_{\alpha }$
relative to Subst
$_{\beta \eta }$
(Theorem5.2.3) could be generalized; specifically, we were unable to prove any stronger p-naturality properties for
$\tilde {q}$
and
$\tilde {u}$
.
The use of gluing categories in the final construction connects with the works of Fiore (Reference Fiore2002, Reference Fiore2022) and Altenkirch et al. (Reference Altenkirch, Hofmann, Streicher, Pitt, Rydeheard and Johnstone1995). Further analysis should investigate this connection.
Our concept of Cartesian-pre-closure can be generalized to other adjunctions and such lax preservation of right adjoints: Does this situation have broader and more general applicability in category theory?
We use a single base type to generate our simple type theory; other generating data may also be considered, for example, constants and equations. The product type former can be readily incorporated; other type formers, such as sums (Altenkirch et al. (Reference Altenkirch, Dybjer, Hofmann and Scott2001); Balat et al. (Reference Balat, Di Cosmo and Fiore2004)), need be considered.
Finally, investigations should be made about how our technique translates into the settings for more sophisticated type theories such as polymorphic and dependent ones.
Acknowledgements
The authors are grateful to Djordje Čubrić and Peter Dybjer for insightful conversation about the background to their original work. The research of the second author was partially supported by EPSRC grant EP/V002309/1.
Competing interests
The authors declare none.
A. Selected Rocq code listings
p-Isomorphism Rocq Definition.
Cartesian p-Category Rocq Definition.
Cartesian p-Functor Rocq Definition.
Cartesian-Closed p-Category Rocq Definition.
Cartesian-Closed p-Functor Rocq Definition.
Simple Types Rocq Definition.
Context Rocq Definition.
Term
$\beta \eta$
-Conversion Rocq Definition.
Context Substitution
$\beta \eta$
-Conversion Rocq Definition.
