# Correct and Complete Type Checking and Certified Erasure for Coq, in Coq

Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, Théo Winterhalter

► To cite this version:

Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, et al.. Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. 2023. hal-04077552

HAL Id: hal-04077552

https://inria.hal.science/hal-04077552

Preprint submitted on 21 Apr 2023

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
Correct and Complete Type Checking and Certified Erasure
for Coq, in Coq

MATTHIEU SOZEAU, Inria, France

YANNICK FORSTER, Inria, France

MEVEN LENNON-BERTRAND, University of Cambridge, United Kingdom

JAKOB BOTSCH NIELSEN, Concordium Blockchain Research Center, Denmark

NICOLAS TABAREAU, Inria, France

THÉO WINTERHALTER, Inria, France

Coq is built around a well-delimited kernel that performs type checking for definitions in a variant of the Calculus of Inductive Constructions (CIC). Although the metatheory of CIC is very stable and reliable, the correctness of its implementation in Coq is less clear. Indeed, implementing an efficient type checker for CIC is a rather complex task, and many parts of the code rely on implicit invariants which can easily be broken by further evolution of the code. Therefore, on average, one critical bug has been found every year in Coq. This paper presents the first implementation of a type checker for the kernel of Coq (without the module system, template polymorphism and $\eta$-conversion), which is proven sound and complete in Coq with respect to its formal specification. Note that because of Gödel's second incompleteness theorem, there is no hope to prove completely the soundness of the specification of Coq inside Coq (in particular strong normalization), but it is possible to prove the correctness and completeness of the implementation assuming soundness of the specification, thus moving from a trusted code base (TCB) to a trusted theory base (TTB) paradigm. Our work is based on the META-Coq project which provides meta-programming facilities to work with terms and declarations at the level of the kernel. We verify a relatively efficient type checker based on the specification of the typing relation of the Polymorphic, Cumulative Calculus of Inductive Constructions (PCUIC) at the basis of Coq. It is worth mentioning that during the verification process, we have found a source of incompleteness in Coq's official type checker, which has then been fixed in Coq 8.14 thanks to our work. In addition to the kernel implementation, another essential feature of Coq is the so-called *extraction* mechanism: the production of executable code in functional languages from Coq definitions. We present a verified version of this subtle type and proof erasure step, therefore enabling the verified extraction of a safe type checker for Coq in the future.

CCS Concepts: • **Theory of computation** → **Type theory**.

Additional Key Words and Phrases: proof assistants, type checker, certification

**ACM Reference Format:**

Matthieu Sozeau, Yannick Forster, Meven Lennon-Bertrand, Jakob Botsch Nielsen, Nicolas Tabareau, and Théo Winterhalter. 2023. Correct and Complete Type Checking and Certified Erasure for Coq, in Coq. J. ACM 1, 1, Article 1 (January 2023), 76 pages.

Authors' addresses: Matthieu Sozeau, Gallinette, Inria, France, matthieu.sozeau@inria.fr; Yannick Forster, Gallinette, Inria, France, yannick.forster@inria.fr; Meven Lennon-Bertrand, University of Cambridge, United Kingdom, mgapb2@cam.ac.uk; Jakob Botsch Nielsen, Concordium Blockchain Research Center, Denmark, jakob.botsch.nielsen@gmail.com; Nicolas Tabareau, Gallinette, Inria, France, nicolas.tabareau@inria.fr; Théo Winterhalter, Inria, Saclay, France, theo.winterhalter@inria.fr.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.

© 2023 Association for Computing Machinery.

0004-5411/2023/1-ART1

https://doi.org/
# Correct and Complete Type Checking and Certified Erasure for Coq, in Coq

MATTHIEU SOZEAU, Inria, France

YANNICK FORSTER, Inria, France

MEVEN LENNON-BERTRAND, University of Cambridge, United Kingdom

JAKOB BOTSCH NIELSEN, Concordium Blockchain Research Center, Denmark

NICOLAS TABAREAU, Inria, France

THÉO WINTERHALTER, Inria, France

Coq is built around a well-delimited kernel that performs type checking for definitions in a variant of the Calculus of Inductive Constructions (CIC). Although the metatheory of CIC is very stable and reliable, the correctness of its implementation in Coq is less clear. Indeed, implementing an efficient type checker for CIC is a rather complex task, and many parts of the code rely on implicit invariants which can easily be broken by further evolution of the code. Therefore, on average, one critical bug has been found every year in Coq. This paper presents the first implementation of a type checker for the kernel of Coq (without the module system, template polymorphism and $\eta$-conversion), which is proven sound and complete in Coq with respect to its formal specification. Note that because of Gödel's second incompleteness theorem, there is no hope to prove completely the soundness of the specification of Coq inside Coq (in particular strong normalization), but it is possible to prove the correctness and completeness of the implementation assuming soundness of the specification, thus moving from a trusted code base (TCB) to a trusted theory base (TTB) paradigm. Our work is based on the META-Coq project which provides meta-programming facilities to work with terms and declarations at the level of the kernel. We verify a relatively efficient type checker based on the specification of the typing relation of the Polymorphic, Cumulative Calculus of Inductive Constructions (PCUIC) at the basis of Coq. It is worth mentioning that during the verification process, we have found a source of incompleteness in Coq's official type checker, which has then been fixed in Coq 8.14 thanks to our work. In addition to the kernel implementation, another essential feature of Coq is the so-called *extraction* mechanism: the production of executable code in functional languages from Coq definitions. We present a verified version of this subtle type and proof erasure step, therefore enabling the verified extraction of a safe type checker for Coq in the future.

CCS Concepts: • **Theory of computation** → **Type theory**.

Additional Key Words and Phrases: proof assistants, type checker, certification

Authors' addresses: Matthieu Sozeau, Gallinette, Inria, France, matthieu.sozeau@inria.fr; Yannick Forster, Gallinette, Inria, France, yannick.forster@inria.fr; Meven Lennon-Bertrand, University of Cambridge, United Kingdom, mgapb2@cam.ac.uk; Jakob Botsch Nielsen, Concordium Blockchain Research Center, Denmark, jakob.botsch.nielsen@gmail.com; Nicolas Tabareau, Gallinette, Inria, France, nicolas.tabareau@inria.fr; Théo Winterhalter, Inria, Saclay, France, theo.winterhalter@inria.fr.

<figure><img src="image_2.png" /></figure>
CONTENTS

<table><tr><td>Abstract</td><td>1</td></tr><tr><td>Contents</td><td>2</td></tr><tr><td>1 Introduction</td><td>3</td></tr><tr><td>2 An overview of Coq's type theory</td><td>6</td></tr><tr><td>2.1 Datatypes</td><td>6</td></tr><tr><td>2.2 Sorts and universes</td><td>9</td></tr><tr><td>2.3 Other Features of Coq Present in PCUIC</td><td>11</td></tr><tr><td>2.4 Other Features of Coq Absent from PCUIC</td><td>11</td></tr><tr><td>3 PCUIC: Coq's core calculus specification</td><td>12</td></tr><tr><td>3.1 Definition of the Syntax and Environments</td><td>13</td></tr><tr><td>3.2 Universes</td><td>14</td></tr><tr><td>3.3 Cumulativity</td><td>16</td></tr><tr><td>3.4 Dealing with the Guard Condition</td><td>19</td></tr><tr><td>3.5 Definition of Typing</td><td>19</td></tr><tr><td>3.6 Well-Formed Environments</td><td>22</td></tr><tr><td>4 Equivalent Algorithmic Specification of PCUIC</td><td>28</td></tr><tr><td>4.1 Universes: Valuation vs Acyclicity</td><td>28</td></tr><tr><td>4.2 Conversion: Algorithmic presentation with equality and reduction</td><td>30</td></tr><tr><td>4.3 Bidirectional Typing</td><td>34</td></tr><tr><td>4.4 Fixing Cumulativity for Pattern Matching on Cumulative Inductive Types</td><td>37</td></tr><tr><td>5 Metatheory of PCUIC</td><td>39</td></tr><tr><td>5.1 Accessibility and Well-Founded Induction</td><td>39</td></tr><tr><td>5.2 Substitution and Weakening</td><td>40</td></tr><tr><td>5.3 Confluence</td><td>41</td></tr><tr><td>5.4 Subject Reduction</td><td>45</td></tr><tr><td>5.5 Strong Normalization</td><td>47</td></tr><tr><td>5.6 Weak Call-by-Value Standardization</td><td>47</td></tr><tr><td>5.7 Canonicity</td><td>50</td></tr><tr><td>5.8 Consistency</td><td>51</td></tr><tr><td>6 A Sound and Complete Checker for PCUIC</td><td>51</td></tr><tr><td>6.1 Technical Insight</td><td>52</td></tr><tr><td>6.2 Abstract Computational Environment</td><td>55</td></tr><tr><td>6.3 Conversion and Cumulativity Without Fuel</td><td>57</td></tr><tr><td>6.4 A Typechecking Algorithm for PCUIC</td><td>61</td></tr><tr><td>7 Type and Proof Erasure for PCUIC</td><td>61</td></tr><tr><td>7.1 The Target Calculus λ□</td><td>62</td></tr><tr><td>7.2 Definition of an Erasure Function</td><td>63</td></tr><tr><td>7.3 Correctness of Erasure</td><td>64</td></tr><tr><td>7.4 Optimizations</td><td>66</td></tr><tr><td>8 Related Work</td><td>67</td></tr><tr><td>9 Conclusion and Future Work</td><td>68</td></tr><tr><td>Acknowledgments</td><td>69</td></tr><tr><td>References</td><td>69</td></tr></table>
CONTENTS

<table><tr><td>Abstract</td><td>1</td></tr><tr><td>Contents</td><td>2</td></tr><tr><td>1 Introduction</td><td>2</td></tr><tr><td>2 PCUIC: Coq's core calculus specification</td><td>6</td></tr><tr><td>2.1 Definition of the Syntax and Environments</td><td>7</td></tr><tr><td>2.2 Universes</td><td>7</td></tr><tr><td>2.3 Cumulativity</td><td>9</td></tr><tr><td>2.4 Dealing with the Guard Condition</td><td>12</td></tr><tr><td>2.5 Definition of Typing</td><td>13</td></tr><tr><td>2.6 Well-Formed Environments</td><td>15</td></tr><tr><td>3 Equivalent Algorithmic Specification of PCUIC</td><td>20</td></tr><tr><td>3.1 Universes: Valuation vs Acyclicity</td><td>21</td></tr><tr><td>3.2 Conversion: Algorithmic presentation with equality and reduction</td><td>23</td></tr><tr><td>3.3 Bidirectional Typing</td><td>26</td></tr><tr><td>3.4 Fixing Cumulativity for Pattern Matching on Cumulative Inductive Types</td><td>30</td></tr><tr><td>4 Metatheory of PCUIC</td><td>31</td></tr><tr><td>4.1 Accessibility and Well-Founded Induction</td><td>32</td></tr><tr><td>4.2 Substitution and Weakening</td><td>32</td></tr><tr><td>4.3 Confluence</td><td>34</td></tr><tr><td>4.4 Subject Reduction</td><td>37</td></tr><tr><td>4.5 Strong Normalization</td><td>39</td></tr><tr><td>4.6 Weak Call-by-Value Standardization</td><td>39</td></tr><tr><td>4.7 Canonicity</td><td>42</td></tr><tr><td>4.8 Consistency</td><td>43</td></tr><tr><td>5 A Sound and Complete Checker for PCUIC</td><td>43</td></tr><tr><td>5.1 Technical Insight</td><td>44</td></tr><tr><td>5.2 Abstract Computational Environment</td><td>46</td></tr><tr><td>5.3 Conversion and Cumulativity Without Fuel</td><td>49</td></tr><tr><td>5.4 A Typechecking Algorithm for PCUIC</td><td>53</td></tr><tr><td>6 Type and Proof Erasure for PCUIC</td><td>53</td></tr><tr><td>6.1 The Target Calculus λ<sub>□</sub></td><td>54</td></tr><tr><td>6.2 Definition of an Erasure Function</td><td>55</td></tr><tr><td>6.3 Correctness of Erasure</td><td>56</td></tr><tr><td>6.4 Optimizations</td><td>57</td></tr><tr><td>7 Related Work</td><td>59</td></tr><tr><td>8 Conclusion and Future Work</td><td>60</td></tr><tr><td>Acknowledgments</td><td>60</td></tr><tr><td>References</td><td>61</td></tr></table>

# 1 INTRODUCTION

Even *Proof Assistants Have Bugs*. Since the introduction of the Calculus of Inductive Constructions (CIC) and the first implementation of the Coq proof assistant, very few issues have been found in the underlying theory of Coq. There have been several debates on what should be the core type theory, because making it stronger can turn it inconsistent with common axioms,<fnref n="1" /> but the

<footnote n="1">¹For instance, the fact that the sort Set of sets was impredicative by default has been changed to maintain compatibility with the axiom of excluded middle.</footnote>
# 1 INTRODUCTION

Even *Proof Assistants Have Bugs*. Since the introduction of the Calculus of Inductive Constructions (CIC) and the first implementation of the CoQ proof assistant, very few issues have been found in the underlying theory of CoQ. There have been several debates on what should be the core type theory, because making it stronger can turn it inconsistent with common axioms,<fnref n="1" /> but the type theory supporting the CoQ proof assistant is overall very stable and reliable. This is however far from being the case for the implementation of the kernel of CoQ, for which on average one critical bug is found every year. The interested reader can directly jump to https://github.com/coq/coq/blob/master/dev/doc/critical-bugs.md, where the list of critical bugs that have been found in the CoQ proof assistant is maintained. For instance, one can find there that for some time, there was a substitution missing in the body of a let in the definition of *match*, somewhere in the code, which could lead to a proof of ⊥.

Fortunately, all those critical bugs are very tricky to exhibit, and would be very unlikely to happen by accident, but still a malicious developer could exploit them to produce very hard to detect fake formalizations. At a time when certificates obtained from proof assistants such as CoQ are gaining traction in the safety & security industry,<fnref n="2" /> this looks like a bad joke.

However, implementing and maintaining an efficient and bug free type checker for CIC is a very complex task, due to its size and the fact that the implementation relies on many invariants which are not always explicit and easy to break by modifying the code or adding new functionality. In this paper, we describe the first implementation of a type checker for the core language of CoQ, which is proven *sound and complete* in CoQ with respect to an entirely formal specification of the calculus.

*Certifying Proof Assistants using Proof Assistants.* We would like to mention right away that we are not claiming to prove the consistency of CoQ in CoQ, which would obviously contradict Gödel’s second incompleteness theorem stating that no consistent axiomatic system which includes Peano arithmetic can prove its own consistency.<fnref n="3" /> Prior work by Barras [2012] already went far in this direction, proving in CoQ that an idealized variant of the calculus of inductive constructions with *n* universes is relatively consistent to an internalization of ZFC with *n* Grothendieck universes. More recently, Adjedj et al. [2024] provide a fully certified type checker for Martin-Löf Type Theory with one universe, Π and Σ types, natural numbers, and equality, removing the detour through set theory and making the gap between the object and meta-theory very thin.

However, although it is not possible to prove the consistency of the kernel of CoQ using CoQ, it is perfectly possible to prove the correctness of an implementation of a type checker *assuming the consistency of the theory*. Our work requires much less logical strength than the above, involving only inductive families on decidable types and structurally recursive definitions. But the challenge resides in the ambitious scale of the object language which is very close to the actual implementation of CoQ, rather than a highly idealized simplified system. In practice, our formalization assumes strong normalization of the reduction, although most of the meta-theory is developed without using that axiom. Indeed, it is mainly used as a basis for the implementation of algorithmic conversion, which is defined by recursion on the strong normalization assumption.

<footnote n="1">¹For instance, the fact that the sort Set of sets was impredicative by default has been changed to maintain compatibility with the axiom of excluded middle.</footnote>

<footnote n="2">²For instance, the French National Cybersecurity Agency (ANSSI) has defined requirements on the use of Coq in the context of Common Criteria Evaluations [ANSSI 2021].</footnote>

<footnote n="3">³Gödel’s original proof was done in the setting of Peano arithmetic (which is classical). But it can also be performed using Heyting arithmetic, which lets us think that it is applicable to CIC even if no precise result have been stated in the literature.</footnote>
type theory supporting the Coq proof assistant is overall very stable and reliable. This is however
far from being the case for the implementation of the kernel of Coq, for which on average one
critical bug is found every year. The interested reader can directly jump to https://github.com/coq/
coq/blob/master/dev/doc/critical-bugs, where the list of critical bugs that have been found in the
Coq proof assistant is maintained. For instance, one can find there that for some time, there was a
substitution missing in the body of a let in the definition of match, somewhere in the code, which
could lead to a proof of ⊥.

Fortunately, all those critical bugs are very tricky to exhibit, and would be very unlikely to
happen by accident, but still a malicious developer could exploit them to produce very hard to
detect fake formalizations. At a time when certificates obtained from proof assistants such as Coq
are gaining traction in the safety & security industry,<fnref n="2" /> this looks like a bad joke.

However, implementing and maintaining an efficient and bug free type checker for CIC is a very
complex task, due to its size and the fact that the implementation relies on many invariants which
are not always explicit and easy to break by modifying the code or adding new functionality. In this
paper, we describe the first implementation of a type checker for the core language of Coq, which
is proven *sound and complete* in Coq with respect to an entirely formal specification of the calculus.

*Certifying Proof Assistants using Proof Assistants.* We would like to mention right away that we are not claiming to prove the consistency of Coq in Coq, which would obviously contradict Gödel’s second incompleteness theorem stating that no consistent axiomatic system which includes Peano arithmetic can prove its own consistency.<fnref n="3" /> Prior work by Barras [2012] went as far as possible in this direction, proving in Coq that an idealized variant of the calculus of inductive constructions with *n* universes is relatively consistent to an internalization of ZFC with *n* Grothendieck universes. Similarly, Abel et al. [2018a] prove in AGDA with inductive-recursive types the strong normalization of Martin-Löf Type Theory with natural numbers and two universes. However, although it is not possible to prove the consistency of the kernel of Coq using Coq, it is perfectly possible to prove the correctness of an implementation of a type checker *assuming the consistency of the theory*. Our work requires much less logical strength than for instance the existence of inductive-recursive definitions, involving only inductive families on decidable types and structurally recursive definitions. In practice, our formalization assumes strong normalization of the reduction of CIC, although most of the meta-theory is developed without using that axiom. Indeed, it is mainly used as a basis for the implementation of algorithmic conversion, which is defined by recursion on the strong normalization assumption. Barras [1999] constructed the first formalization of the Calculus of Constructions (with 2 universes) in Coq, we extend this to the full theory of Coq including the full cumulative universe hierarchy, universe polymorphism and cumulative (co)inductive type families.

Note that the strong normalization assumption is intimately related to the so-called guard
condition, the restriction on (co)fixpoint definitions which makes it impossible to define non-
terminating functions, and therefore to prove ⊥. Our point of view on the guard condition is
abstract: we formalize it as a parameter of the theory which implies strong normalization, and
we collect on the way the syntactic requirements it should fulfill for the meta-theory to satisfy
important properties such as subject reduction. For instance, the guard condition has to be stable
under reduction, otherwise some accepted fixpoints may not type-check after reduction.

<footnote n="2">²For instance, the French National Cybersecurity Agency (ANSSI) has defined requirements on the use of Coq in the context of Common Criteria Evaluations [ANSSI 2021].</footnote>

<footnote n="3">³Gödel’s original proof was done in the setting of Peano arithmetic (which is classical). But it can also be performed using Heyting arithmetic, which lets us think that it is applicable to CIC even if no precise result have been stated in the literature.</footnote>
Note that this strong normalization assumption is intimately related to the so-called guard condition, the restriction on (co)fixpoint definitions which makes it impossible to define non-terminating functions, and therefore to prove $⊥$. Our point of view on the guard condition is abstract: we formalize it as a parameter of the theory which implies strong normalization, and we collect on the way the syntactic requirements it should fulfill for the meta-theory to satisfy important properties such as subject reduction. For instance, the guard condition has to be stable under reduction, otherwise some accepted fixpoints may not type-check after reduction.

*From a Trusted Code Base to a Trusted Theory Base Paradigm.* Thus, the assumed normalization with its accompanying requirements on the guard condition is the only Achilles heel of our formalization: if it holds, then there is no error in the implementation. So, this paper proposes to switch from a trusted code base to a trusted theory base paradigm! Moreover, if one of the assumed properties were false, the implementation might be wrong, but there would be a much more serious problem to fix in Coq's meta-theory. Without getting into philosophical debates, we argue that this work provides important assurances about the correctness of the system, that is complimentary to the many theoretical studies of variants of the Calculus of Constructions and Martin-Löf Type Theory from the literature [Coquand and Huet 1988; Martin-Löf 1998], of which none is as close to the calculus actually implemented in Coq as our work. True believers in computation and type theory might actually enjoy the relatively small, formal specification of the calculus implemented in Coq (a few pages for the typing and cumulativity rules). Our work also sheds light on the many formal properties of the calculus that are used by the implementation, are probably known by most developers of proof assistants, but are seldom spelled out in detail, and formally. We believe that getting a better understanding of those properties can serve as a guide for better and more efficient implementations in the near future.

To avoid unnecessary complications, we work with a mildly simplified version of Coq's core language we call PCUIC (for Predicative Calculus of Cumulative Inductive Constructions<fnref n="4" />), and show an equivalence with the implemented version (up to representation of strings and arrays). Note that the kernel of Coq also includes a module system, template polymorphism, $\eta$-conversion and efficient conversion algorithms, and primitive types (integers, floats and persistent arrays) that we exclude for now. As explained earlier, we leave abstract the guard and productivity checking. Finally, our strict positivity judgment for (co-)inductive definitions does not yet support nested inductive types. This is only a technical limitation that will be lifted in future work.

*From Specification to Implementation.* We start by providing an entirely declarative version of the specification, as close as possible to its mathematical presentation on paper. For instance, the definition of the consistency of a polymorphic universe hierarchy via a valuation in natural numbers is very direct, without resorting to notions such as graphs of universes or acyclicity. Similarly, the specification of the cumulativity and conversion relations is a proper inductive judgmental equality judgment, which does not even mention a notion of reduction.

From this, we proceed by separating the specification of the type system of PCUIC from its implementation—in two steps. First, we provide an intermediate “algorithmic” specification, that is much closer to the implementation, and which we show equivalent to the declarative specification. This algorithmic specification uses acyclic graphs to represent universe constraints, equality up to reduction for conversion and a bidirectional version of typing [Lennon-Bertrand 2021; Pierce and Turner 2000] in order to constrain the use of the conversion rule to specific places, and get canonical typing derivations. The proof that the declarative and algorithmic presentations of PCUIC are equivalent requires strong meta-theoretical properties on the algorithmic version, such

<footnote n="4">⁴Despite the “Predicative” in the name, the calculus includes an impredicative sort *Prop*.</footnote>
*From a Trusted Code Base to a Trusted Theory Base Paradigm*. Thus, the assumed normalization with its accompanying requirements on the guard condition is the only Achilles heel of our formalization: if it holds, then there is no error in the implementation. So, this paper proposes to switch from a trusted code base to a trusted theory base paradigm! Moreover, if one of the assumed properties were false, the implementation might be wrong, but there would be a much more serious problem to fix in Coq's meta-theory. Without getting into philosophical debates, we argue that this work provides important assurances about the correctness of the system, that is complimentary to the many theoretical studies of variants of the Calculus of Constructions and Martin-Löf Type Theory from the literature [Coquand and Huet 1988; Martin-Löf 1998], of which none is as close to the calculus actually implemented in Coq as our work. True believers in computation and type theory might actually enjoy the relatively small, formal specification of the calculus implemented in Coq (a few pages for the typing and cumulativity rules). Our work also sheds light on the many formal properties of the calculus that are used by the implementation, are probably known by most developers of proof assistants, but are seldom spelled out in detail, and formally. We believe that getting a better understanding of those properties can serve as a guide for better and more efficient implementations in the near future.

To avoid unnecessary complications, we work with a mildly simplified version of Coq's core language we call PCUIC (for Predicative Calculus of Cumulative Inductive Constructions<fnref n="4" />), and show an equivalence with the implemented version (up to representation of strings and arrays). Note that the kernel of Coq also includes a module system, template polymorphism, η-conversion and efficient conversion algorithms, and primitive integers as well as arrays that we exclude for now.

*From Specification to Implementation.* We start by providing an entirely declarative version of the specification, as close as possible to its mathematical presentation on paper. For instance, the definition of the consistency of a polymorphic universe hierarchy via a valuation in natural numbers is very direct, without resorting to notions such as graphs of universes or acyclicity. Similarly, the specification of the cumulativity and conversion relations is a proper inductive judgmental equality judgment, which does not even mention a notion of reduction.

From this, we proceed by separating the specification of the type system of PCUIC from its implementation—in two steps. First, we provide an intermediate “algorithmic” specification, that is much closer to the implementation, and which we show equivalent to the declarative specification. This algorithmic specification uses acyclic graphs to represent universe constraints, equality up to reduction for conversion and a bidirectional version of typing [Lennon-Bertrand 2021; Pierce and Turner 2000] in order to constrain the use of the conversion rule to specific places, and get canonical typing derivations. The proof that the declarative and algorithmic presentations of PCUIC are equivalent requires strong meta-theoretical properties on the algorithmic version, such as confluence of reduction, or subject reduction, that are all formally proven. Note that this part of our work does not rely on normalization, thus the equivalence between the declarative and algorithmic presentations of PCUIC is axiom free.

Second, to move from the algorithmic specification to an actual implementation, we rely on the (iterated) comparison of weak-head normal forms (whnfs) to test cumulativity and conversion. Therefore, our proofs of soundness and completeness show that the abstract declarative specification can be decided this way, providing on the way a form of standardization theorem for reduction. Of course, termination of reduction to whnfs only holds if the system is strongly normalizing, and this is actually the only place where we need to use this axiom. This axiom is propositional, so we also know that none of the programs we develop can rely on its computational content, and it can

<footnote n="4">⁴Despite the “Predicative” in the name, the calculus includes an impredicative sort *Prop*.</footnote>
as confluence of reduction, or subject reduction, that are all formally proven. Note that this part of our work does not rely on normalization, thus the equivalence between the declarative and algorithmic presentations of PCUIC is axiom free.

Second, to move from the algorithmic specification to an actual implementation, we rely on the (iterated) comparison of weak-head normal forms (whnfs) to test cumulativity and conversion. Therefore, our proofs of soundness and completeness show that the abstract declarative specification can be decided this way, providing on the way a form of standardization theorem for reduction. Of course, termination of reduction to whnfs only holds if the system is strongly normalizing, and this is actually the only place where we need to use this axiom. This axiom is propositional, so we also know that none of the programs we develop can rely on its computational content, and it can be safely erased by extraction. The rest of the meta-theoretical properties have been developed entirely independently of it.

*A type-checking algorithm parametrized with decision procedures.* The type-checking algorithm is written in the form of proof-carrying code, because we are only able to call the conversion algorithm on well-typed terms (otherwise conversion checking may not terminate), and we thus cannot separate the correctness of the type checker from its definition. In practice, this means that the type checker is a complex interleaving of decision procedures (such as universe consistency checking or lookup in the global environment), and proof obligations saying that those checks are actually correct. So some extra care is needed to make sure that all decision procedures actually lead to pieces of code that can be run. To do so, we have parametrized the type checker by the various decision procedures and proofs that they are correct. This has two main advantages. First, we can later instantiate one decision procedure with a more efficient one, as long as it meets the specification. For instance, we can replace our current naive implementation of acyclicity and constraint checking with a more efficient one, such as the incremental cycle detection algorithm of Bender et al. [2015] actually used in the CoQ kernel, while being sure not to break anything in the type checker, as soon as we know that the efficient implementation fulfills the same specification. The second interest of dealing with an interface for decision procedures is that we can make sure not to use any other inlined decision procedure in the type-checking algorithm by putting all remaining pieces of information in Prop.

*Certified Extraction.* Finally, to get a reasonably fast implementation, we need to extract to an efficient language such as OCAML. In order to maintain the correctness guarantees on the extracted code, we also implement a proven correct type-and-proof erasure algorithm based on the work by Letouzey [2004], and complemented with a verified compilation from the target of erasure to OCAML [Forster et al. 2024]. Note that during the development of the type checking algorithm, we experienced difficulties because extraction was producing an ill-typed term, which supports our claim that a better-understood extraction is needed.

*Outline of the Paper.* We start in §2 with a high-level overview of the rich features of CoQ that we need to cover in PCUIC. §3 presents the precise abstract specification of universes, cumulativity/conversion as well as typing for PCUIC. §4 describes the equivalent algorithmic presentation of PCUIC, where universes are described using an acyclic graph, cumulativity is defined by reduction and typing is bidirectional. §5 presents the meta-theoretical properties of PCUIC—such as confluence and subject reduction—that are required to define the correct and complete type checking algorithm, whose definition is deferred to §6. The metatheory relates the declarative, algorithmic and bidirectional versions of the type system. §7 explains type and proof erasure for PCUIC. §8 discusses related work and §9 concludes and discusses future work.
be safely erased by extraction. The rest of the meta-theoretical properties have been developed entirely independently of it.

*A Type-checking algorithm parametrized with decision procedures.* The type-checking algorithm is written in the form of proof-carrying code, because we are only able to call the conversion algorithm on well-typed terms (otherwise conversion checking may not terminate), and we thus cannot separate the correctness of the type checker from its definition. In practice, this means that the type checker is a complex interleaving of decision procedures (such as universe consistency checking or lookup in the global environment), and proof obligations saying that those checks are actually correct. So some extra care is needed to make sure that all decision procedures actually lead to pieces of code that can be run. To do so, we have parametrized the type checker by the various decision procedures and proofs that they are correct. This has two main advantages. First, we can later instantiate one decision procedure with a more efficient one, as long as it meets the specification. For instance, we can replace our current naive implementation of acyclicity and constraint checking with a more efficient one, such as the incremental cycle detection algorithm of Bender et al. [2015] actually used in the CoQ kernel, while being sure not to break anything in the type checker, as soon as we know that the efficient implementation fulfills the same specification. The second interest of dealing with an interface for decision procedures is that we can make sure not to use any other inlined decision procedure in the type-checking algorithm by putting all remaining pieces of information in Prop.

*Towards a Certified Extraction.* Finally, to get a reasonably fast implementation, we need to extract to an efficient language such as OCAML. In order to maintain the correctness guarantees on the extracted code, we also implement a proven correct type and proof erasure algorithm based on the work by Letouzey [2004]. Note that during the development of the type checking algorithm, we experienced difficulties to extract it because extraction was producing an ill-typed term, which supports our claim that a certified extraction is needed.

*Outline of the Paper.* §2 presents the abstract specification of universes, cumulativity/conversion as well as typing for PCUIC. §3 describes the equivalent algorithmic presentation of PCUIC, where universes are described using an acyclic graph, cumulativity is defined by reduction and typing is bidirectional. §4 presents the meta-theoretical properties of PCUIC—such as confluence and subject reduction—that are required to define the correct and complete type checking algorithm, whose definition is deferred to §5. §6 explains type and proof erasure for PCUIC. §7 discusses related work and §8 concludes and discusses future work.

The complete CoQ formalization can be found on the META-CoQ project page<fnref n="5" />. The whole project is more than 300kloc of CoQ code and a thin layer of 10kLoC of OCAML to interoperate with CoQ’s implementation. It takes around 15 min to compile on a standard recent machine. The current article describes the 1.2 version of META-CoQ, available for CoQ 8.16 [The Coq Development Team 2022] as an OPAM package.<fnref n="6" /> In the remainder of the text, we refer to PCUIC: *MyFile* to indicate the file *PCUICMyFile.v* in the development. The electronic version has links to the *coqdoc* documentation on the web.

**Prior publication.** This paper is a substantial extension of a prior conference publication [Sozeau et al. 2019b]. The main addition is the proof of completeness, which is done by considering bidirectional type checking as an intermediate specification. Contrarily to this previous work, we present the certification of the type checker in two steps, first an equivalence between the

<footnote n="5">⁵https://github.com/MetaCoq/metacoq/tree/v1.2-8.16</footnote>

<footnote n="6">⁶See the installation instructions for details</footnote>
This paper introduces various judgment forms, all of which are summarized in Tables 1 and 2 to provide the reader with a comprehensive overview.

The complete Coq formalization can be found on the META-Coq project page.<fnref n="5" /> The whole project is more than 300kloc of Coq code and a thin layer of 10kLoC of OCaml to interoperate with Coq's implementation. It takes around 15 min to compile on a standard recent machine. The current article describes the 1.2 version of META-Coq, available for Coq 8.16 [The Coq Development Team 2022] as an OPAM package.<fnref n="6" /> In the remainder of the text, we refer to PCUIC: *MyFile* to indicate the file `PCUICMyFile.v` in the development. The electronic version has links to the `coqdoc` documentation on the web.

**Prior publication.** This paper is a substantial extension of a prior conference publication [Sozeau et al. 2019b]. The main addition is the proof of completeness, which is done by considering bidirectional type checking as an intermediate specification. Contrarily to this previous work, we present the certification of the type checker in two steps, first an equivalence between the mathematical specification of the system and its algorithmic specification, and then the equivalence with the decision procedure. This led us to the discovery of a completeness bug in Coq itself, which has then been corrected in Coq (since version 8.14) thanks to our work.

This paper also contains the first formal treatment of cumulative inductive types, in particular a proof of subject reduction for the resulting calculus. To date, only a semantic work over a simplified fragment was covered in the literature [Timany and Sozeau 2018]. Finally, we provide a complete and more precise formal proof of correctness for erasure, which was relying on conjectures in the conference version.

# 2 AN OVERVIEW OF COQ'S TYPE THEORY

Before diving into formal definitions, we provide a brief overview of the various features Coq offers to meet its users' needs, which we aim to support in META-Coq. This section is intended as a high-level summary rather than a detailed specification, assuming the reader has some familiarity with dependent type theory. Unless explicitly noted, all features discussed here are included in PCUIC, the slightly simplified version of Coq's core language that we specify.

## 2.1 Datatypes

*Inductive types*. Coq allows users to define and manipulate inductively defined datatypes, such as natural numbers. More notably, these inductive types can be *indexed* by other types, exemplified by the well-known case of length-indexed vectors:

Inductive vector $A: N \rightarrow Type :=$
| nil : vector A 0
| cons : V (h:A) (n:N), vector A n \rightarrow vector A (S n).

This is a powerful mechanism to embed complex invariants about data inside their type. It is also useful to inductively define propositions:

Inductive even : N \rightarrow Prop :=
| even_0 : even 0
| even_S (n : N) : odd n \rightarrow even (S n)
with odd : N \rightarrow Prop :=
| odd_S (n : N) : even n \rightarrow odd (S n).

<footnote n="5">⁵https://github.com/MetaCoq/metacoq/tree/v1.2-8.16</footnote>

<footnote n="6">⁶See the installation instructions for details</footnote>
Inductive term : Set :=
| tRel (n : N)
| tSort (u : universe)
| tProd (na : name) (A B : term)
| tLambda (na : name) (A t : term)
| tLetIn (na : name) (b B t : term)
| tApp (u v : term)
| tConst (k : kername) (ui : universe_instance)
| tInd (ind : inductive) (ui : universe_instance)
| tConstruct (ind : inductive) (n : N) (ui : universe_instance)
| tCase (indn : case_info) (p : predicate term) (c : term) (brs : list (branch term))
| tProj (p : projection) (c : term)
| tFix (mfix : mfixpoint term) (idx : N)
| tCoFix (mfix : mfixpoint term) (idx : N).

Fixpoint mkApps (t : term) (us : list term) : term :=
match us with
| [] ⇒ t
| u :: us ⇒ mkApps (tApp t u) us
end.

<caption>Fig. 1. Syntax of PCUIC</caption>

mathematical specification of the system and its algorithmic specification, and then the equivalence
with the decision procedure. This led us to the discovery of a completeness bug in Coq itself, which
has then been corrected in Coq (since version 8.14) thanks to our work.

This paper also contains the first formal treatment of cumulative inductive types, in particular a
proof of subject reduction for the resulting calculus. To date, only a semantic work over a simplified
fragment was covered in the literature [Timany and Sozeau 2018]. Finally, we provide a complete
and more precise formal proof of correctness for erasure, which was relying on conjectures in the
conference version.

## 2 PCUIC: COQ'S CORE CALCULUS SPECIFICATION

As a type system, PCUIC is an extension of the Predicative Calculus of (Co)-Inductive Constructions,
a Pure Type System with an infinite hierarchy of universes *Type*<sub>i</sub> and an impredicative sort *Prop*,
extended with cumulative inductive and coinductive type families. The system also includes *universe*
polymorphism [Harper and Pollack 1991; Sozeau and Tabareau 2014], making it flexible in handling
constructions that are generic in universes and cumulative inductive types as introduced and
justified by Timany and Sozeau [2017] with a pen and paper proof (for a variant of the calculus
with eliminators).

As a programming language, PCUIC is a standard pure dependent λ-calculus extended with
a let-in construct for local definitions, case analysis and projections of datatypes and mutual
(co)recursion operators.

The specification of PCUIC in Coq follows the pattern of the specification of the kernel of Coq
inside Coq itself, as already described by Anand et al. [2018] and Sozeau et al. [2019a]. We now
explain the syntax, universes, (untyped) cumulativity and typing judgments of PCUIC.
The above gives an example of *mutual inductive types*, which define at the same time multiple inductive types that refer to each other. Only constructors can refer to the other types in the mutual block, but not the inductive types themselves—this more complex feature is called induction-induction [Nordvall Forsberg 2013], and is currently not supported by Coq.

*Positivity.* To ensure critical properties like normalization (§5.5) and logical consistency, only specific datatypes are permitted: specifically, those that satisfy a *strict positivity criterion*. In essence, the arguments to constructors must be of a function type where the domain does not reference the inductive type, while the codomain can reference the inductive type, as illustrated by the example of countably-branching trees:

Inductive tree (A : Type) : Type :=
| leaf : tree A
| node (children : N → tree A) : tree A.

Moreover, an inductive type can be *nested*, meaning that the type can appear as argument to another inductive type. The standard example are so-called rose trees:

Inductive rose (A : Type) : Type :=
| rleaf : rose A
| rnode (children : list (rose A)) : rose A.

This adds a significant amount of complexity to the manipulation of inductive definitions, and is a challenge for tooling [Tassi 2019]. We currently do not cover nested inductive types in PCUIC (§3.6.1).

*Pattern matching and fixed points.* To use inductive values, Coq gives users access to two primitives, *pattern matching*, and a *fixed point constructor*:

Fixpoint is_even (n : N) : B :=
match n with
| 0 ⇒ true
| 1 ⇒ false
| S (S n') ⇒ is_even n'
end.

Although typically introduced with the top-level `Fixpoint` keyword, fixed points are given by a first-class term constructor. Moreover, complex pattern matchings such as the one above are not available in the kernel, which only understands a *primitive pattern matching* construction with exactly one case for each constructor. Thus, the above definition really boils down to the following, which is what Coq's kernel ultimately sees:

fix is_even (n : N) : B :=
match n return B with
| 0 ⇒ true
| S n0 ⇒ match n0 return B with
| 0 ⇒ false
| S n' ⇒ is_even n'
end
end

In the previous example, the `return` keyword is used. In the context of inductive types, this keyword specifies how the type of the pattern matching depends on the indices and the value of the scrutinee—the term being matched. The `as` and `in` keywords are employed to further refine this
## 2.1 Definition of the Syntax and Environments

The syntax of PCUIC is defined in Fig. 1. This inductive type is a direct representation of the constr datatype used in the implementation of Coq terms in OCAML. The only difference is that PCUIC's application `tApp` is binary-while it is *n*-ary in the OCAML implementation-and that PCUIC has no type cast construct<fnref n="7" />. We can define *n*-ary application *a posteriori* as the fixpoint `mkApps`, but this *n*-ary application is not primitive in PCUIC. The constructor `tRel` represents variables-using de Bruijn indices implemented as natural numbers-bound by abstractions (introduced by `tLambda`), dependent products (introduced by `tProd`) and local definitions (introduced by `tLetIn`). The type `name` is a printing annotation. Sorts are represented with `tSort`, which takes a `universe` as argument. A `universe` can be either `IProp` or a more complex expression representing one of the `IType` universes. More details are given in §2.2.

The three constructors `tConst`, `tInd` and `tConstruct` represent references to constants declared in a global environment. The first is for definitions or axioms, the second for (co)inductive types or record types, and the last for constructors of inductive types. Because we handle universe polymorphism, those three constructors take a `universe_instance`, which is a list of `Level`.

The constructor `tCase` represents pattern matching, where `p` is the return predicate, `c` is an inhabitant of the inductive type corresponding to `indn` and `brs` is the list of branches corresponding to each possible constructor of the inductive type.

The constructor `tProj` represents primitive projections for records, the argument `p` contains the name of the record type and a natural number indicating which field of the record type is projected. The term `c` is the inhabitant of the record type that is projected.

The constructors `tFix` and `tCoFix` respectively represents (mutual) fixpoints and cofixpoints. A mutual (co)fixpoint is a list of (co)fixpoint definitions, each containing a type (given by the field `dtype`) and a body (given by the field `dbody`). The natural number `idx` corresponds to the term focused on in the mutual definition. In other words, if `mfix` mutually defines $f_1, \dots, f_n$, then `tFix mfix k` corresponds to $f_k$. This focusing is needed because in its absence we would have a list of terms with a list of types, rather than a single term with a single type.

In PCUIC, the meaning of a term is relative to a global environment which is constant throughout a typing derivation, and to a local context which may increase when going under binders.

The *local context* consists of a list of declarations written in *snoc* order: we use the notation $\Gamma$, $d$ for adding $d$ at the head of $\Gamma$. We write $x : A$ for a declaration without a body (as introduced by `tLambda`) and $x := t : A$ for a declaration with a body (as introduced by `tLetIn`). The *global environment* consists of three parts: a list of declarations, properly ordered according to dependencies, a global universe context representing the global constraints and possibly some additional local universe declarations used to type-check the body of a universe polymorphic declaration. A declaration is either the declaration of a constant (a definition or an axiom, depending on the presence or absence of a body) or of a block of mutual inductive types, which brings both the inductive types and their constructors to the context. We defer the presentation of the (co-)inductive type structure to §2.6.

## 2.2 Universes

The universe hierarchy is used in PCUIC to avoid the so-called “Type-in-Type” paradox of MLTT— originally due to Girard [1972] and later simplified by Hurkens [1995]—which is the type-theoretic counterpart of Russell’s paradox in set theory. The standard mathematical representation of the

<footnote n="7">⁷Casts are only necessary to inform the kernel about which conversion algorithm to use, while we only implement one such algorithm. The implementation actually also includes constructors for existential variables instantiated at a given term substitution and named variables (hypothesis names in goals): we do not present them in this paper as they are dismissed by typing for the moment. They are not present in terms stored by Coq, but only used by higher layers.</footnote>
dependency, as shown in the following example:

Fixpoint even_is_even (n : N) : (is_even n = true) → even n :=
match n as x return is_even x = true → even x with
| 0 ⇒ fun _ ⇒ even_0
| 1 ⇒ fun (e : false = true) ⇒
  (match e in _ = x return (if x then even 1 else True) with
   | eq_refl ⇒ I
   end)
| S (S n') ⇒ fun e ⇒ even_S_ (odd_S_ (even_is_even n' e))
end.

While usually inferred by Coq's elaboration, this information is always present in full in the kernel's primitive pattern matching.

Just like inductive definitions, fixed points are constrained in order to retain normalization. This constraint is called the *guard condition*. In essence, recursive calls are only allowed on “subterms”. What qualifies as a subterm needs to be flexible enough to meet users’ expressivity requirements, which makes the current guard condition of Coq quite complex. Since its exact definition is not essential to any aspect of our work, our specification of PCUIC is parametrized by an abstract guard condition, subject to a few properties (§5.2.2).

Record types and primitive projections. CoQ provides special support for record types, tuples whose fields can be accessed through (named) projections:

Record sig (A : Type) (B : A → Type) : Type ::= {fst : A ; snd : B fst} . (* Record type *)
Definition pair : sig N (fun _ ⇒ B ) ::= {| fst := 0 ; snd := true |} . (* Record constructor *)
Definition fst fun {A : Type} {B : A → Type} (p : sig A B) : A := p.(fst) . (* Projections *)

Beyond the dedicated syntax, the main difference between records and one-field inductive types is the fact that records support *primitive projections*, an optimized presentation of field projections which only records the projection name, rather than a bunch of unnecessary arguments. For instance, in the example above, even if `fst fun p` can usually infer its implicit arguments `A` and `B`, they are still present, and need to be type-checked by the kernel. In contrast, these are simply absent from the term `p.(fst)`. In record-heavy settings, typically when using canonical structures or type classes, this distinction is crucial for performance. Moreover, non-recursive records support *η-equality*—see §2.3.

Coinductive types. The final kind of data types that CoQ supports is coinductive types: potentially infinite, lazy values. Coinductive types can be presented in two ways. The positive coinductive types are very similar to inductive types, being introduced by constructors and eliminated via pattern matching. The only difference is the guard condition for co-fixed points: a co-fixed point must construct a coinductive value with at least one constructor before calling itself recursively. This ensures productivity of functions targeting coinductive types, i.e., that they cannot run indefinitely without producing data.

CoInductive stream (A : Type) : Type ::=
| scons (head : A) (tail : stream A) : stream A.

CoFixpoint repeat (A : Type) (a : A) : stream A :=
scons _ a (repeat A a).
Inductive ConstraintType : Set := Le (z : Z) | Eq.

Definition UnivConstraint : Set := Level * ConstraintType * Level.

Record valuation := { valuation_mono : string → positive; valuation_pol y : N → N }.

Definition val (v : valuation) (l : Level) : Z :=
match l with
| lzero ⇒ 0
| level s ⇒ Z pos (v.(valuation_mono) s)
| lvar x ⇒ Z .of N (v.(valuation_pol y) x)
end.

<caption>Fig. 2. Definition of constraints and valuations</caption>

hierarchy is done by indexing occurrences of the universe *Type* with a natural number expressing its level in the hierarchy. In a practical setting, however, this presentation would be too rigid for a user. PCUIC therefore features monomorphic universes, which provide a way to refer to levels more abstractly with names, and polymorphic universes, which provide a way to quantify over those universes.

PCUIC features three kinds of level for a universe.

Inductive Level : Set := lzero | level (s : string) | lvar (n : N).

The constructor lzero refers to the smallest level, and corresponds to the encoding of the universe printed as Set in Coq. Constructor level s encodes a monomorphic universe with name s (i.e., traditional global universes), while lvar n represents a polymorphic universe, where n is the de Bruijn level of the corresponding variable in the universe context.

Definition UnivExpr := Level × N.

Inductive universe := lProp | lType (ls : nonEmptyUnivExprSet).

Then, a UnivExpr is a pair (1,n) of a level 1 and a natural number n, meaning intuitively that we
are talking about the universe 1+n. Finally, a universe is either lProp or lType ls, where ls is a
non-empty set of UnivExpr. The non-empty set ls of UnivExpr is interpreted as an encoding for
the maximum of its elements, representing so-called "algebraic" universes. For instance, the term
tSort (lType { (u,0) ; (v,1) }) encodes the universe that is usually written Type max(u,v+1) in the literature.
In the remainder, we write tProp for the term tSort lProp.

*Constraints and Valuations.* To allow for a flexible and modular account of universes, Coq implements typical ambiguity and universe polymorphism. The universe hierarchy is hence not fixed but rather maintained using an extensible (“elastic”, as coined by its original designer Gérard Huet [1988]) set of universe levels and associated constraints (UnivConstraint) which say that a level is at least z times smaller or equal (Le z) or equal (Eq) to another level, as described in Fig. 2. Universe polymorphism [Harper and Pollack 1991; Sozeau and Tabareau 2014] further adds the possibility to make definitions and inductive types polymorphic in the set of universe levels and constraints, so that they can be reused at different levels. This is akin to bounded prenex polymorphism à la ML. In the Coq type checker, consistency of the universe hierarchy is checked using an acyclicity criterion on the graph induced by the constraints. However, this characterization of consistency is quite far from the mathematical model, which says that universe levels are natural numbers. To keep the specification as close as possible to the meta-theory, we therefore introduce the notion of valuation
Positive coinductive types have a rather ill-behaved meta-theory. In particular, they do not satisfy subject reduction.<fnref n="7" /> In part to circumvent this issue, the alternative *negative coinductive types* were introduced, inspired by Abel et al. [2013]. These simply are recursive records, with a productivity constraint on their co-fixed points similar to their positive counterparts:

```
CoInductive stream' (A : Type) : Type :=
    { head' : A ; tail' : stream' A }.
```

```
CoFixpoint repeat' (A : Type) (a : A) : stream' A :=
    {| head' := a ; tail' := repeat' A a |}.
```

In PCUIC, we support the two variants in parts of the development—for instance, confluence (§5.3) and most of the meta-theory is proven for both—but the positive variant is disallowed via a flag system for the subject reduction theorem (§5.4).

## 2.2 Sorts and universes

A second, perhaps less visible, source of complexity in the implementation of CoQ are sorts: types whose inhabitants are themselves types, that is `Type`, `Set`, `Prop` and the recently introduced `SProp`.

*Monomorphic universes.* It is well known since Girard [1972] that the simple `Type` : `Type` typing rule is logically inconsistent, and leads to a non-normalising system. The typical theoretical solution is to introduce a hierarchy of `Type` sorts, indexed by natural numbers, each typed by the next: `Type₀` : `Type₁` : `Type₂` : ... In practice, though, this has been found too tedious to use, requiring to specify precisely each type universe, so more complex mechanisms are at work in CoQ. They retain the idea that each occurrence of `Type` contains a *universe*, corresponding to its “height” in a hierarchy. However, this universe is not merely an integer.

Harper and Pollack [1991] have proposed the first approach to this issue, where universes are morally algebraic expressions built from *global universe levels*. Each time a user writes `Type`, a new such universe level is generated for this occurrence. The type checker collects constraints on universes, and offloads them to a dedicated sub-routine that verifies that this collection of constraints is consistent—meaning that there exists a *valuation*, a mapping from levels to integers, that satisfies them. This is directly inspired by the typical ambiguity principle introduced by Bertrand Russell in Principia Mathematica, where a similar stratification was introduced in set theory to avoid paradoxes. The sort `Set` essentially represents the bottom of the hierarchy, what would correspond to `Type` at level 0 in an integer-based hierarchy.

*Cumulativity.* For this approach to be flexible enough, Huet [1988] introduced a notion of *cumulativity* of universes and a refined constraint checker. Cumulativity means that universes are subject to a partial order, which gives rise to a form of subtyping whereby an occurrence of `Type` is a subtype of another if its universe is smaller. This subtyping, combined with computation rules in the *cumulativity* relation, generalizes the conversion (definitional equality) typically used by dependent type systems.

*Propositions.* In addition to the `Type` sorts, CoQ also features two others dedicated to propositions: types whose inhabitants are *proofs*. Proofs are terms which should intuitively not participate in the computational behavior of programs—a property which is usually called *proof irrelevance*. This separation between relevant and irrelevant content is important for extraction (§7), the process

<footnote n="7">⁷This was a conscious design decision when coinductive types were first introduced [Giménez 1996]: the alternative was to break decidability of type checking.</footnote>
on universe levels, which associates 0 to `lzero`, a positive number to monomorphic universes (a monomorphic universe cannot be `lzero`) and a natural number to polymorphic universes.

Then a valuation satisfies a set of constraints when:

Inductive satisfies<sub>0</sub> (v : valuation) : UnivConstraint → Prop :=
| satisfies<sub>0</sub>_Le (l l' : Level) (z : Z) : val v l ≤ val v l' - z → satisfies<sub>0</sub> v (l, Le z, l')
| satisfies<sub>0</sub>_Eq (l l' : Level) : val v l = val v l' → satisfies<sub>0</sub> v (l, Eq, l').

Definition satisfies v : UnivConstraintSet → Prop := For_all (satisfies<sub>0</sub> v).

The universe hierarchy is consistent when there exists a valuation which satisfies its set of constraints:

Definition consistent ctrs := ∃ v, satisfies v ctrs.

Note that this definition of consistency is not a priori decidable, and this is the point of §3.1 to
provide an alternative specification using acyclicity of a graph, which is a checkable and modular
property.

*Cumulativity on universes.* The notion of subtyping on types is defined as definitional equality up to cumulativity on universes, which states that `tSort l` is a subtype of `tSort l'` as soon as `l` is smaller than `l'`. Comparison of universes depends on the set of constraints under consideration. Indeed, a universe `u` is smaller than a universe `u'` for a given set of constraints `φ` when for any valuation which satisfies `φ`, the value of `u` is smaller than the value of `u'`. Formally, it is defined as follows:

Definition leq_universe (φ : UnivConstraintSet) u u' :=
∀ v : valuation, satisfies v φ → (val v u ≤ val v u').

Similarly, `eq_universe` defines when two universes are equal. The notion of comparison is extended to `tProp` by stating that it is smaller than any other universe if the flag governing the `Prop ≤ Type` rule is set, and incomparable otherwise. We will see in §4 and 6 that correctness of erasure holds only in a theory without this rule.

Finally, the function `global_ext_constraints` collects the universe constraints appearing in a global environment Σ.

2.3 Cumulativity

Conversion is one of the key ingredient for the definition of dependent type theories. It implements a syntactic notion of equality that can be used during typing to use a term of type A when a term of type B was expected, under the condition that A and B are convertible. In the case of CoQ and of PCUIC, this notion of conversion is untyped, i.e., it relates terms without making use of the types of those terms, in contrast with the typed definitional equality judgment which is customary in Martin-Löf Type Theory [Martin-Löf 1984]. Moreover, conversion further refines to a notion of cumulativity that extends it with a subtyping rule: `Type<sub>i</sub>` is a subtype of `Type<sub>j</sub>` when `i ≤ j` in the hierarchy, as described in §2.2.

The specification of cumulativity between two terms t and u, written Σ ; Γ ⊢ t ≤<sub>s</sub><sup>R1e</sup> u, is relative to a global context Σ and a local context Γ and is parametrized by a relation R1e between universes. We use the s subscript (for specification) to distinguish it later on from the algorithmic presentation of cumulativity, written Σ ; Γ ⊢ t ≤<sub>a</sub><sup>R1e</sup> u. When R1e is instantiated with leq_universe (global_ext_constraints Σ), this gives rise to the notion of cumulativity (written ≤<sub>s</sub>), and when it is instantiated with Re := eq_universe (global_ext_constraints Σ), it boils down to conversion (written ≈<sub>s</sub>).
which takes a Coq term and turns it into a program in e.g., OCAML, and among other things erases all proofs.

The older sort `Prop` enforces this by constraining pattern matching on inductive types whose codomain sort is `Prop`. This restriction, called *subsingleton elimination*, forbids programs that branch on propositional values:

```coq
Definition ex_falso (f : ⊥) : N :=
    match f with end. (* allowed *)
```

```coq
Fail Definition forbidden (o : True ∨ True) : N :=
    match o with
    | or_introl _ ⇒ 0
    | or_intror _ ⇒ 1
end.
```

The sort `Prop` has a somewhat special place with respect to the `Type` hierarchy. On one side, it is smaller than any `Type` with respect to cumulativity. On the other, it is *impredicative*: any quantification $\forall x : A, P$ is of type `Prop` as soon as $P$ is, making the logic of `coqeProp` comparable to that of Zermelo-Fraenkel Set Theory.

While `Prop` is merely compatible with proof irrelevance—the statement $\forall (P : Prop) (p q : P), p = q$ is neither provable nor refutable—the sort `SProp` [Gilbert et al. 2019] of *strict propositions* goes further. Indeed, Coq automatically identifies two inhabitants of the same $P : SProp$ up to conversion. To allow for this, `SProp` is more restricted than `Prop`: its equivalent of the subsingleton criterion is less permissive, and `SProp` is not in cumulativity with any other sort.

PCUIC covers `Prop` with all its properties. `SProp` is also present, although the integration of its main characteristic, definitional proof irrelevance, is currently a work in progress [Leray 2022].

*Polymorphic universes.* The system of monomorphic universes goes a long way, but the fact that all instances of the same definition share the same global universe can be limiting in cases such as the following:

```coq
Definition id (A : Type) (a : A) := a.
Fail Check (id _ id).
```

Or, for a more mathematically interesting example, to define a category of categories. This issue can be fixed by manual duplication, e.g., defining small categories and a large category of small categories. But of course this then incurs duplication of all definitions and theorems, and quickly becomes unmanageable.

*Universe polymorphism* [Sozeau and Tabareau 2014] solves this issue by letting definitions be polymorphic over their universe levels, in an implicit prenex fashion, similar to type polymorphism in ML languages. Every time a universe polymorphic definition is used, new fresh universe levels are generated for this particular use—just as when using `Type`. With universe polymorphism, the example of `id` above checks, because the two instances of `id` are instantiated with different universe levels, and one can be smaller than the other.

*Template and sort polymorphism.* Universe polymorphism does not encompass `Prop` or `SProp`, although in many cases one would want to extend polymorphic definitions to these, e.g., the case of (dependent) pairs, which come in three flavours in the standard library of Coq. An ad-hoc mechanism called *template polymorphism* has long existed to allow for a limited form of this.

However, it is considered legacy, and is planned to be supplanted by a more general form of *sort polymorphism* [Gilbert et al. 2023] which extends universe polymorphism to also consider
The complete definition has 24 rules which can be found in the Appendix (Figs. 19 and 20). To avoid clutter, we prefer to describe the rules grouped by their purpose, dealing with ordering, cumulativity, computation or congruence. Note also that in the definition of Figs. 19 and 20, we take the liberty of directly using the notation in the header, which is possible in systems such as AGDA, but not in COQ. We believe this makes the definition easier to read and avoids the need to introduce an auxiliary useless name. We will do so for several inductive definitions in this paper.

### 2.3.1 Ordering Rules.
There are three rules to enforce the specification of cumulativity to be a pre-order and conversion to be an equivalence relation.

$$ \begin{array}{l} \texttt{cumul\_Refl} : \forall t, \\ \qquad \Sigma; \Gamma \vdash t \leq_s^{\text{Re}} t \\ \texttt{cumul\_Sym} : \forall t u, \\ \qquad \Sigma; \Gamma \vdash t \approx_s u \rightarrow \\ \qquad \Sigma; \Gamma \vdash u \leq_s^{\text{Re}} t \end{array} \qquad \begin{array}{l} \texttt{cumul\_Trans} : \forall t u v, \\ \qquad \Sigma; \Gamma \vdash t \leq_s^{\text{Re}} u \rightarrow \\ \qquad \Sigma; \Gamma \vdash u \leq_s^{\text{Re}} v \rightarrow \end{array} \qquad \begin{array}{l} \texttt{is\_closed\_context} \Gamma \rightarrow \texttt{is\_open\_term} \Gamma u \rightarrow \\ \qquad \texttt{is\_closed\_context} \Gamma \rightarrow \texttt{is\_open\_term} \Gamma u \rightarrow \\ \qquad \Sigma; \Gamma \vdash t \leq_s^{\text{Re}} u \rightarrow \Sigma; \Gamma \vdash u \leq_s^{\text{Re}} v \rightarrow \end{array} \qquad \Sigma; \Gamma \vdash t \leq_s^{\text{Re}} v $$

Rules `cumul_Trans` and `cumul_Refl` state that cumulativity is transitive and reflexive, and Rule `cumul_Sym` states that only conversion is symmetric. Note that the Rule `cumul_Sym` can also be used to show that conversion is included in cumulativity (by using the rule twice).

We would like to mention a technical difficulty here, in presence of untyped cumulativity and conversion. The transitivity rule needs to be restricted to introduce only a term `u` whose free variables appear in a closed context `Γ`, as ensured by the `is_closed_context` `Γ` and `is_open_term` `Γ` `u` conditions. This is necessary to maintain the invariant that a proof of conversion between two well-scoped terms only involves well-scoped terms. This invariant is important because reduction of non-well-scoped terms is not confluent (this is explained in §4.3.1) and thus the correspondence with algorithmic conversion (see §3.2.2) only works on well-scoped terms.

### 2.3.2 Cumulativity Rules.
There are three rules dealing with cumulativity of both universes and inductive types.

$$ \begin{array}{l} \texttt{cumul\_Ind} : \forall i u u' \text{ args args',} \\ \qquad \texttt{R_global_instance} \Sigma \text{ Re Re} (\text{IndRef } i) \#|\text{args}| u u' \rightarrow \\ \qquad \texttt{All2} (\texttt{fun } t u \Rightarrow \Sigma; \Gamma \vdash t \leq_s^{\text{Re}} u) \text{ args args'} \rightarrow \\ \qquad \Sigma; \Gamma \vdash \text{mkApps} (\texttt{tInd } i u) \text{ args} \leq_s^{\text{Re}} \text{mkApps} (\texttt{tInd } i u') \text{ args'} \\ \\ \texttt{cumul\_Construct} : \forall i k u u' \text{ args args',} \\ \qquad \texttt{R_global_instance} \Sigma \text{ Re Re} (\text{ConstructRef } i k) \#|\text{args}| u u' \rightarrow \\ \qquad \texttt{All2} (\texttt{fun } t u \Rightarrow \Sigma; \Gamma \vdash t \leq_s^{\text{Re}} u) \text{ args args'} \rightarrow \\ \qquad \Sigma; \Gamma \vdash \text{mkApps} (\texttt{tConstruct } i k u) \text{ args} \leq_s^{\text{Re}} \text{mkApps} (\texttt{tConstruct } i k u') \text{ args'} \end{array} \qquad \begin{array}{l} \texttt{cumul\_Sort} : \forall s s', \\ \qquad \texttt{Rle s s'} \rightarrow \\ \qquad \Sigma; \Gamma \vdash \texttt{tSort s} \leq_s^{\text{Re}} \texttt{tSort s'} \end{array} $$

Rule `cumul_Sort` is the direct expression of the subtyping rule on universes, while Rules `cumul_Ind` and `cumul_Construct` deal with cumulativity for inductive types. Following Timany and Sozeau [2017], `cumul_Ind` states that two *fully applied* inductive types are in the cumulativity relation when their arguments are convertible,<fnref n="8" /> and when their universe levels are related according to the variance of `tInd` `i` `u` registered in the global environment `Σ`. Rule `cumul_Construct` ensures similarly that the two *fully applied* constructors live in inductive types which are in the cumulativity relation. We will explain cumulativity of inductives types in more detail in §2.6.2.

### 2.3.3 Computation Rules.
There are 9 rules representing computation in PCUIC of various kinds (functions, pattern-matching, (co)fixpoints, definitions, projections).

$$ \begin{array}{l} \texttt{cumul\_beta} : \forall n a t b a, \\ \qquad \Sigma; \Gamma \vdash tApp (\texttt{tLambda} na t b) a \leq_s^{\text{Re}} b \{0 := a\} \\ \texttt{cumul\_zeta} : \forall n a b t b', \\ \qquad \Sigma; \Gamma \vdash tLetIn na b t b' \leq_s^{\text{Re}} b' \{0 := b\} \end{array} $$

<footnote n="8">⁸This condition on the list of arguments is ensured using the `All2` predicate which requires that the elements of the list are pointwise related, here by conversion.</footnote>
the “quality” of a sort, i.e., it being a type, proposition or strict proposition. This mechanism is experimentally introduced in recent versions of Coq.

Because of its legacy status and complexity, PCUIC does not try to specify template polymorphism. Sort polymorphism has not yet been integrated either.

## 2.3 Other Features of Coq Present in PCUIC

Let bindings. CoQ allows one to use local `let` bindings virtually everywhere. While seemingly innocuous, in a dependently typed setting this introduces an important specificity: the body of the `let` is aware of the value of the bound variable. For instance, the following is well typed:

Definition test : 0 = 0 := let x := 0 in (eq_refl x : 0 = 0).

Compare to the behavior of a similar $\lambda$-abstraction, whose type-checking fails as $x$ can no longer be converted to $0$ under the binder:

Fail Definition test' : 0 = 0 := (fun x = eq_refl x : 0 = 0) 0.

Thus, all contexts in CoQ and PCUIC contain variables that are either abstract (without body, such as those introduced by $\lambda$-abstractions), or defined (as introduced by a `let`), and one must carefully adapt the definitions of valid renaming, substitution, etc.

## 2.4 Other Features of Coq Absent from PCUIC

$\eta$-conversion. Beyond the computation rules for functions, (co-)inductive types, local and global definitions, projections and (co-)fixed points, the equational theory used by CoQ to compare types also contains the so-called $\eta$-conversion rules for functions and non-recursive records with primitive projections.<fnref n="8" /> That is, the following example is well typed in CoQ—for the second one, provided the Primitive Projection flag is active:

Check (fun f : N → N ⇒ eq_refl) : ∀ f : N → N, f = (fun x = f x).

Check (fun p : sig N (fun _ ⇒ B) ⇒ eq_refl) :
∀ p : sig N (fun _ ⇒ B), p = {| fst := p.(fst) ; snd := p.(snd) |}.

When introduced in CoQ 8.4, $\eta$-conversion came with the following justification:

The addition of $\eta$-conversion is justified by the confidence that the formulation of the Calculus of Inductive Constructions based on typed equality (such as the one considered in Lee and Werner to build a set-theoretic model of CIC [Lee and Werner 2011]) is applicable to the concrete implementation of Coq.

While we also believe this, the current presentation of PCUIC is based on untyped conversion, which is fundamental to the structure of the development. Yet, this makes it difficult to incorporate $\eta$-conversion, explaining why PCUIC does not currently support it.

Primitive types. To facilitate efficient operations, CoQ allows direct manipulation of machine integers, strings, and arrays. It offers a variety of primitive operations for these data types, along with an axiomatization of their behavior. In PCUIC, these are only partially supported—literal primitive constants can be typed, but the computational behavior of primitive operations is not specified and is treated axiomatically. While these features are currently limited, we anticipate no significant challenges in fully supporting them in the future.

<footnote n="8">⁸$\eta$-conversion for recursive records breaks decidability of conversion [McBride 2009].</footnote>
Rules `cumul-beta` and `cumul-zeta` encode usual computation of function application and of the let-binding construct. They make use of **substitution** `b{0 := a}` which is a shorthand for the use of the capture-avoiding de Bruijn instantiation function.

```
cumul_rel : ∀ i body,
  option_map decl_body (nth_error Γ i) = Some (Some body) →
  Σ ; Γ ⊢ tRel i ≤_s^Rle lift_0 (S i) body
```

Rule `cumul_rel` deals with variables in the local context that have a body, corresponding to definitions as introduced by `tLetIn`. The body is lifted to be well scoped in Γ.

```
cumul_iota : ∀ ci c u args p brs br,
  nth_error brs c = Some br → #|args| = (ci.(ci_npar) + context_assumptions br.(bcontext)) →
  Σ ; Γ ⊢ tCase ci p (mkApps (tConstruct ci.(ci_ind) c u) args) brs ≤_s^Rle iota_red ci p args br
```

Rule `cumul_iota` corresponds to computation of pattern-matching, ensuring that the constructor is fully applied and selecting the right branch. The function `iota_red` computes the right substitution of the selected branch `br`.

```
cumul_fix : ∀ mfix idx args narg fn,
  unfoldoprof mfix idx = Some (narg, fn) → is_constructor narg args = true →
  Σ ; Γ ⊢ mkApps (tFix mfix idx) args ≤_s^Rle mkApps fn args
```

Rule `cumuloprof` corresponds to fixpoint unfolding when the fixpoint is applied to a constructor of the corresponding inductive type. This restriction ensures that fixpoints cannot be unfolded forever, so as to preserve termination.

```
cumul_cofix_case : ∀ ip p mfix idx args narg fn brs,
  unfold_cofix mfix idx = Some (narg, fn) →
  Σ ; Γ ⊢ tCase ip p (mkApps (tCoFix mfix idx) args) brs ≤_s^Rle tCase ip p (mkApps fn args) brs
```

```
cumul_cofix proj : ∀ p mfix idx args narg fn,
  unfold_cofix mfix idx = Some (narg, fn) →
  Σ ; Γ ⊢ tProj p (mkApps (tCoFix mfix idx) args) ≤_s^Rle tProj p (mkApps fn args)
```

Dually, Rules `cumul_cofix_case` and `cumul_cofixproj` describe how cofixpoints can also be unfolded when forced by a pattern-matching or projection, that is when they are the scrutinees of `tCase` or `tProj`.

```
cumul_delta : ∀ c decl body (isdecl : declaredConstant Σ c decl) u,
  decl.(cst_body) = Some body →
  Σ ; Γ ⊢ tConst c u ≤_s^Rle body@[u]
```

Rule `cumul_delta` represents constant unfolding from the global environment `Σ`. In case the definition is universe polymorphic, its universes are instantiated, which is written `body@[u]`.

```
cumulproj : ∀ i pars narg args u arg,
  nth_error args (pars + narg) = Some arg →
  Σ ; Γ ⊢ tProj (i, pars, narg) (mkApps (tConstruct i 0 u) args) ≤_s^Rle arg
```

Finally, Rule `cumulproj` describes projection of record types, relating the projection of the constructor of a record to the corresponding field.
Inductive term: Set :=
| tRel (n: N) (* de Bruijn local variable *)
| tSort (u: universe) (* Prop | SProp | Type@{u} *)
| tProd (na: name) (A B: term) (* V na : A, B *)
| tLambda (na: name) (A t: term) (* fun na : A ⇒ t *)
| tLetIn (na: name) (a A t: term) (* let na : A := a in t *)
| tApp (u v: term) (* u v *)
| tConst (k: kername) (ui: universe_instance) (* k@[ui] *)
| tInd (ind: inductive) (ui: universe_instance) (* ind@[ui] *)
| tConstruct (ind: inductive) (n: N) (ui: universe_instance) (* (ind,n)@[ui] *)
| tCase (indn: case_info) (p: predicate term) (c: term) (brs: list (branch term))
| tProj (p: projection) (c: term) (* c.(p) *)
| tFix (mfix: mfixpoint term) (idx: N) (* fix mfix for idx *)
| tCoFix (mfix: mfixpoint term) (idx: N). (* cofix mfix for idx *)

Fixpoint mkApps (t: term) (us: list term): term :=
match us with
| [] ⇒ t
| u:: us ⇒ mkApps (tApp t u) us
end.

<caption>Fig. 1. Syntax of PCUIC</caption>

Modules and functors. Similarly to OCAML, COQ has a module system [Soubiran 2010], which differs from the first-class record system in that it also encompasses top-level constructs such as inductive definitions, as well as many non-kernel features (notations, type classes, etc.). It is used in particular to represent file imports, and is more generally responsible for name-spacing. While basic modules are relatively straightforward, the behavior of functors, modules taking other modules as arguments, module signatures and mixes are rather subtle. This system is currently outside the scope of PCUIC, and we conjecture that efforts to formalize the module system would be mostly orthogonal to our existing formalization.

3 PCUIC: COQ'S CORE CALCULUS SPECIFICATION

As a type system, PCUIC is an extension of the Predicative Calculus of (Co-)Inductive Constructions, a Pure Type System with an infinite hierarchy of universes Typeᵢ and an impredicative sort Prop, extended with cumulative inductive and coinductive type families. The system also includes *universe polymorphism* [Harper and Pollack 1991; Sozeau and Tabareau 2014], making it flexible in handling constructions that are generic in universes and cumulative inductive types as introduced and justified by *Timany and Sozeau* [2017] with a pen and paper proof (for a variant of the calculus with eliminators).

As a programming language, PCUIC is a standard pure dependent λ-calculus extended with a let-in construct for local definitions, case analysis and projections of datatypes and mutual (co)recursion operators.

The specification of PCUIC in CoQ follows the pattern of the specification of the kernel of CoQ inside CoQ itself, as already described by Anand et al. [2018] and Sozeau et al. [2019a]. We now explain the syntax, universes, (untyped) cumulativity and typing judgments of PCUIC.
### 2.3.4 Congruence Rules.
The last set of rules deals with congruence closure of the cumulativity relation. There is one rule per term constructor of PCUIC, which basically amounts to checking recursively that the arguments are in the cumulativity relation. There is a minor subtlety however, because cumulativity of PCUIC is only equivariant on the left-hand side of an arrow,<fnref n="9" /> which means that in the following rule for products, while b and b' are recursively compared for cumulativity, a and a' are only compared for conversion.

cumul_Prod : ∨ na na' a a' b b',
            eq_binder_annot na na' →
            Σ ; Γ ⊢ a ≤<sub>s</sub> Conv a' →
            Σ ; Γ , na : a ⊢ b ≤<sub>s[pb]</sub> b' →
            Σ ; Γ ⊢ tProd na a b ≤<sub>s[pb]</sub> tProd na' a' b'

The complete set of congruence rules can be found in Fig. 20.

## 2.4 Dealing with the Guard Condition

Before giving the specification of typing, we need to introduce two guard conditions that determine when recursive and corecursive definitions are valid. Those conditions are used in the typing rules of fixpoints and cofixpoints, ensuring strong normalization of PCUIC. We defer the discussion on strong normalization to § 4.5, but we can already say that strong normalization is treated as an axiom in our framework that depends on the notion of guard condition.

To make apparent that the guard conditions for fixpoints and cofixpoints share many properties, we parametrize the definition of the guard condition by the two-valued type FixCoFix, thus having only one predicate, dealing with fixpoints when the value is Fix, and cofixpoints otherwise. We thus postulate (in PCUIC: Typing) the existence of a guard condition checker as follows:

Inductive FixOrCoFix : Type := Fix | CoFix.
Axiom guard : FixOrCoFix → global_env_ext → context → mfixpoint term → Prop.
Definition fix-guard := guard Fix.
Definition cofix-guard := guard CoFix.

This presentation has two main advantages. First, it makes it clear that our meta-theoretic study of reduction and typing (§ 4), and in particular our proof of subject reduction, does not depend on a particular guard condition. Rather, it only relies on a few stability properties (e.g., stability by reduction or substitution). These conditions are listed in PCUIC: GuardCondition, and § 4.2.2 describes in more details the axiom of stability under reduction and substitution. Second, it makes explicit that while we need the guard condition to imply strong normalization in order to implement a terminating type checker, this normalization axiom is not necessary for most of the meta-theoretic development, and it indeed appears very late in the formalization. As we cannot prove strong normalization anyway due to Gödel’s incompleteness theorem, we believe that our axiomatic presentation makes more sense as it sheds light on the exact syntactic properties that must be satisfied by any guard condition on (co)fixpoints.

In Coq, the guard condition for fixpoints that is implemented is based on recursive calls which must be done on strict sub-terms.<fnref n="10" /> We do not enter into those details in this section, and they are not useful for the definition of typing; all that matters is that the typing rules of fixpoints and cofixpoints make use of this guard condition.

<footnote n="9">⁹This restriction comes from the fact that it is difficult to model contravariant cumulativity in set-theoretic models [Timany and Sozeau 2018]. Whether cumulativity could be contravariant on the left-hand side of an arrow or not is still the subject of ongoing theoretical investigations.</footnote>

<footnote n="10">¹⁰Actually the condition is slightly more general, but this is beyond the scope of this paper.</footnote>
COMPREHENSIVE LIST OF JUDGMENT FORMS

For reference, Tables 1 and 2 provide a comprehensive list of all judgment forms, along with references to the sections where each one is introduced.

<table><caption>Table 1. List of judgment forms</caption><thead><tr><th>Name</th><th>Notation</th><th>Reference</th></tr></thead><tbody><tr><td>Cumulativity</td><td>Σ; Γ ⊢ t &le;<sup>R1e</sup><sub>s</sub> u</td><td>§3.3</td></tr><tr><td>Typing</td><td>Σ; Γ ⊢ t : T</td><td>§3.5</td></tr><tr><td>Local context formation</td><td>wf_local Σ Γ</td><td>§3.5</td></tr><tr><td>Positivity</td><td>m; Γ ⊢<sup>arg</sup><sub>+</sub> ty</td><td>§3.6.1</td></tr><tr><td>Strict positivity</td><td>m@i; Γ ⊢<sup>+</sup> ty</td><td>§3.6.1</td></tr><tr><td>Global environment well-formedness</td><td>wf Σ</td><td>§3.6</td></tr><tr><td>Single step reduction</td><td>Σ; Γ ⊢ t &harr; u</td><td>§4.2.1</td></tr><tr><td>Syntactic equality up to universes</td><td>Σ ⊢ t &le;<sup>R1e</sup><sub>napp</sub> u</td><td>§4.2.1</td></tr><tr><td>Inference</td><td>Σ; Γ ⊢ t ⊢ T</td><td>§4.3.1</td></tr><tr><td>Checking</td><td>Σ; Γ ⊢ t &larr; T</td><td>§4.3.1</td></tr><tr><td>Constrained inference</td><td>Σ; Γ ⊢ t ⊢ Π (na,A,B)</td><td>§4.3.1</td></tr><tr><td>Algorithmic cumulativity</td><td>Σ; Γ ⊢ T &le; [R1e] U</td><td>§5.3.4</td></tr><tr><td>Algorithmic context cumulativity</td><td>Σ ⊢ Γ' &le; [R1e] Γ</td><td>§5.3.4</td></tr><tr><td>Parallel reduction</td><td>Γ, t &harr; Δ, t'</td><td>§5.3</td></tr><tr><td>One-step weak call-by-value reduction</td><td>Σ ⊢ t &harr;<sub>wcbv</sub> t'</td><td>§5.6</td></tr><tr><td>Type and proof erasure</td><td>Σ; Γ ⊢ t &harr; ε t'</td><td>§7.3</td></tr><tr><td>Weak call-by-value (big-step) evaluation</td><td>Σ ⊢ t &harr; v</td><td>§7.3</td></tr></tbody></table>

<table><caption>Table 2. List of derived judgment forms</caption><tr><td>Σ; Γ ⊢ t &le; u</td><td>:=</td><td>Σ; Γ ⊢ t &le;<sup>R1e</sup><sub>s</sub> u where R1e := leq_universe (global_ext_constraints Σ)</td></tr><tr><td>Σ; Γ ⊢ t &approx; u</td><td>:=</td><td>Σ; Γ ⊢ t &le;<sup>R1e</sup><sub>s</sub> u where R1e := eq_universe (global_ext_constraints Σ)</td></tr><tr><td>Σ; Γ ⊢ t &harr;* u</td><td>:=</td><td>clos_refl_trans (fun t u : term &rarr; Σ; Γ ⊢ t &harr; u)</td></tr><tr><td>Σ &harr; ε Σ'</td><td>:</td><td>Pointwise extension of &harr;ε</td></tr></table>

## 3.1 Definition of the Syntax and Environments

The syntax of PCUIC is defined in Fig. 1. This inductive type is a direct representation of the constr datatype used in the implementation of Coq terms in OCAML. The only difference is that PCUIC’s application tApp is binary—while it is n-ary in the OCAML implementation—and that PCUIC has no type cast construct.<fnref n="9" /> We can define n-ary application a posteriori as the fixpoint mkApps, but this n-ary application is not primitive in PCUIC. The constructor tRel represents variables—using de Bruijn indices implemented as natural numbers—bound by abstractions (introduced by tLambda), dependent products (introduced by tProd) and local definitions (introduced by tLetIn). The type

<footnote n="9">⁹Casts are only necessary to inform the kernel about which conversion algorithm to use, while we only implement one such algorithm. The implementation actually also includes constructors for existential variables instantiated at a given term substitution and named variables (hypothesis names in goals): we do not present them in this paper as they are dismissed by typing for the moment. They are not present in terms stored by Coq, but only used by higher layers.</footnote>
## 2.5 Definition of Typing

The typing rules of PCUIC are defined as an inductive family, written $Σ; Γ ⊢ t : T$, where $Σ$ is a global environment, $Γ$ is a local context and $t$ and $T$ are terms. The pointwise extension of typing to local context $Γ$ is written $wf_local Σ Γ$, and all the rules that are leaves (i.e., that do not mention typing in their premises) require the local context to be well formed. The rule are mostly standard in the context of the Calculus of Inductive Constructions or Martin-Löf Type Theory. As we did for cumulativity, we now explain them one by one. The complete definition can be found in the Appendix (Fig. 21).

```
type_Rel : ∀ n decl,
         wf_local Σ Γ → nth_error Γ n = Some decl →
         Σ; Γ ⊢ tRel n : lift₀ (S n) decl.(decl_type)

         type_Sort : ∀ s,
         wf_local Σ Γ → wf_universe Σ s →
         Σ; Γ ⊢ tSort s : tSort (super s)
```

The constructor `type_Rel` corresponds to the case of variables, it just amounts to recovering the type of the variable stored in the local context (when it is defined). `type_Sort` is the rule for typing universes. Here `super` is the function that takes a universe `l` and returns the smallest universe larger than `l`, and `wf_universe` is a function that checks that the levels appearing in `s` are defined in `Σ`.

```
type_Lambda : ∀ na B s1 B,
               type_App : ∀ t na A B s u,
               Σ; Γ ⊢ A : tSort s1 → Σ; Γ, na : A ⊢ t : B →
               Σ; Γ ⊢ tLambda na A t : tProd na A B
               Σ; Γ ⊢ tApp t u : B{0 := u}
```

`type_Lambda` is the introduction of dependent functions, it checks that `A` is a type and that `t` is a term of type `B` in the local context extended with the variable `na` of type `A`. `type_App` is the usual application rule. It makes use of substitution and in general, the typing rules use `substitution` (`B{0 := u}`) and `lifting` (`lift₀`) operations of de Bruijn indexes, whose definitions are standard.

```
type_LetIn : ∀ na b B t s1 A,
             type_Prod : ∀ na A B s1 s2,
             Σ; Γ ⊢ B : tSort s1 → Σ; Γ ⊢ b : B →
             Σ; Γ, na := b : B ⊢ t : A →
             Σ; Γ ⊢ tLetIn na b B t : tLetIn na b B A
             Σ; Γ ⊢ tProd na A B : tSort (sort_of_product s1 s2)
```

`type_LetIn` is the typing rule for let-binding, which is somehow a mix of `type_Lambda` and `type_App`. Note that the body `t` is typed in a context extended by a *definition* `na := b : B`, rather than a mere assumption, making it possible to use the value of that variable when typing `t`, as expressed by rule `cumul_rel` for cumulativity. In the typing rule `type_Prod` for products, `sort_of_product` is the maximum of the two levels (encoded as a non-empty set of levels) when $s_2$ is not `tProp` and `tProp` otherwise. This rule makes `tProp` impredicative, as it is possible to remain in `tProp` even when quantifying over an arbitrary type, including `tProp` itself.

```
type_Cumul : ∀ t A B s,
             type_Const : ∀ cst u d,
             Σ; Γ ⊢ t : A → Σ; Γ ⊢ B : tSort s →
             Σ; Γ ⊢ A ≤s B →
             Σ; Γ ⊢ t : B
             wf_local Σ Γ → declaredConstant Σ cst d →
             consistent_instance_ext Σ d.(cst_universes) u →
             Σ; Γ ⊢ tConst cst u : d.(cst_type)[u]
```

The Rule `type_Cumul` is the rule for cumulativity, which directly uses the definition of §2.3. Because cumulativity is untyped, we explicitly impose here that the target type `B` is a valid type. This is necessary to prove the *validity* theorem and we will later show in §4 that the two types are necessarily in the same universe hierarchy, i.e., that the sorts of `A` and `B` are related (both are `Prop` or both are `Type`). The Rule `type_Const` for typing a constant requires that it is declared in the global environment, and that the provided universe instance `u` respects the universe constraints `d.(cst_universe)` from that declaration.
name is a printing annotation. Sorts are represented with `tSort`, which takes a `universe` as argument. A universe can be either `lProp` or a more complex expression representing one of the `lType` universes. More details are given in §3.2.

The three constructors `tConst`, `tInd` and `tConstruct` represent references to constants declared in a global environment. The first is for definitions or axioms, the second for (co)inductive types or record types, and the last for constructors of inductive types. Because we handle universe polymorphism, those three constructors take a `universe_instance`, which is a list of `Level`.

The constructor `tCase` represents pattern matching, where `p` is the return predicate, `c` is an inhabitant of the inductive type corresponding to `indn` and `brs` is the list of branches corresponding to each possible constructor of the inductive type.

The constructor `tProj` represents primitive projections for records, the argument `p` contains the name of the record type and a natural number indicating which field of the record type is projected. The term `c` is the inhabitant of the record type that is projected.

The constructors `tFix` and `tCoFix` respectively represents (mutual) fixpoints and cofixpoints. A mutual (co)fixpoint is a list of (co)fixpoint definitions, each containing a type (given by the field `dtype`) and a body (given by the field `dbody`). The natural number `idx` corresponds to the term focused on in the mutual definition. In other words, if `mfix` mutually defines $f_1, \dots, f_n$, then `tFix mfix k` corresponds to $f_k$. This focusing is needed because in its absence we would have a list of terms with a list of types, rather than a single term with a single type.

In PCUIC, the meaning of a term is relative to a global environment which is constant throughout a typing derivation, and to a local context which may increase when going under binders.

The *local context* consists of a list of declarations written in *snoc* order: we use the notation $\Gamma$, $d$ for adding $d$ at the head of $\Gamma$. We write $x : A$ for a declaration without a body (as introduced by `tLambda`) and $x := t : A$ for a declaration with a body (as introduced by `tLetIn`). The *global environment* consists of three parts: a list of declarations, properly ordered according to dependencies, a global universe context representing the global constraints and possibly some additional local universe declarations used to type-check the body of a universe polymorphic declaration. A declaration is either the declaration of a constant (a definition or an axiom, depending on the presence or absence of a body) or of a block of mutual inductive types, which brings both the inductive types and their constructors to the context. We defer the presentation of the (co-)inductive type structure to §3.6.

## 3.2 Universes

The universe hierarchy is used in PCUIC to avoid the so-called “Type-in-Type” paradox of MLTT— originally due to Girard [1972] and later simplified by Hurkens [1995]—which is the type-theoretic counterpart of Russell’s paradox in set theory. The standard mathematical representation of the hierarchy is done by indexing occurrences of the universe *Type* with a natural number expressing its level in the hierarchy. In a practical setting, however, this presentation would be too rigid for a user. PCUIC therefore features monomorphic universes, which provide a way to refer to levels more abstractly with names, and polymorphic universes, which provide a way to quantify over those universes.

PCUIC features three kinds of level for a universe.

*Inductive Level : Set := lzero | level (s : string) | lvar (n : N).*

The constructor `lzero` refers to the smallest level, and corresponds to the encoding of the universe printed as `Set` in `Coq`. Constructor `level s` encodes a monomorphic universe with name `s` (i.e., traditional global universes, whose name is usually auto-generated by `Coq` when introducing an anonymous `Type`), while `lvar n` represents a polymorphic universe, where `n` is the de Bruijn *level* of the corresponding variable in the universe context.
type_Ind : ∀ ind u mdecl idecl,
wf_local Σ Γ → declared_inductive Σ ind mdecl idecl →
consistent_instance_ext Σ mdecl.(ind_universes) u →
Σ; Γ ⊢ tInd ind u : idecl.(ind_type)@[u]

type_Construct : ∀ ind i u mdecl idecl cdecl,
wf_local Σ Γ → declared__constructor Σ (ind, i) mdecl idecl cdecl →
consistent_instance_ext Σ mdecl.(ind_universes) u →
Σ; Γ ⊢ tConstruct ind i u : type__of__constructor mdecl cdecl (ind, i) u

Similarly, rules type_Ind and type_Construct check that the inductive type and constructor are
declared in the global environment, with a consistent universe instance. The rule to accept the
definition of a new constant or inductive type are given in the definition of a well-formed global
environment in § 2.6. Since the three typing rules type_Const, type_Ind, and type_Construct are
very similar, they could be unified with a single construction, as done for instance in Coq-Elpi [Tassi
2018].

type_Case : ∀ ci p c brs indices ps mdecl idecl,
let predctx := case predicate_context ci.(ci_ind) mdecl idecl p in
let ptm := it_mkLambda_or_LetIn predctx p.(preturn) in
declared__inductive Σ ci.(ci_ind) mdecl idecl →
Σ; Γ ++ predctx ⊢ p.(preturn) : tSort ps →
Σ; Γ ⊢ c : mkApps (tInd ci.(ci_ind) p.(puinst)) (p.(pparams) ++ indices) →
case__side__conditions Σ Γ ci p ps mdecl idecl indices predctx →
case__branch__typing Σ Γ ci p ps mdecl idecl ptm brs →
Σ; Γ ⊢ tCase ci p c brs : mkApps ptm (indices ++ [c])

The Rule type_Case represents typing of pattern matching. It basically asks for the scrutinee c, the
return type p.(preturn) and each branch to be well typed, and for the inductive type of the scrutinee
to be declared; but there are also side conditions imposed by the predicate case__side__conditions.
The two main parts are that the universe instance must be consistent and that the elimination must
be allowed (in the case of Prop, elimination is restricted to subsingleton elimination, see §2.6.3).
Case analysis is forbidden for coinductive types because it is known to break subject reduction (see
§ 4.4).

type_Proj : ∀ p c u mdecl idecl cdecl pdecl args,
declared__projection Σ p mdecl idecl cdecl pdecl → #|args| = ind_npars mdecl →
Σ; Γ ⊢ c : mkApps (tInd (fst (fst p))) u args →
Σ; Γ ⊢ tProj p c : subst₀ (c :: List.rev args) (snd pdecl)@[u]

Rule type_Proj is the typing rule for projection of record types (which are described using the
constructor tInd as for (co-)inductive types). It checks that p is a well-declared projection of the
record fst (fst p). If this is the case, the projection's type is snd pdecl substituted by the list of
arguments c :: List.rev args (as defined by the operation subst₀).

... mfix n decl,

wf_local Σ Γ → fix guard Σ Γ mfix → nth_error mfix n = Some decl →
wf fix Σ mfix → All (fun d ⇒ {s & Σ; Γ ⊢ d.(dtype) : tSort s}) mfix →
All (fun d ⇒ Σ; Γ ++ fix_context mfix ⊢ d.(dbody) : lift₀ #|fix_context mfix| d.(dtype)) mfix →
Σ; Γ ⊢ tFix mfix n : decl.(dtype)

type_Fix : ∀ mfix n decl,
wf_local Σ Γ → fix guard Σ Γ mfix → nth_error mfix n = Some decl →
wf fix Σ mfix → All (fun d ⇒ {s & Σ; Γ ⊢ d.(dtype) : tSort s}) mfix →
All (fun d ⇒ Σ; Γ ++ fix_context mfix ⊢ d.(dbody) : lift₀ #|fix_context mfix| d.(dtype)) mfix →
Σ; Γ ⊢ tFix mfix n : decl.(dtype)

type_CoFix : ∀ mfix n decl,
Inductive ConstraintType : Set := Le (z : Z ) | Eq.

Definition UnivConstraint : Set := Level * ConstraintType * Level.

Record valuation := { valuation_mono : string → positive; valuation_pol y : N → N }.

Definition val (v : valuation) (l : Level) : Z ::= match l with | lzero ⇒ 0 | level s ⇒ Z pos (v.(valuation_mono) s) | lvar x ⇒ Z .of$_{N}$ (v.(valuation_pol y) x) end.

<caption>Fig. 2. Definition of constraints and valuations</caption>

Definition UnivExpr := Level × N .
Inductive universe := lProp | lType (ls : nonEmptyUnivExprSet).

Then, a UnivExpr is a pair (1,n) of a level 1 and a natural number n, meaning intuitively that we
are talking about the universe 1+n. Finally, a universe is either lProp or lType ls, where ls is a
non-empty set of UnivExpr. The non-empty set ls of UnivExpr is interpreted as an encoding for
the maximum of its elements, representing so-called “algebraic” universes. For instance, the term
tSort (lType { (u,0) ; (v,1) }) encodes the universe that is usually written Type max(u,v+1) in the literature.
In the remainder, we write tProp for the term tSort lProp.

Constraints and Valuations. To allow for a flexible and modular account of universes, Coq
implements typical ambiguity and universe polymorphism. The universe hierarchy is hence not
fixed but rather maintained using an extensible ("elastic", as coined by its original designer Gérard
Huet [1988]) set of universe levels and associated constraints (UnivConstraint) which say that a
level, incremented by z is smaller than or equal to another (Le z) or equal (Eq) to another level,
as described in Fig. 2. Universe polymorphism [Harper and Pollack 1991; Sozeau and Tabareau
2014] further adds the possibility to make definitions and inductive types polymorphic in the set
of universe levels and constraints, so that they can be reused at different levels. This is akin to
bounded prenex polymorphism à la ML. In the Coq type checker, consistency of the universe
hierarchy is checked using an acyclicity criterion on the graph induced by the constraints. However,
this characterization of consistency is quite far from the mathematical model, which says that
universe levels are natural numbers. To keep the specification as close as possible to the meta-theory,
we therefore introduce the notion of valuation on universe levels, which associates 0 to lzero,
a positive number to monomorphic universes (a monomorphic universe cannot be lzero) and a
natural number to polymorphic universes.

Then a valuation satisfies a set of constraints when each constraint is individually satisfied
(satisfies₀):

Inductive satisfies₀ (v : valuation) : UnivConstraint → Prop :=
| satisfies₀_Le (l l' : Level) (z : Z) : val v l ≤ val v l' - z → satisfies₀ v (l, Le z, l')
| satisfies₀_Eq (l l' : Level) : val v l = val v l' → satisfies₀ v (l, Eq, l').

Definition satisfies v : UnivConstraintSet → Prop := For_all (satisfies₀ v).

The universe hierarchy is consistent when there exists a valuation which satisfies its set of
constraints:
wf_local Σ Γ → cofix-guard Σ Γ mfix → nth_error mfix n = Some decl →
wf_cofix Σ mfix → All (fun d ⇒ {s & Σ ; Γ ⊢ d.(dtype) : tSort s}) mfix →
All (fun d ⇒ Σ ; Γ ++ fix_context mfix ⊢ d.(dbody) : lift₀ #|fix_context mfix| d.(dtype)) mfix →
Σ ; Γ ⊢ tCoFix mfix n : decl.(dtype)

Finally, Rules type_Fix and type_CoFix are the typing rules for mutual fixpoints and cofixpoints.
The typing hypotheses are similar, and enforce for each of the mutually defined (co)fixpoints that
its type dtype is a valid type, in the sense that it has a sort, and that its body dbody has type dtype
in the local context extended by the fixpoint definition (so as to allow for recursive calls). What
sets these rules apart are the guard conditions fix-guard and cofix-guard, which remain abstract
as explained in §2.4, and the well-formedness conditions wf-fix and wf-cofix. These mainly check
that the type of the recursive argument of a fixpoint is an inductive type, and that the codomain of
a cofixpoint is a coinductive type.

In the Coq development, the typing relation is parametrized by a record of flags. The flags are
also used in the verified type-checking algorithm we explain later, and the type is thus called
checker_flags. We show it here with comments to explain what every flag stands for:

Class checker_flags := {
  (* default true, setting to false adds the (inconsistent) Type : Type rule *)
  check_univ : B;
  (* default true, false for extraction, enables Prop <: Type *)
  prop_sub_type : B;
  (* default false, lets indices matter for the type universe of an inductive *)
  indices_matter : B;
  (* default true, allows constructor types to contain lets *)
  lets_in_constructor_types : B.
}

## 2.6 Well-Formed Environments

The definition of the typing judgment is relative to a global environment that contains the global constants and inductive definitions. For typing to be well behaved, this global environment must be well formed. Beyond enforcing that all definitions are well typed, this well-formation condition also contains constraints about universes and cumulativity, and in the case of inductive types, allowed eliminations of its inhabitants, and the (strict) positivity criterion.

More precisely, an environment is represented as a record of a global universe context (a set of levels and a set of universe constraints) and an association list of (unique) kernel names to constant or inductive declarations.

Inductive global decl :=
  | ConstantDecl : constant_body → global decl
  | InductiveDecl : mutual_inductive_body → global decl.

Definition global_declarations := list (kername * global decl).

Record global_env :=
  { universes : LevelSet * UnivConstraintSet; declarations : global_declarations }.

Note that this is the specification of a global environment, but Coq's algorithm uses a more efficient
representation. In §5, we describe a type checker that is abstract with respect to a particular choice
of representation, as long as it is equivalent to the specification.
**Definition consistent ctrs** := $\exists v$, satisfies $v$ ctrs.

Note that this definition of consistency is not a priori decidable, and this is the point of §4.1 to provide an alternative specification using acyclicity of a graph, which is a checkable property.

*Cumulativity on universes.* The notion of subtyping on types is defined as definitional equality up to cumulativity on universes, which states that $tSort 1$ is a subtype of $tSort 1'$ as soon as $1$ is smaller than $1'$. Comparison of universes depends on the set of constraints under consideration. Indeed, a universe $u$ is smaller than a universe $u'$ for a given set of constraints $\varphi$ when for any valuation which satisfies $\varphi$, the value of $u$ is smaller than the value of $u'$. Formally, it is defined as follows:

**Definition leq_universe** ($\varphi$ : UnivConstraintSet) $u$ $u'$ :=
$\forall v : valuation$, satisfies $v$ $\varphi \to (\mathbf{val} \ v \ u \le \mathbf{val} \ v \ u')$.

Similarly, `eq_universe` defines when two universes are equal. The notion of comparison is extended to `tProp` by stating that it is smaller than any other universe if the flag governing the `Prop` $\le$ `Type` rule is set, and incomparable otherwise. We will see in §5 and 7 that correctness of erasure holds only in a theory without this rule.

Finally, the function `global_ext_constraints` collects the universe constraints appearing in a global environment $\Sigma$.

## 3.3 Cumulativity

Conversion is one of the key ingredient for the definition of dependent type theories. It implements a syntactic notion of equality that can be used during typing to use a term of type A when a term of type B was expected, under the condition that A and B are convertible. In the case of `COQ` and of `PCUIC`, this notion of conversion is untyped, i.e., it relates terms without making use of the types of those terms, in contrast with the typed definitional equality judgment which is customary in Martin-Löf Type Theory [Martin-Löf 1984]. Moreover, conversion further refines to a notion of cumulativity that extends it with a subtyping rule: `Typei` is a subtype of `Typej` when $i \le j$ in the hierarchy, as described in §3.2.

The specification of cumulativity between two terms $t$ and $u$, written $\Sigma; \Gamma \vdash t \preceq_s^{Rle} u$, is relative to a global context $\Sigma$ and a local context $\Gamma$ and is parametrized by a relation $\mathbf{Rle}$ between universes. We use the $s$ subscript (for specification) to distinguish it later on from the algorithmic presentation of cumulativity, written $\Sigma; \Gamma \vdash t \preceq_a^{Rle} u$. When $\mathbf{Rle}$ is instantiated with `leq_universe` (`global_ext_constraints` $\Sigma$), this gives rise to the notion of cumulativity (written $\preceq_s$), and when it is instantiated with `Re` := `eq_universe` (`global_ext_constraints` $\Sigma$), it boils down to conversion (written $\approx_s$).

The complete definition has 24 rules which can be found in the Appendix (Figs. 19 and 20). To avoid clutter, we prefer to describe the rules grouped by their purpose, dealing with ordering, cumulativity, computation or congruence. Note also that in the definition of Figs. 19 and 20, we take the liberty of directly using the notation in the header, which is possible in systems such as `AGDA`, but not in `COQ`. We believe this makes the definition easier to read and avoids the need to introduce an auxiliary useless name. We will do so for several inductive definitions in this paper.

### 3.3.1 Ordering Rules.
There are three rules to enforce the specification of cumulativity to be a pre-order and conversion to be an equivalence relation.

$\mathbf{cumul\_Refl}: \forall t,$
$\Sigma; \Gamma \vdash t \preceq_s^{Rle} t$

$\mathbf{cumul\_Sym}: \forall t u,$
$\Sigma; \Gamma \vdash t \approx_s u \to$
$\Sigma; \Gamma \vdash u \preceq_s^{Rle} t$

$\mathbf{cumul\_Trans}: \forall t u v,$
$\mathbf{is\_closed\_context} \Gamma \to \mathbf{is\_open\_term} \Gamma u \to$
$\Sigma; \Gamma \vdash t \preceq_s^{Rle} u \to \Sigma; \Gamma \vdash u \preceq_s^{Rle} v \to \Sigma; \Gamma \vdash t \preceq_s^{Rle} v$
Constant declarations (`constant_body`) record the type (`cst_type`) and optional body (`cst_body`) of said constant, and a universe declaration (`cst_universes`). The presence or absence of a body discriminates between a `Definition` and an `Axiom`.

Record constant_body := {
  cst_type : term;
  cst_body : option term;
  cst_universes : universes Decl }.

The universe declaration is either monomorphic or polymorphic:

Inductive universes Decl : Type :=
| Monomorphic_ctx
| Polymorphic_ctx (cst : list name * UnivConstraintSet).

Monomorphic declarations do not introduce universes or constraints, they instead rely on those already declared in the global universe context. Polymorphic definitions come with an abstract universe context: a list of variables and constraints on them that are instantiated at each use of a polymorphic construction.

Inductive types have more structure. In full generality, they are represented as a mutual inductive block. Actually, the same representation is used to encode inductive, co-inductive or record types (with potentially primitive projections). This common representation allows us to factorize the many similarities in the specification of those types.

Record mutual_inductive_body := {
  ind_finite : recursivity kind; ind_npars : N; ind_params : context;
  ind_universes : universes Decl; ind_variance : option (list Variance);
  ind_bodies : list one_inductive_body }.

Mutual inductive blocks have a recursivity kind annotation to distinguish between inductive, co-inductive and non-recursive types—as introduced with the `Variant` keyword in CoQ. Note in particular that it is not possible to mix inductive and co-inductive definitions in the same mutual inductive block. All inductive types in a block share a context of parameters `ind_params`, whose number of assumptions is recorded in `ind_npars`, a universe declaration and an optional universe variance annotation (discussed in §2.6.2). Finally, there is a (non-empty) list of inductive bodies representing each (co-)inductive type in the mutual block:

Record one_inductive_body := {
  ind_name : ident; ind_indexes : context; ind_sort : Universe; ind_type : term;
  ind_kelim : allowedEliminations;
  ind_actors : list constructor_body; ind_projs : list projection_body }.

Each inductive type has a name `ind_name` and an arity `ind_type` which should decompose into a dependent product starting with the shared parameters, the indices `ind_indexes` and a sort `ind_sort` as conclusion.<fnref n="11" /> The allowed elimination sorts of its inhabitants is described by the `ind_kelim` parameter (see §2.6.3 for a detailed explanation). The (possibly empty) list `ind_actors` records for each constructor their name, context of arguments, and the indices at which they instantiate the conclusion’s inductive type (the parameters are fixed for a whole mutual family). Finally, the projections (for primitive records) record the name and type of each projection.

Record constructor_body := { cstr_name : ident; cstr_args : context; cstr_indexes : list term }.

<footnote n="11">¹¹Arities are the subset of n-ary dependent products and let-ins whose final codomain is a sort</footnote>
Rules `cumul_Trans` and `cumul_Reflect` state that cumulativity is transitive and reflexive, and Rule `cumul_Sym` states that only conversion is symmetric. Note that the Rule `cumul_Sym` can also be used to show that conversion is included in cumulativity (by using the rule twice).

We would like to mention a technical difficulty here, in presence of untyped cumulativity and conversion. The transitivity rule needs to be restricted to introduce only a term `u` whose free variables appear in a closed context `Γ`, as ensured by the `is_closed_context` `Γ` and `is_open_term` `Γ` `u` conditions. This is necessary to maintain the invariant that a proof of conversion between two well-scoped terms only involves well-scoped terms. This invariant is important because reduction of non-well-scoped terms is not confluent (this is explained in §5.3.1) and thus the correspondence with algorithmic conversion (see §4.2.2) only works on well-scoped terms.

### 3.3.2 Cumulativity Rules.
There are three rules dealing with cumulativity of both universes and inductive types.

$$ \mathit{cumul\_Ind} : \forall i u' \text{ args args}', $$

$$ \mathit{R_global_instance} \Sigma \mathit{Re} \mathit{Rle} (\mathit{IndRef} i) \#|\text{args}| u u' \to $$

$$ \mathit{All2} (\mathit{fun} t u \Rightarrow \Sigma; \Gamma \vdash t \preceq_s^{\mathit{Re}} u) \text{args args}' \to $$

$$ \Sigma; \Gamma \vdash \mathit{mkApps} (\mathit{tInd} i u) \text{args} \preceq_s^{\mathit{Rle}} \mathit{mkApps} (\mathit{tInd} i u') \text{args}' $$

$$ \mathit{cumul\_Sort} : \forall s s', $$

$$ \mathit{Rle} s s' \to $$

$$ \Sigma; \Gamma \vdash \mathit{tSort} s \preceq_s^{\mathit{Rle}} \mathit{tSort} s' $$

$$ \mathit{cumul\_Construct} : \forall i k u u' \text{ args args}', $$

$$ \mathit{R_global_instance} \Sigma \mathit{Re} \mathit{Rle} (\mathit{ConstructRef} i k) \#|\text{args}| u u' \to $$

$$ \mathit{All2} (\mathit{fun} t u \Rightarrow \Sigma; \Gamma \vdash t \preceq_s^{\mathit{Re}} u) \text{args args}' \to $$

$$ \Sigma; \Gamma \vdash \mathit{mkApps} (\mathit{tConstruct} i k u) \text{args} \preceq_s^{\mathit{Rle}} \mathit{mkApps} (\mathit{tConstruct} i k u') \text{args}' $$

Rule `cumul_Sort` is the direct expression of the subtyping rule on universes, while Rules `cumul_Ind` and `cumulConstruct` deal with cumulativity for inductive types. Following Timany and Sozeau [2017], `cumul_Ind` states that two *fully applied* inductive types are in the cumulativity relation when their arguments are convertible,<fnref n="10" /> and when their universe levels are related according to the variance of `tInd` `i` `u` registered in the global environment `Σ`. The relation on the universe arguments according to the declared variance is verified by the `R_global_instance` predicate. Rule `cumulConstruct` ensures similarly that the two *fully applied* constructors live in inductive types which are in the cumulativity relation. We will explain cumulativity of inductives types in more detail in §3.6.2.

### 3.3.3 Computation Rules.
There are 9 rules representing computation in PCUIC of various kinds (functions, pattern-matching, (co)fixpoints, definitions, projections).

$$ \mathit{cumul\_beta} : \forall \text{na t b a}, $$

$$ \Sigma; \Gamma \vdash \mathit{tApp} (\mathit{tLambda} \text{ na t b}) a \preceq_s^{\mathit{Rle}} b \{0 := a\} $$

$$ \mathit{cumul\_zeta} : \forall \text{na b t b'}, $$

$$ \Sigma; \Gamma \vdash \mathit{tLetIn} \text{ na b t b'} \preceq_s^{\mathit{Rle}} b' \{0 := b\} $$

Rule `cumul beta` encodes usual computation of function application and `cumul zeta` is the standard (call-by-name) reduction of a let-binding construct. They make use of substitution `b{0 := a}` which is a shorthand for the use of the capture-avoiding de Bruijn instantiation function.

$$ \mathit{cumul\_rel} : \forall i \text{ body}, $$

$$ \text{option\_map} \text{ decl\_body} (\text{nth\_error} \Gamma i) = \text{Some} (\text{Some body}) \to $$

$$ \Sigma; \Gamma \vdash \mathit{tRel} i \preceq_s^{\mathit{Rle}} \mathit{lift}_0 (S i) \text{ body} $$

Rule `cumul rel` deals with variables in the local context that have a body, corresponding to definitions as introduced by `tLetIn`. The body is lifted to be well scoped in `Γ`. We use the auxiliary

<footnote n="10">¹⁰This condition on the list of arguments is ensured using the `All2` predicate which requires that the elements of the list are pointwise related, here by conversion.</footnote>
Record projection_body := { proj_name : ident; proj_type : term }.

Altogether, this data forms the raw structure of global environments of PCUIC. Well-formed global environments impose strict restrictions on this data.

• First, all names should be globally unique.<fnref n="12" />

• For constants, the declared type should be typeable by a sort and the optional constant body should be typeable using the declared type, in the universe context associated with `cst_universes`.

• For inductive blocks, the inductive types, constructors and projections should all be well typed, but this is not enough: various extra properties are imposed on these blocks. We will describe them in the remainder of this section.

2.6.1 Positivity criterion. Allowing arbitrary recursive types breaks strong normalization, as the untyped $\lambda$-calculus can easily be expressed using such arbitrary recursive types. Hence, CoQ restricts the class of definable inductive types to strictly-positive ones. Coarsely, strict positivity ensures that one can always derive a meaningful elimination rule with induction hypotheses for each recursive argument of each constructor [Coquand and Paulin 1990].

We formalize the strict positivity condition as a predicate on the shapes of constructors of an inductive declaration (Fig. 3). It relies on an auxiliary predicate that checks positivity of each type argument of a constructor. A constructor argument ty is positive with respect to a mutual inductive declaration $m$ in context $\Gamma$, written $m; \Gamma \vdash_+^{arg} ty$, when its weak $\zeta$-normal form (meaning let-in are reduced away) either:

• does not mention the inductive block, or

• is of shape `mkApps` (`tRel k`) 1 where $k$ refers to an inductive in the block (checked using `mdecl_at_i`) and 1 does not refer to the inductive block, or

• is of shape `tProd na ty ty'` where `ty` does not mention the inductive block and `ty'` is induc- tively positive in the context extended with `na : ty`.

The context $\Gamma$ tracks the parameters and arguments of the constructor, while de Bruijn references above `#|\Gamma|` represent the inductive types in the block.

Then, a constructor type `ty` is strictly positive, written $m@i; \Gamma \vdash_+ ty$, with respect to a mutual inductive declaration $m$ and inductive $i$ in this block in context $\Gamma$ when its weak $\zeta$-normal form is of shape `tProd na_1 ty_1` (`tProd na_2 ty_2` (`tProd ... concl`)) where moreover:

• all the arguments in `ty_i` are positive; and

• the conclusion `concl` is of shape `mkApps` (`tRel k`) `args` where $k$ refers to the current inductive $i$ and `args` do not mention any of the inductive types in the block.

We (weakly) $\zeta$-normalize types (as CoQ does), so this definition allows *unused* let-bindings to mention the inductive type, potentially in a non-strictly positive way. It is however clear that the same inductive type without the unused let-bindings is equivalent for all purposes.

This definition is a simplification of the actual criterion of CoQ which additionally handles *nested* inductive types [Abbott et al. 2004], i.e., inductive types where a constructor can take as argument another inductive type applied to one of the mutually defined ones. A typical example is that of rose trees: a tree where the single node constructor takes a *list* of subtrees.

2.6.2 Cumulative Inductive Types. CoQ additionally features cumulative inductive types, which extends the cumulativity relation through polymorphic inductive families. Intuitively, this allows “smaller” instances of an inductive family to be used where a larger one is expected. A typical

<footnote n="12">¹²Technically in CoQ, there is a notion of namespace to be able to use the same name in different modules or files, so globally is to be understood up to name space.</footnote>
definitions nth_error for optional lookup in a list (returning None if the index is out of bounds), and
the standard polymorphic option_map which maps a function under an option type.

cumul_iota: ∀ ci c u args p brs br,
nth_error brs c = Some br → #|args| = (ci.(ci_npar) + context_assumptions br.(bcontext)) →
Σ; Γ ⊢ tCase ci p (mkApps (tConstruct ci.(ci_ind) c u) args) brs ≤< Rle s iota_red ci p args br

Rule cumul_iota corresponds to computation of pattern-matching, by selecting the appropriate branch and ensuring that the constructor is fully applied, using the context_assumptions function to count only the non-let assumptions in the branches' context, which actually bind arguments. The function iota_red computes the right substitution of the selected branch br.

cumul擎: ∀ mfix idx args narg fn,
    unfold擎 mfix idx = Some (narg, fn) → is_constructor narg args = true →
    Σ; Γ ⊢ mkApps (tFix mfix idx) args ≤< Rle mkApps fn args

Rule cumul擎 corresponds to fixpoint unfolding when the fixpoint is applied to a constructor (using is_constructor) in its principal argument position narg computed by unfold擎, which selects the recursive function among the mutually recursive block mfix. This restriction ensures that fixpoints cannot be unfolded forever, so as to preserve termination.

cumul_cofix_case : ∀ ip p mfix idx args narg fn brs,
    unfold_cofix mfix idx = Some (narg, fn) →
    Σ; Γ ⊢ tCase ip p (mkApps (tCoFix mfix idx) args) brs ≤< Rle s tCase ip p (mkApps fn args) brs

cumul_cofixproj : ∀ p mfix idx args narg fn,
    unfold_cofix mfix idx = Some (narg, fn) →
    Σ; Γ ⊢ tProj p (mkApps (tCoFix mfix idx) args) ≤< Rle s tProj p (mkApps fn args)

Dually, Rules cumul_cofix_case and cumul_cofix proj describe how cofixpoints can also be un-
folded when forced by a pattern-matching or projection, that is when they are the scrutinee of
tCase or tProj.

cumul_delta : ∀ c decl body (isdecl : declaredConstant Σ c decl) u,
    decl.(cst_body) = Some body →
    Σ; Γ ⊢ tConst c u ≤< Rle s body@[u]

Rule cumul_delta represents constant unfolding from the global environment Σ. In case the defini-
tion is universe polymorphic, its universes are instantiated, which is written body@[u].

cumulproj : ∀ i pars narg args u arg,
nth_error args (pars + narg) = Some arg →
Σ; Γ ⊢ tProj (i, pars, narg) (mkApps (tConstruct i 0 u) args) ≤< Rle arg

Finally, Rule cumulproj describes projection of record types, relating the projection of the constructor of a record to the corresponding field.

3.3.4 Congruence Rules. The last set of rules deals with congruence closure of the cumulativity relation. There is one rule per term constructor of PCUIC, which basically amounts to checking recursively that the arguments are in the cumulativity relation. There is a minor subtlety however, because cumulativity of PCUIC is only equivariant on the left-hand side of an arrow,<fnref n="11" /> which means

<footnote n="11">¹¹This restriction comes from the fact that it is difficult to model contravariant cumulativity in set-theoretic models [Timany and Sozeau 2018]. Whether cumulativity could be contravariant on the left-hand side of an arrow or not is still the subject of ongoing theoretical investigations.</footnote>
Inductive _:_Γ⁺arg_ (m: mutual_inductive_body) (Γ:context) : term → Type :=
| pos_arg_closed ty : closedn #Γ| ty → m ; Γ ↣⁺arg ty
| pos_arg_concl l k i : #l| = ind_realargs i → All (closedn #Γ|) l →
  mdecl_at_i m i Γ k → m ; Γ ↣⁺arg mkApps (tRel k) l
| pos_arg_let na b ty ty' : m ; Γ ↣⁺arg ty' {0 := b} → m ; Γ ↣⁺arg tLetIn na b ty ty'
| pos_arg_ass na ty ty' : closedn #Γ| ty → m ; na : ty ::= Γ ↣⁺arg ty' → m ; Γ ↣⁺arg tProd na ty ty'.

Inductive _@_;Γ+_ (m: mutual_inductive_body) (i:N) (Γ:context) : term → Type :=
| pos_let na b ty ty' : m @ i ; Γ ↣_+ ty' {0 := b} → m @ i ; Γ ↣_+ tLetIn na b ty ty'
| pos_ass na ty ty' : m ; Γ ↣⁺arg ty → m @ i ; na : ty ::= Γ ↣_+ ty' → m @ i ; Γ ↣_+ tProd na ty ty'
| pos_concl l : All (closedn #Γ|) l → m @ i ; Γ ↣_+ mkApps (tRel (#m.(ind_bodies)| - S i + #Γ|)) l.

<caption>Fig. 3. Positivity judgment</caption>

example is given by the type of lists: an object of type `list@{Set} N` can be used anywhere a `list@{i} N` is expected, without introducing an explicit coercion. Another useful intuition is that such a subtyping is justified because we could automatically introduce identity coercions in such places, which do not change the computational content of the objects, but only their universe annotations.

In the original presentation [Timany and Sozeau 2018], inductive types do not have parameters and the cumulativity relation is extended by a general judgement asserting that two inductive families I and I' are in the cumulativity relation when:

* they have the same number of constructors

* for each pair of types of corresponding constructors `ty` and `ty'`, each constructor argument type pairs are in the cumulativity relation, assuming $I \le I'$ inductively.

For two universe instantiations of the polymorphic `list@{i}` datatype on carrier type `A`, e.g., corresponding to types `list@{k}` `A` and `list@{l}` `A` in the theory with parameters, this requires to consider only the `cons_A`: `A` → `list@{i}` `A` → `list@{i}` `A` case and check that `A` ≤ `A` and `list@{k}` `A` ≤ `list@{l}` `A`. The first one holds by reflexivity while the second one is our induction hypothesis. In this case we can see that actually no particular relationship should hold on the universe levels `l` and `k`, meaning that all `list@{\{\}}` `A` types are convertible.

More interestingly, inductive families that actually embed universes lift to the cumulativity relation. In particular all types-with-structure records fall into this subset. Suppose we define the type of monoids as a record:

Record monoid@{u} := { carrier : Type@{u} ; unit : carrier ; op : carrier → carrier → carrier }

In that case, the universe `u` is used *covariantly* in the inductive definition, and cumulativity enables the use of a monoid@{Set} (e.g., natural numbers with addition) where a monoid at any higher type is expected. More generally monoid@{i} ≤ monoid@{j} whenever $i \le j$. In general, we can let `Coq` infer the variance of universes for cumulative inductive types (it is then printed using the `About` or `Print` commands), but there is also surface syntax to specify it. The inference performs a cumulativity test between two instances of the inductive type and gathers the necessary constraints for the first to be a subtype of the other, marking universe variables as irrelevant, covariant or invariant. As we are extending the `Type` cumulativity relation which is not contravariant on function domains, there is also no contravariant status here.

**Variance.** The notion of variance was introduced in `Coq` together with polymorphic cumulative inductive types to describe the status of each universe variable of an inductive declaration with a
that in the following rule for products, while `b` and `b'` are recursively compared for cumulativity, `a` and `a'` are only compared for conversion.

```
cumul_Prod : ∀ na' a a' b b',
  eq_binder_annot na na' →
  Σ ; Γ ⊢ a ≲<sup>Re</sup> a' →
  Σ ; Γ , na : a ⊢ b ≲<sup>Rle</sup> b' →
  Σ ; Γ ⊢ tProd na a b ≲<sup>Rle</sup> tProd na' a' b'
```

The complete set of congruence rules can be found in Fig. 20.

## 3.4 Dealing with the Guard Condition

Before giving the specification of typing, we need to introduce two guard conditions that determine when recursive and corecursive definitions are valid. Those conditions are used in the typing rules of fixpoints and cofixpoints, ensuring strong normalization of PCUIC. We defer the discussion on strong normalization to § 5.5, but we can already say that strong normalization is treated as an axiom in our framework that depends on the notion of guard condition.

To make apparent that the guard conditions for fixpoints and cofixpoints share many properties, we parametrize the definition of the guard condition by the two-valued type `FixCoFix`, thus having only one predicate, dealing with fixpoints when the value is `Fix`, and cofixpoints otherwise. We thus postulate (in PCUIC: *Typing*) the existence of a guard condition checker as follows:

```
Inductive FixOrCoFix : Type := Fix | CoFix.
```

```
Axiom guard : FixOrCoFix → global_env_ext → context → mfixpoint term → Prop.
```

```
Definition fix guard := guard Fix.
```

```
Definition cofix guard := guard CoFix.
```

This presentation has two main advantages. First, it makes it clear that our meta-theoretic study of reduction and typing (§ 5), and in particular our proof of subject reduction, does not depend on a particular guard condition. Rather, it only relies on a few stability properties (e.g., stability by reduction or substitution). These conditions are listed in PCUIC: *GuardCondition*, and § 5.2.2 describes in more details the axiom of stability under reduction and substitution. Second, it makes explicit that while we need the guard condition to imply strong normalization in order to implement a terminating type checker, this normalization axiom is not necessary for most of the meta-theoretic development, and it indeed appears very late in the formalization. As we cannot prove strong normalization anyway due to Gödel's incompleteness theorem, we believe that our axiomatic presentation makes more sense as it sheds light on the exact syntactic properties that must be satisfied by any guard condition on (co)fixpoints.

In Coq, the guard condition for fixpoints that is implemented is based on recursive calls which must be done on strict sub-terms.<fnref n="12" /> We do not enter into those details in this section, and they are not useful for the definition of typing; all that matters is that the typing rules of fixpoints and cofixpoints make use of this guard condition.

## 3.5 Definition of Typing

The typing rules of PCUIC are defined as an inductive family, written $Σ ; Γ ⊢ t : T$, where $Σ$ is a global environment, $Γ$ is a local context and $t$ and $T$ are terms. The pointwise extension of typing to local context $Γ$ is written $wf_local Σ Γ$, and all the rules that are leaves (i.e., that do not mention typing in their premises) require the local context to be well formed. The rules are mostly standard in the context of the Calculus of Inductive Constructions or Martin-Löf Type Theory. As we did

<footnote n="12">¹²Actually the condition is slightly more general, but this is beyond the scope of this paper.</footnote>
variance annotation that specifies how the universe variable behaves with respect to cumulativity, as exemplified above with list and monoid. However, variance has never been considered before from a formal point of view, and our work is the first place where this notion is formalized, and crucially so: we need specific properties of cumulative inductive types to complete the subject reduction proof (§4.4). The specification of cumulative inductive types ensures that the declared variances of a cumulative inductive type give rise to the expected subtyping relations between the types of inductives and each constructor. Variance is defined as a simple enumeration:

Inductive Variance.t := Irrelevant | Covariant | Invariant.

A variance annotation is simply a list of variances, one for each bound universe in a polymorphic definition.

In the remainder of this section, we consider a fixed cumulative inductive definition. From a variance annotation, along with the polymorphic universe context of the definition, we can generate a new context univs consisting of two copies of the polymorphic universe context instantiated at universe levels u and v (variance_universes), in addition to constraints witnessing the variance relationship between u and v, i.e., no relationship for irrelevant universes, equality for invariant ones and inequality for covariant ones. This context is proven to be consistent, starting from a consistent inductive universe context.

From this data, we specify when the cumulative inductive type under consideration respects the variance annotations using two conditions.

**Inductive types.** Recall that the cumulative inductive type declaration is composed of a context of parameters, a context of indices and a conclusion sort. We write $\Gamma_{\text{param}}$ (resp. $\Gamma_{\text{ind}}$) for the context of parameters (resp. indices) where let-bindings have been expanded. The first condition expresses that $\Gamma_{\text{ind}}$ instantiated at u is in the cumulativity relation with $\Gamma_{\text{ind}}$ instantiated at v, under the context of parameters at the “lower” instance of the universes, and that the constraints in univs are sufficient to derive this.

$\Sigma, \text{univs} ; \Gamma_{\text{param}}@[u] \vdash \Gamma_{\text{ind}}@[u] \leq_s \Gamma_{\text{ind}}@[v]$.

We consider contexts where let-bindings have been expanded to avoid potentially useless constraints on let-bound variables. There is only one parameter context involved: it models the fact that cumulativity of inductive types in CoQ only allows to subsume one instance of an inductive type by another when they share convertible parameters, as explained above. The only sensible choice here is to use the “lower” universe instance for the parameters here as the indices at levels u might not be typeable if parameters are at a higher level v, but the converse holds (this is proven in PCUIC: InductiveInversion).

**Constructor types.** Following the intuition that cumulative inductive types simply extend the usual Type cumulativity, the judgment for constructors ensures that, for each constructor declaration cs, the two (let-expanded) argument contexts (written $\Gamma_{\text{args}}$) are in the cumulativity relation pointwise.

$\Sigma, \text{univs} ; \Gamma_{\text{ar}} \quad \text{++} \quad \Gamma_{\text{param}}@[u] \vdash \Gamma_{\text{args}}@[u] \leq_s \Gamma_{\text{args}}@[v]$.

Note that due to the encoding of constructors where recursive references to the current inductive block are modeled using de Bruijn indices, we also put the arities ($\Gamma_{\text{ar}}$) in the local context, along with the parameters. Of course, this also models that $I@{\{u\}} \leq I@{\{v\}}$ is assumed when checking the cumulativity, as both constructors will have the same variable in place of references to the inductive type.

Finally, we must also check that the specific list of indices indices for each pair of constructors stay in the convertibility relation rather than cumulativity, otherwise this would lead to unsoundness (Timany and Sozeau [2018] give more details).
for cumulativity, we now explain them one by one. The complete definition can be found in the Appendix (Fig. 21).

```
type_Rel : ∀ n decl,
         wf_local Σ Γ → nth_error Γ n = Some decl →
         Σ ; Γ ⊢ tRel n : lift₀ (S n) decl.(decl_type)
```

The constructor `type_Rel` corresponds to the case of variables, it just amounts to recovering the type of the variable stored in the local context (when it is defined). The rule `type_Sort` is the introduction rule for universes. Here `super` is the function that takes a universe 1 and returns the smallest universe larger than 1, and `wf_universe` is a function that checks that the levels appearing in `s` are defined in `Σ`.

```
type_Lambda : ∀ na t s1 B,
               Σ ; Γ ⊢ A : tSort s1 → Σ ; Γ , na : A ⊢ t : B →
               Σ ; Γ ⊢ tLambda na A t : tProd na A B
```

The `type_Lambda` rule introduces dependent functions. It checks that `A` is a type and that `t` is a term of type `B` in the local context extended with the variable `na` of type `A`. The application rule `type_App` is as usual. It makes use of substitution and in general, the typing rules use `substitution` (`B{0 := u}`) and `lifting` (`lift₀`) operations of the Bruijn indexes, whose definitions are standard.

```
type_LetIn : ∀ na b B t s1 A,
            Σ ; Γ ⊢ B : tSort s1 → Σ ; Γ ⊢ b : B →
            Σ ; Γ , na := b : B ⊢ t : A →
            Σ ; Γ ⊢ tLetIn na b B t : tLetIn na b B A
```

The typing rule for let-bindings, `type_LetIn`, is somehow a mix of `type_Lambda` and `type_App`. Note that the body `t` is typed in a context extended by a definition `na := b : B`, rather than a mere assumption, making it possible to use the value of that variable when typing `t`, as expressed by rule `cumul_rel` for cumulativity. In the typing rule `type_Prod` for products, `sort_of_product` is the maximum of the two levels (encoded as a non-empty set of levels) when `s₂` is not `tProp` and `tProp` otherwise. This rule makes `tProp` impredicative, as it is possible to remain in `tProp` even when quantifying over an arbitrary type, including `tProp` itself.

```
type_Cumul : ∀ t A B s,
            Σ ; Γ ⊢ t : A → Σ ; Γ ⊢ B : tSort s →
            Σ ; Γ ⊢ A ≤s B →
            Σ ; Γ ⊢ t : B
```

The Rule `type_Cumul` is the rule for cumulativity, which directly uses the definition of §3.3. Because cumulativity is untyped, we explicitly impose here that the target type `B` is a valid type. This is necessary to prove the validity theorem and we will later show in §5 that the two types are necessarily in the same universe hierarchy, i.e., that the sorts of `A` and `B` are related (both are `Prop` or both are `Type`). The Rule `type_Const` for typing a constant requires that it is declared in the global environment, and that the provided universe instance `u` respects the universe constraints `d.(cst_universe)` from that declaration.
$\Sigma$, univers ; $\Gamma_{ar}$ ++ $\Gamma_{param}$@[u] ++ $\Gamma_{args}$@[u] $\vdash$ indices@[u] $\approx_S$ indices@[v].

These invariants are sufficient to show that reduction preserves typing. In the verified type
checker, we also need to develop a decision procedure based on the conversion test to check that
these judgments hold when checking inductive type declarations. They follow rather directly from
this specification.

2.6.3 *Allowed Elimination*. The sort Prop of Coq is meant to be computationally irrelevant: objects in sort Type (i.e., terms t : T with T : Type) should not depend in any relevant way on objects in sorts Prop (i.e., terms t : P with P : Prop). This is crucial for three reasons. First, because Prop is compatible with the axiom of proof irrelevance. Second, because due to the impredicativity of Prop, the type theory would otherwise be inconsistent [Coquand 1989; Geuvers 2007]. And third, for extraction to programming languages to safely erase propositional content, computational content should not depend on it in any non-trivial manner.

To enforce this irrelevance, Coq restricts the elimination of inductive types defined in the sort Prop to types in the sort Type. For inductive types in Prop, such an elimination is only allowed if the so-called subsingleton elimination criterion applies.<fnref n="13" /> An inductive in sort P is considered a subsingleton when it has at most one constructor, where all arguments have sort Prop again, i.e., are of type P : Prop for some P.

As explained above, in PCUIC, each inductive type in a mutual block contains a field `ind_kelim` expressing the sort in which an inhabitant of said inductive type is allowed to be eliminated. It is of type `allowedEliminations` defined as follows:<fnref n="14" />

`Inductive allowedEliminations : Set := IntoProp | IntoAny.`

The functions `elim_sortProp_ind` computes the minimal elimination sort allowed for an inductively defined proposition, given as input the list of lists of sort arguments of each constructor:

Fixpoint elim_sortProp_ind (ind_actors_sort : list (list Universe)) :=
  match ind_actors_sort with
  | [] => IntoAny
  | [ tProp :: s ] => elim_sortProp_ind [s]
  | _ => IntoProp
  end.

For an inductive definition to be valid, its allowed eliminations, recorded in the field `ind_kelim`, should be at least as restrictive as the minimal one computed using `elim_sortProp_ind`.

3 EQUIVALENT ALGORITHMIC SPECIFICATION OF PCUIC

In order to fill the gap between the abstract declarative specifications of universes, cumulativity and typing given in § 2 and the candidate implementation, this section introduces an equivalent but more algorithmic specification.

For universes, the notion of consistent universe hierarchy based on valuations into natural numbers is shown to be equivalent to an acyclicity criterion on the induced graph. The notion of cumulativity between t and u is shown to be equivalent to the fact that both terms reduce respectively to terms which are syntactically equal (up to cumulativity on universe levels). In particular, this definition removes the transitivity rule, and we show instead that transitivity is admissible thanks to the confluence of reduction. Finally, the typing judgement is shown to be

<footnote n="13">¹³Coq's official terminology is "empty or singleton elimination".</footnote>

<footnote n="14">¹⁴Actually, the current development also mentions the sort SProp but this is beyond the scope of this paper.</footnote>
type_Ind : ∀ ind u mdecl idecl,
wf_local Σ Γ → declared_inductive Σ ind mdecl idecl →
consistent_instance_ext Σ mdecl.(ind_universes) u →
Σ ; Γ ⊢ tInd ind u : idecl.(ind_type)@[u]

type_Construct : ∀ ind i u mdecl idecl cdecl,
wf_local Σ Γ → declared_constructor Σ (ind, i) mdecl idecl cdecl →
consistent_instance_ext Σ mdecl.(ind_universes) u →
Σ ; Γ ⊢ tConstruct ind i u : type_of_constructor mdecl cdecl (ind, i) u

Similarly, rules type_Ind and type_Construct check that the inductive type and constructor are
declared in the global environment, with a consistent universe instance. The rule to accept the
definition of a new constant or inductive type are given in the definition of a well-formed global
environment in § 3.6. Since the three typing rules type_Const, type_Ind, and type_Construct are
very similar, they could be unified with a single construction, as done for instance in CoQ-Elpi [Tassi
2018].

type_Case : ∀ ci p c brs indices ps mdecl idecl,
let predctx := case predicate_context ci.(ci_ind) mdecl idecl p in
let ptm := it_mkLambda_or_LetIn predctx p.(preturn) in
declared_inductive Σ ci.(ci_ind) mdecl idecl →
Σ ; Γ ++ predctx ⊢ p.(preturn) : tSort ps →
Σ ; Γ ⊢ c : mkApps (tInd ci.(ci_ind) p.(puinst)) (p.(pparams) ++ indices) →
case_side_conditions Σ Γ ci p ps mdecl idecl indices predctx →
caseahanbng Σ Γ ci p ps mdecl idecl ptm brs →
Σ ; Γ ⊢ tCase ci p c brs : mkApps ptm (indices ++ [c])

The Rule type_Case represents typing of pattern matching. It basically asks for the scrutinee c, the
return type p.(preturn) and each branch to be well typed, and for the inductive type of the scrutinee
to be declared; but there are also side conditions imposed by the predicate case_side_conditions.
The two main parts are that the universe instance must be consistent and that the elimination must
be allowed (in the case of Prop, elimination is restricted to subsingleton elimination, see §3.6.3). Case
analysis is forbidden for coinductive types because it is known to break subject reduction (see §5.4).

type_Proj : ∀ p c u mdecl idecl cdecl pdecl args,
          declared projection Σ p mdecl idecl cdecl pdecl → #|args| = ind_npars mdecl →
          Σ ; Γ ⊢ c : mkApps (tInd (fst (fst p)) u) args →
          Σ ; Γ ⊢ tProj p c : subst₀ (c :: List.rev args) (snd pdecl)@[u]

Rule type_Proj is the typing rule for projection of record types (which are described using the
constructor tInd as for (co-)inductive types). It checks that p is a well-declared projection of the
record fst (fst p). If this is the case, the projection's type is snd pdecl substituted by the list of
arguments c :: List.rev args (as defined by the operation subst₀).
**Definition Edge** := $V * Z * V$.

**Definition RootedGraph** := $(V \cup E) * (G \cup \Gamma) * V$.

**Definition EdgeOf** (*G* : RootedGraph) *x* *y* := {*N* : Z & EdgeSet.In (*x*, *n*, *y*) (*E* *G*)}.

**Inductive PathOf** *G* : *V* → *V* → **Type** :=

* pathOf_refl : ∀ *x*, PathOf *G* *x* *x*

* pathOf_step : ∀ *x* *y*, *EdgeOf* *G* *x* *y* → PathOf *G* *y* *y* → PathOf *G* *x* *y*.

**Fixpoint weight** {*x* *y*} (*p* : PathOf *G* *x* *y*) :=

match *p* with

* pathOf_refl *x* ⇒ 0

* pathOf_step *e* *p* ⇒ *e* 1 + **weight** *p*

end.

**Definition acyclic** *G* := ∀ *x* (*p* : PathOf *G* *x* *x*), **weight** *G* *p* ≤ 0.

<caption>Fig. 4. Definition of acyclicity for a graph</caption>

equivalent to a bidirectional presentation, where the cumulativity rule corresponding to `type.cumul` is only used in a restricted way, giving rise to canonical typing derivations.

## 3.1 Universes: Valuation vs Acyclicity

The specification of universe consistency (§2.2) as the existence of a valuation into natural numbers which respects the constraints on the universes does not directly give rise to a decision procedure. In CoQ, the implementation of this consistency check is performed using an acyclicity check on the weighted graph induced by the constraints. We thus formalize this notion of weighted graph, the acyclicity condition, and show its equivalence with consistency defined using a valuation.

Our formalization uses finite sets, which we represent using AVL trees from the standard library.<fnref n="15" />
Given a type *A*, we write `ASet` for the type of finite sets with elements in *A*.

Our notion of weighted graph (Fig. 4) is parametrized by a type *V* of nodes (assumed fixed in this explanation, for simplicity). An edge between *x* and *y* of (possibly negative) weight *z* is represented as a tuple (*x*,*z*,*y*). Such an edge encodes the constraint `Le z` between *x* and *y*, i.e., the fact that the valuation should satisfy *x* + *z* ≤ *y*.

Then, a rooted graph *G* is a weighted graph (whose set of edges is written *E* *G*) with a distinguished node *s* *G* in *V*, the root of the graph. We need our weighted graphs to be rooted because a graph representing a universe hierarchy always contains *lzero*, a level smaller than all the others (apart from `tProp` which is treated separately and not represented in the graph), and this plays a particular role as we thus know that the graph has a single connected component.

The type of edges between the two nodes *x* and *y* is written `EdgeOf` *G* *x* *y*. And the type of paths between two nodes *x* and *y* is written `PathOf` *G* *x* *y*. It is inductively defined and can either be the reflexive path (using `pathOf_refl`) or the concatenation of an edge in `EdgeOf` *x* *y* and a path in `PathOf` *G* *y* *y* (using `pathOf_step`). The notion of **weight** is extended to paths by simply taking the sum of the weight of each edge it is composed of.

<footnote n="15">¹⁵https://coq.inria.fr/stdlib/Coq.MSets.MSetAVL.html</footnote>
```c
type_Fix:   ∀ mfix n decl,
            wf_local Σ Γ → fix-guard Σ Γ mfix → nth_error mfix n = Some decl →
            wf擎 Σ mfix → All (fun d ⇒ {s & Σ; Γ ⊢ d.(dtype) : tSort s}) mfix →
            All (fun d ⇒ Σ; Γ ++ fix-context mfix ⊢ d.(dbody) : lift₀ #|fix_context mfix| d.(dtype)) mfix →
            Σ; Γ ⊢ tFix mfix n : decl.(dtype)
```

```c
type_CoFix:   ∀ mfix n decl,
            wf_local Σ Γ → cofix-guard Σ Γ mfix → nth_error mfix n = Some decl →
            wf_cofix Σ mfix → All (fun d ⇒ {s & Σ; Γ ⊢ d.(dtype) : tSort s}) mfix →
            All (fun d ⇒ Σ; Γ ++ fix-context mfix ⊢ d.(dbody) : lift₀ #|fix_context mfix| d.(dtype)) mfix →
            Σ; Γ ⊢ tCoFix mfix n : decl.(dtype)
```

Finally, Rules type_Fix and type_CoFix are the typing rules for mutual fixpoints and cofixpoints. The typing hypotheses are similar, and enforce for each of the mutually defined (co)fixpoints that its type dtype is a valid type, in the sense that it has a sort, and that its body dbody has type dtype in the local context extended by the fixpoint definition (so as to allow for recursive calls). What sets these rules apart are the guard conditions fix-guard and cofix-guard, which remain abstract as explained in §3.4, and the well-formedness conditions wf擎 and wf_cofix. These mainly check that the type of the recursive argument of a fixpoint is an inductive type, and that the codomain of a cofixpoint is a coinductive type.

In the Coq development, the typing relation is parametrized by a record of flags. The flags are also used in the verified type-checking algorithm we explain later, and the type is thus called checker_flags. We show it here with comments to explain what every flag stands for:

```c
Class checker_flags := {
    check_univ : B;
    (* default true, setting to false adds the (inconsistent) Type : Type rule *)
    prop_sub_type : B;
    (* default true, false for extraction, enables Prop <: Type *)
    indices_matter : B;
    (* default false, lets indices matter for the type universe of an inductive *)
    lets_in_constructor_types : B;
    (* default true, allows constructor types to contain lets *)
};
```

The theory we develop assumes in general that universes are checked, the Prop ≤ Type rule is available (except for the erasure correctness proofs), indices_matter is false (this otherwise makes type checking of inductive declarations compatible with the Homotopy Type Theory interpretation of inductive types) and let-bindings are allowed in constructor types. A verified translation allows to move from the presentation with let-bindings in constructors to one where they have been expanded.

## 3.6 Well-Formed Environments

The definition of the typing judgment is relative to a global environment that contains the global constants and inductive definitions. For typing to be well behaved, this global environment must be well formed (denoted wf Σ). Beyond enforcing that all definitions are well typed, this well-formation condition also contains constraints about universes and cumulativity, and in the case of inductive types, allowed eliminations of its inhabitants, and the (strict) positivity criterion.

More precisely, an environment is represented as a record of a global universe context (a set of levels and a set of universe constraints) and an association list of (unique) kernel names to constant or inductive declarations.
Acyclicity of a weighted graph can then be stated as the fact that every reflexive path has a negative weight. This is more relaxed than asking that every reflexive path is of weight 0, because it allows for strictly negative reflexive paths, but it actually captures all valid inequations. For instance, consider the constraints $x \le y+2$ and $y+1 \le x$. These two constraints correspond to edges $(x,-2,y)$ and $(y,1,x)$, which give rise to reflexive path of weight $-1$ on $x$, encoding the constraint $x-1 \le x$, which is perfectly valid, although useless.

Now, we turn to the formalization that the acyclicity of the graph induced by the constraints is equivalent to the existence of a valuation respecting the constraints. First, it is easy to define a notion of correct labeling of a graph (where $labeling := V \to N$), which corresponds to the notion of a valuation satisfying the constraints.

**Definition correct_labeling (l : labeling) :=**
$$l(sG) = 0 \land \forall x n y, \text{EdgeSet.In}(x,n,y) (E G) \to l x + n \le l y.$$

We now turn to show that acyclicity is equivalent to the existence of a correct labeling. To do so, we use the notion of longest simple path between two nodes, which provides at the same time a characterization of acyclicity and a decision procedure to check acyclicity.

A simple path in SPath $s \times y$ is a path from $x$ to $y$ going only through the nodes in $s$, without visiting twice the same node, except for the last one which can appear twice (thus forming a loop).<fnref n="16" />

**Inductive SPath : VSet $\to$ V $\to$ V $\to$ Type :=**
$$\begin{align*}
\text{spath_refl} & : \forall s x, \text{SPath s x x} \\
\text{spath_step} & : \forall s s' x y z, \text{DisjointAdd x s s'} \to \text{EdgeOf G x y} \to \text{SPath s y z} \to \text{SPath s' x z}.
\end{align*}$$

From this notion, it is possible to compute the weight of the longest simple path (or simply lsp) between two nodes by taking the maximum of all possible simple paths between $x$ and $y$. The difficulty with this definition is that it is recursive, and the recursive call is done on a subset of the original set $s$ of nodes that can be visited, which is not structurally decreasing. To overcome this issue, we use the standard fuel trick, because we know that the number of necessary recursive calls is bounded by the cardinal of $s$.

**Fixpoint lsp₀ (fuel:N) (s : VSet) (x z : V) : option Z :=**
$$\begin{align*}
\text{let base} &:= \text{if } V \text{eq\_dec} x z \text{ then } \text{Some } 0 \text{ else } \text{None} \text{ in} \\
\text{match fuel with} \\
&\quad 0 \Rightarrow \text{base} \\
&\quad S \text{ fuel} \Rightarrow \\
&\quad \begin{align*}
\text{match mem x s with} \\
\quad \text{true} \Rightarrow \text{let ds} &:= \text{map (fun ' (n, y)} \Rightarrow \text{Some } n + \text{lsp}_0 \text{ fuel (remove x s) y z} \text{) (succs x)} \text{ in} \\
&\quad \text{fold\_left max ds base} \\
\quad \text{false} \Rightarrow \text{base} \\
\end{align*}
\end{align*}$$

**Definition lsp s := lsp₀ (cardinal s) s.**

where `succs x` computes the list of edges with source $x$. Note that the function goes to option $Z$ because there may not be any path between $x$ and $y$. Thus, the constructor `None` of option $Z$ corresponds to $-\infty$ when extending addition, maximum, and comparison to option $Z$.

We then show that `lsp s x y` is equal to the maximum of weights of simple paths from $x$ to $y$.

<footnote n="16">¹⁶The usual notion of simple path does not allow such a repetition, but we need it to handle constraints between a level and itself.</footnote>
Inductive global decl :=

| ConstantDecl : constant_body → global Decl

| InductiveDecl : mutual_inductive_body → global decl.

Definition global_declarations := list (kername * global decl).

Record global_env :=

{ universes : LevelSet * UnivConstraintSet; declarations : global_declarations }.

Note that this is the specification of a global environment, but CoQ’s algorithm uses a more efficient
representation. In § 6, we describes a type checker that is abstract with respect to a particular choice
of representation, as long as it is equivalent to the specification.

Constant declarations (constant_body) record the type (cst_type) and optional body (cst_body) of said constant, and a universe declaration (cst_universes). The presence or absence of a body discriminates between a Definition and an Axiom.

Record constant_body := {

cst_type : term;

cst_body : option term;

cst_universes : universes decl }.

The universe declaration is either monomorphic or polymorphic:

Inductive universes decl : Type :=

| Monomorphic_ctx

| Polymorphic_ctx (cst : list name * UnivConstraintSet).

Monomorphic declarations do not introduce universes or constraints as they rely on those already declared in the global universe context. Polymorphic definitions come with an abstract universe context: a list of variables and constraints on them that are instantiated at each use of a polymorphic construction.

Inductive types have more structure. In full generality, they are represented as a mutual inductive
block. Actually, the same representation is used to encode inductive, co-inductive or record types
(with potentially primitive projections). This common representation allows us to factorize the
many similarities in the specification of those types.

Record mutual_inductive_body := {

ind finite : recursivity kind; ind npars : N ; ind params : context;

ind_universes : universes decl; ind_variance : option (list Variance);

ind Bodies : list one_inductive_body }.

Mutual inductive blocks have a recursivity_type annotation to distinguish between inductive, co-inductive and non-recursive types—as introduced with the Variant keyword in CoQ. Note in particular that it is not possible to mix inductive and co-inductive definitions in the same mutual inductive block. All inductive types in a block share a context of parameters ind_params, whose number of assumptions is recorded in ind_npars, a universe declaration and an optional universe variance annotation (discussed in § 3.6.2). Finally, there is a (non-empty) list of inductive bodies representing each (co-)inductive type in the mutual block:

Record one_inductive_body := {

ind_name : ident; ind_indexes : context; ind_sort : Universe; ind_type : term;

ind_kelim : allowedEliminations;

ind_actors : list constructor_body ; ind_projs : list projection_body }.
Lemma lsp_spec_le s x y (p : SPath s x y) : Some (weight p) ≤ lsp s x y.

Lemma lsp_spec_eq s x n : lsp s x y = Some n → ∃ p : SPath s x y, weight p = n.

With this notion of lsp, we can prove that acyclicity is equivalent to the existence of a correct labeling, by showing that acyclicity implies that the weight of the longest simple reflexive path on x is 0. This allows us to derive the fact that the labeling induced by the weight of the longest simple path from the root is correct when the graph is acyclic.

Lemma acyclic_lsp s x : acyclic G → lsp s x x = Some 0.

Lemma lsp_correctness : acyclic G → correct_labeling (fun x ⇒ option_get 0 (lsp V (s G) x)).

Conversely, we can show that the property of a correct labeling extends to paths, from which we directly conclude that the existence of a correct labeling implies acyclicity of the graph.

Lemma correct_labeling_PathOf l : correct_labeling l →

V x y (p : PathOf G x y), x + weight p ≤ l y.

Lemma acyclic_labeling l : correct_labeling l → acyclic G.

In particular, it gives us a decision procedure to check that a graph is acyclic, by simply checking that lsp V x x is 0 for every node x in the graph (see §5.2.3). To conclude, we just need to remark that the existence of a correct labeling is equivalent to the existence of a valuation that satisfies the constraints of the graph.

## 3.2 Conversion: Algorithmic presentation with equality and reduction

The specification of cumulativity and conversion of §2.3 is quite far from a decision procedure. First, the transitivity rule cumul_Trans can be applied at any time, making an intermediate term appear out of thin air. Second, when looking at conversion, the symmetry rule can always be applied twice, without any progress in the comparison. Finally, when comparing inductive types and constructors, for instance mkApps (tInd i u) args and mkApps (tInd i u') args', several rules can be applied and in particular cumul_Ind which compares them up to cumulativity and cumul_App which compares them as standard constants. Thus, we have some kind of critical pairs in the definition of a cumulativity derivation.

To remedy this issue, it is common to decide conversion by using reduction instead. The idea is that two terms are convertible if and only if they can both be reduced to the same term. In the presence of universe polymorphism and cumulativity, the notion of “same term” needs to be relaxed to syntactical equality up to universes.

In this section we define an algorithmic notion of cumulativity based on reduction and show that it is indeed equivalent to cumulativity defined in §2.3 and given in full in Figs. 19 and 20. The main technical ingredient of the proof is confluence of reduction.

### 3.2.1 Reduction and Syntactical Equality up to Universes.

Single step reduction of PCUIC terms is defined in Fig. 5, and written $Σ ; Γ ⊢ t ↣ u$. We only show representative cases, as the definition shares a lot with the definition of cumulativity. Basically, reduction corresponds to the computation and congruence rules of cumulativity. For computation rules, they are literally the same, as the reader can check on red_beta and red_iota. Congruence rules however are slightly different because we do not want the reduction to be parallel, so we need a rule per argument of a constructor. For instance, in the case of tLambda, there are two rules: abs_red_l which reduces the type annotation, and abs_red_r which reduces the body of the lambda.

From this single step reduction, general reduction is simply defined as its reflexive and transitive closure.

Notation $"Σ ; Γ ⊢ t ↣^* u" := clos_refl_trans (fun t u : term ⇒ Σ ; Γ ⊢ t ↣ u)$.
Each inductive type has a name `ind_name` and an arity `ind_type` which should decompose into a dependent product starting with the shared parameters, the indices `ind_indices` and a sort `ind_sort` as conclusion.<fnref n="13" /> The allowed elimination sorts of its inhabitants is described by the `ind_kelim` parameter (see §3.6.3 for a detailed explanation). The (possibly empty) list `ind_actors` records for each constructor their name, context of arguments, and the indices at which they instantiate the conclusion’s inductive type (the parameters are fixed for a whole mutual family). Finally, the projections (for primitive records) record the name and type of each projection.

Record constructor_body := { cstr_name : ident; cstr_args : context; cstr_indices : list term }.

Record projection_body := { proj_name : ident; proj_type : term }.

Altogether, this data forms the raw structure of global environments of PCUIC. Well-formed global environments impose strict restrictions on this data.

* First, all names should be globally unique.<fnref n="14" />

* For constants, the declared type should be typeable by a sort and the optional constant body should be typeable using the declared type, in the universe context associated with `cst_universes`.

* For inductive blocks, the inductive types, constructors and projections should all be well typed, but this is not enough: various extra properties are imposed on these blocks. We will describe them in the remainder of this section.

### 3.6.1 Positivity criterion.
Allowing arbitrary recursive types breaks strong normalization, as the untyped $\lambda$-calculus can easily be expressed using such arbitrary recursive types. Hence, Coq restricts the class of definable inductive types to strictly-positive ones. Coarsely, strict positivity ensures that one can always derive a meaningful elimination rule with induction hypotheses for each recursive argument of each constructor [Coquand and Paulin 1990].

We formalize the strict positivity condition as a predicate on the shapes of constructors of an inductive declaration (Fig. 3). It relies on an auxiliary predicate that checks positivity of each type argument of a constructor. A constructor argument `ty` is positive with respect to a mutual inductive declaration `m` in context $\Gamma$, written $m; \Gamma \vdash_+^{arg} ty$, when its weak $\zeta$-normal form (meaning let-in are reduced away) either:

* does not mention the inductive block, or

* is of shape `mkApps` (`tRel k`) 1 where `k` refers to an inductive in the block (checked using `mdecl_at_i`) and 1 does not refer to the inductive block, or

* is of shape `tProd na ty ty'` where `ty` does not mention the inductive block and `ty'` is inductively positive in the context extended with `na : ty`.

The context $\Gamma$ tracks the parameters and arguments of the constructor, while de Bruijn references above `#|Γ|` represent the inductive types in the block.

Then, a constructor type `ty` is strictly positive, written $m@i; \Gamma \vdash_+ ty$, with respect to a mutual inductive declaration `m` and inductive `i` in this block in context $\Gamma$ when its weak $\zeta$-normal form is of shape `tProd na_1 ty_1 (tProd na_2 ty_2 (tProd ... concl))` where moreover:

* all the arguments in `ty_i` are positive; and

* the conclusion `concl` is of shape `mkApps` (`tRel k`) `args` where `k` refers to the current inductive `i` and `args` do not mention any of the inductive types in the block.

<footnote n="13">¹³Arities are the subset of n-ary dependent products and let-ins whose final codomain is a sort</footnote>

<footnote n="14">¹⁴Technically in Coq, there is a notion of namespace to be able to use the same name in different modules or files, so globally is to be understood up to name space.</footnote>
Inductive "Σ; Γ ⊢ _ ↝ _": term → term → Type :=
| red beta : ∀ na t b a,
    Σ; Γ ⊢ tApp (tLambda na t b) a ↝ b {0 := a}
| red iota : ∀ ci c u args p brs br,
    nth_error brs c = Some br → #|args| = ci.(ci_npar) + context_assumptions br.(bcontext) →
    Σ; Γ ⊢ tCase ci p (mkApps (tConstruct ci.(ci_ind) c u) args) brs ↝ iota_red ci p args br
| ... (** Other computation rules are similar *)
| abs red_1 : ∀ na ty ty' t,
    Σ; Γ ⊢ ty ↝ ty' → Σ; Γ ⊢ tLambda na ty t ↝ tLambda na ty' t
| abs red_r : ∀ na ty t t',
    Σ; Γ, na : ty ⊢ t ↝ t' → Σ; Γ ⊢ tLambda na ty t ↝ tLambda na ty' t
| ... (** Other congruence rules are similar **)

Inductive "Σ ⊢ _ ≤<sup>R1e</sup><sub>napp</sub> _": term → term → Type :=
| eq_Rel : ∀ n,
    Σ ⊢ tRel n ≤<sup>R1e</sup><sub>napp</sub> tRel n
| eq_Sort : ∀ s s',
    R1e s s' → Σ ⊢ tSort s ≤<sup>R1e</sup><sub>napp</sub> tSort s'
| eq_Lambda : ∀ na na' ty ty' t t',
    eq_binder_annot na na' → Σ ⊢ ty ≤<sup>Re</sup><sub>0</sub> ty' → Σ ⊢ t ≤<sup>R1e</sup><sub>0</sub> t' →
    Σ ⊢ tLambda na ty t ≤<sup>R1e</sup><sub>napp</sub> tLambda na' ty' t'
| eq_App : ∀ t t' u u',
    Σ ⊢ t ≤<sup>sR1e</sup><sub>Snapp</sub> t' → Σ ⊢ u ≤<sup>Re</sup><sub>0</sub> u' →
    Σ ⊢ tApp t u ≤<sup>R1e</sup><sub>napp</sub> tApp t' u'
| eq_Ind : ∀ i u u',
    R_global_instance Σ Re R1e (IndRef i) napp u u' →
    Σ ⊢ tInd i u ≤<sup>R1e</sup><sub>napp</sub> tInd i u'
| ... (** Other cumulativity and congruence rules are similar **)

<caption>Fig. 5. Single step reduction and syntactical equality up to universes (excerpt)</caption>

The fundamental property that reduction satisfies is confluence. Its proof is involved and requires
several auxiliary notions, so we defer its explanation to § 4. However, let us just state the relevant
result for this section: reduction is confluent on well-scoped terms (that is terms whose variables
are bound in the local context Γ).

Lemma red_confluence Γ (t : open_term Γ) u v :
Σ ; Γ ⊢ t ↝* u → Σ ; Γ ⊢ t ↝* v → {v' & Σ ; Γ ⊢ u ↝* v' * Σ ; Γ ⊢ v ↝* v'}.,

Syntactical equality up to universes is also defined in Fig. 5, and written Σ ⊢ t ≤<sup>R1e</sup><sub>napp</sub> u. Basically, it contains the cumulativity and congruence rules of cumulativity. Note that syntactical equality does not depend on a local context because variables are compared syntactically (Rule eq_Rel), but it depends on a relation R1e comparing universes and a natural number n<sub>app</sub>. The index R1e is used in the exact same way as for cumulativity, to compare universes and inductive types up to cumulativity. The index n<sub>app</sub> deserves more explanation.

Because we want the algorithmic specification to be closer to a decision procedure, we do not
want to have the critical pairs that we have for the specification of cumulativity/conversion. This
means that to compare mkApps (tInd i u) args and mkApps (tInd i u') args' we always want to use
Inductive _:_Γ⁺arg_ (m: mutual_inductive_body) (Γ:context) : term → Type :=
| pos_arg_closed ty : closedn #Γ| ty → m ; Γ ↳⁺arg ty
| pos_arg_concl l k i : #|l| = ind_realargs i → All (closedn #Γ|) l →
  mdecl_at_i m i Γ k → m ; Γ ↳⁺arg mkApps (tRel k) l
| pos_arg_let na b ty ty' : m ; Γ ↳⁺arg ty' {0 := b} → m ; Γ ↳⁺arg tLetIn na b ty ty'
| pos_arg_ass na ty ty' : closedn #Γ| ty → m ; na : ty ::= Γ ↳⁺arg ty' → m ; Γ ↳⁺arg tProd na ty ty'.

Inductive _@_;Γ+_ (m: mutual_inductive_body) (i:N) (Γ:context) : term → Type :=
| pos_let na b ty ty' : m @ i ; Γ ↤_+ ty' {0 := b} → m @ i ; Γ ↤_+ tLetIn na b ty ty'
| pos_ass na ty ty' : m ; Γ ↤⁺arg ty → m @ i ; na : ty ::= Γ ↤_+ ty' → m @ i ; Γ ↤_+ tProd na ty ty'
| pos_concl l : All (closedn #Γ|) l → m @ i ; Γ ↤_+ mkApps (tRel (#|m.(ind_bodies)| - S i + #|Γ|)) l.

<caption>Fig. 3. Positivity judgment</caption>

We (weakly) $\zeta$-normalize types (as Coq does), so this definition allows *unused* let-bindings to mention the inductive type, potentially in a non-strictly positive way. It is however clear that the same inductive type without the unused let-bindings is equivalent for all purposes.

This definition is a simplification of the actual criterion of Coq which additionally handles *nested* inductive types [Abbott et al. 2004], i.e., inductive types where a constructor can take as argument another inductive type applied to one of the mutually defined ones. A typical example is that of rose trees: a tree where the single node constructor takes a *list* of subtrees.

### 3.6.2 Cumulative Inductive Types.
CoQ additionally features cumulative inductive types, which extends the cumulativity relation through polymorphic inductive families. Intuitively, this allows “smaller” instances of an inductive family to be used where a larger one is expected. A typical example is given by the type of lists: an object of type `list@{Set} N` can be used anywhere a `list@{i} N` is expected, without introducing an explicit coercion. Another useful intuition is that such a subtyping is justified because we could automatically introduce identity coercions in such places, which do not change the computational content of the objects, but only their universe annotations.

In the original presentation [Timany and Sozeau 2018], inductive types do not have parameters and the cumulativity relation is extended by a general judgement asserting that two inductive families I and I' are in the cumulativity relation when:

* they have the same number of constructors

* for each pair of types of corresponding constructors `ty` and `ty'`, each pair of constructor argument types are in the cumulativity relation, assuming $I \le I'$ inductively.

For two universe instantiations of the polymorphic `list@{i}` datatype on carrier type `A`, e.g., corresponding to types `list@{k}` `A` and `list@{l}` `A` in the theory with parameters, this requires to consider only the `cons_A:A → list@{i} A → list@{i} A` case and check that `A \le A` and `list@{k} A \le list@{l} A`. The first one holds by reflexivity while the second one is our induction hypothesis. In this case we can see that actually no particular relationship should hold on the universe levels 1 and `k`, meaning that all `list@{\_} A` types are convertible.

More interestingly, inductive families that actually embed universes lift to the cumulativity relation. In particular all records including a carrier type field and some operations and properties on them fall into this subset. Typically, suppose we define the type of monoids as a record:

Record monoid@{u} := { carrier : Type@{u} ; unit : carrier ; op : carrier → carrier → carrier }
Inductive "Σ ; Γ ⊢ _ ≤<sup>R1e</sup><sub>a</sub> _": term → term → Type :=
| cumul_syntactical_eq : ∀ t u,
Σ ⊢ t ≤<sup>R1e</sup><sub>0</sub> u → Σ ; Γ ⊢ t ≤<sup>R1e</sup><sub>a</sub> u
| cumul_red_l : ∀ t u v,
Σ ; Γ ⊢ t ↝ v → Σ ; Γ ⊢ v ≤<sup>R1e</sup><sub>a</sub> u → Σ ; Γ ⊢ t ≤<sup>R1e</sup><sub>a</sub> u
| cumul_red_r : ∀ t u v,
Σ ; Γ ⊢ t ≤<sup>R1e</sup><sub>a</sub> v → Σ ; Γ ⊢ u ↝ v → Σ ; Γ ⊢ t ≤<sup>R1e</sup><sub>a</sub> u.

<caption>Fig. 6. Algorithmic cumulativity</caption>

congruence of application (Rule eq_App). As such, the congruence rule eq_Ind for tInd needs to
account for cumulativity. However, we have an issue here because the cumulativity rule only
applies to fully applied inductive types. This is why we need to store the number of applications
that we have traversed during the syntactic equality check: this is the exact purpose of the n<sub>app</sub>
index.

Indeed, Rule eq_App increments the index in the premise of the the applied functions (here Σ ⊢ t ≤<sub>Sn<sub>app</sub></sub><sup>R1e</sup> t'). Note that the index is reset to 0 for the premise on the arguments of the application.

For other congruence rules, such as eq_Lambda, n_app is reset to 0 in the premise to account for the fact that we are not under an n-ary application.

Is it not difficult to show that syntactical equality up to universes is reflexive, symmetric and transitive as soon as the relations Re and R1e comparing universes are as well.

3.2.2 Algorithmic cumulativity and its properties. Algorithmic cumulativity between two terms is defined as the fact these two terms reduce to terms that are syntactically equal up to universes (see Fig. 6).

We now turn to the proof that this algorithmic presentation of cumulativity is equivalent to
the abstract specification. Thus, algorithmic cumulativity provides a crucial intermediate point
between the abstract specification and the concrete implementation of cumulativity/conversion.

To show that algorithmic cumulativity implies the abstract specification, we only have to show
that all the rules of reduction and syntactic equality up to universes are admissible rules of the
abstract specification.

For reduction, this is fairly straightforward, as the computation rules are literally the same, the
only remaining work is to use reflexivity of the abstract specification to be able to encode the
non-parallel congruence rule of reduction.

Proposition red cumulSpec Γ t u : Σ ; Γ ⊢ t ↝ u → Σ ; Γ ⊢ t ≈<sub>s</sub> u.

The proof that the rules of syntactic equality up to universes are admissible requires to state a
more general lemma that essentially checks that the n<sub>app</sub> index of syntactic equality is computing
the number of applications in the right way.

Proposition eq_term_upto_univ cumulSpec (Γ : context) {Re R1e} t u args args' :
Σ ⊢ t ≤<sup>R1e</sup><sub>=|args|</sub> u → All2 (fun t u ⇒ Σ ; Γ ⊢ t ≤<sup>Re</sup><sub>s</sub> u) args args' →
Σ ; Γ ⊢ mkApps t args ≤<sup>R1e</sup><sub>s</sub> mkApps u args'.

Then, the fact that syntactic equality up to universes implies the abstract specification of cumu-
lativity is a direct consequence, when args and args' are the empty list.

From this, we can conclude directly that algorithmic cumulativity is correct, using transitivity of
the abstract specification.
In that case, the universe $u$ is used *covariantly* in the inductive definition, and cumulativity enables the use of a monoid$\{Set\}$ (e.g., natural numbers with addition) where a monoid at any higher type is expected. More generally monoid$\{i\} \le$ monoid$\{j\}$ whenever $i \le j$. In general, we can let Coq infer the variance of universes for cumulative inductive types (it is then printed using the About or Print commands), but there is also surface syntax to specify it. The inference performs a cumulativity test between two instances of the inductive type and gathers the necessary constraints for the first to be a subtype of the other, marking universe variables as irrelevant, covariant or invariant. As we are extending the Type cumulativity relation which is not contravariant on function domains, there is also no contravariant status here.

**Variance.** The notion of variance was introduced in Coq together with polymorphic cumulative inductive types to describe the status of each universe variable of an inductive declaration with a variance annotation that specifies how the universe variable behaves with respect to cumulativity, as exemplified above with list and monoid. However, variance for polymorphic cumulative inductive types has never been considered before from a formal point of view, and our work is the first place where this notion is formalized, and crucially so: we need specific properties of cumulative inductive types to complete the subject reduction proof (§ 5.4). The specification of cumulative inductive types ensures that the declared variances of a cumulative inductive type give rise to the expected subtyping relations between the types of inductives and each constructor. Variance is defined as a simple enumeration:

Inductive Variance.t := Irrelevant | Covariant | Invariant.

A variance annotation is simply a list of variances, one for each bound universe in a polymorphic definition.

In the remainder of this section, we consider a fixed cumulative inductive definition. From a variance annotation, along with the polymorphic universe context of the definition, we can generate a new context universs consisting of two copies of the polymorphic universe context instantiated at universe levels $u$ and $v$ (variance_universes), in addition to constraints witnessing the variance relationship between $u$ and $v$, i.e., no relationship for irrelevant universes, equality for invariant ones and inequality for covariant ones. This context is proven to be consistent, starting from a consistent inductive universe context.

From this data, we specify when the cumulative inductive type under consideration respects the variance annotations using two conditions.

**Inductive types.** Recall that the cumulative inductive type declaration is composed of a context of parameters, a context of indices and a conclusion sort. We write $\Gamma_{param}$ (resp. $\Gamma_{ind}$) for the context of parameters (resp. indices) where let-bindings have been expanded. The first condition expresses that $\Gamma_{ind}$ instantiated at $u$ is in the cumulativity relation with $\Gamma_{ind}$ instantiated at $v$, under the context of parameters at the “lower” instance of the universes, and that the constraints in universes are sufficient to derive this.

$$ \Sigma, \mathit{univs} ; \Gamma_{\mathit{param}}@[u] \vdash \Gamma_{\mathit{ind}}@[u] \leq_s \Gamma_{\mathit{ind}}@[v]. $$

We consider contexts where let-bindings have been expanded to avoid potentially useless constraints on let-bound variables. There is only one parameter context involved: it models the fact that cumulativity of inductive types in Coq only allows to subsume one instance of an inductive type by another when they share convertible parameters, as explained above. The only sensible choice here is to use the “lower” universe instance for the parameters here as the indices at levels $u$ might not be typeable if parameters are at a higher level $v$, but the converse holds (this is proven in PCUIC: InductiveInversion).
**Proposition cumulAlgo cumulSpec Rle Γ (t u : term) : Σ ; Γ ⊢ t ≤<sup>Rle</sup><sub>a</sub> u → Σ ; Γ ⊢ t ≤<sup>Rle</sup><sub>s</sub> u.**

For the opposite direction, the situation is more complicated as we need to show that some
rules, such as reflexivity, transitivity or symmetry, which are not at all present in the definition of
algorithmic cumulativity, are nevertheless admissible. As already mentioned, this strongly relies on
the fact the reduction is confluent, but only on well-scoped terms (see §4.3 for a counter-example
of unconditional confluence). This means that completeness of algorithmic cumulativity only holds
for well-scoped terms, but not for arbitrary ill-scoped terms. Fortunately, type checking only calls
cumulativity checking on well-typed terms, which are in particular well scoped, so this conditional
completeness is enough for our purpose.

To understand why confluence is a key property, consider three (well-scoped in Γ) terms t,
u and v, such that Σ ; Γ ⊢ t ≤<sup>Rle</sup><sub>a</sub> u and Σ ; Γ ⊢ u ≤<sup>Rle</sup><sub>a</sub> v. It may be the case that this holds because
Σ ; Γ ⊢ u ↛ t and Σ ; Γ ⊢ u ↛ v. But then, as the reduction is not deterministic, there is no reason
for t and v to be syntactically equal (up to universes) (for instance, one reduction could use Rule
cumul_red_1 while the other could come from Rule cumul_red_r), so the only sensible way to show
transitivity in this case is to have confluence and get a common reduct ρ(u) from t and v. This way,
in our example Σ ; Γ ⊢ t ≤<sup>Rle</sup><sub>a</sub> v holds by using Rules cumul_red_1, cumul_red_r and reflexivity on
ρ(u).

In fact, we have been able to show that this particular situation generalizes to the arbitrary case,
so that confluence of reduction is enough to deduce transitivity of algorithmic cumulativity (on
well-scoped terms). Beyond confluence, we also need that reduction and syntactic equality up
to universes behave well with respect to each other. More precisely, we show that the latter is a
simulation with respect to the former:

Lemma red<sub>1</sub>_eq_term_upto_univ_l {Σ Σ' : global_env} Re Rle n<sub>app</sub> Γ u v u' :
Σ' ⊢ u ≤<sup>Rle</sup><sub>n<sub>app</sub></sub> u' → Σ ; Γ ⊢ u ↛ v → ∃ v' , Σ ; Γ ⊢ u' ↛ v' × Σ' ⊢ v ≤<sup>Rle</sup><sub>n<sub>app</sub></sub> v'.

For the rest of the rules of the abstract specification of cumulativity, things are a bit simpler. Com-
putation rules are directly mimicked by the corresponding rules for the reduction, and cumulativity
rules are directly related to corresponding rules for the syntactic equality up to universes. Finally,
congruence rules are obtained by using corresponding congruence rules for both reduction and
syntactic equality up to universes. Of course, to prove that all those rules are admissible, there is a
fair amount of bureaucratic proof obligations popping up, but they are not particularly informative
and we refer the curious reader to the formalization for details.

Armed with all those admissible rules, it is now easy to prove completeness of algorithmic cumulativity.

**Proposition cumulSpec cumulAlgo Rle Γ (t u : open_term Γ) : Σ ; Γ ⊢ t ≤<sup>Rle</sup><sub>s</sub> u → Σ ; Γ ⊢ t ≤<sup>Rle</sup><sub>a</sub> u.**

3.3 Bidirectional Typing

The last step to go from the abstract specification to an algorithmic specification is to deal with
typing derivations (§2.5). We will call them undirected when needing to distinguish it from the
other judgments we are about to introduce.

The main difficulty here is Rule type_Cumul. Indeed, similarly to transitivity for cumulativity, it
can be used at any point in a typing derivation and involve a completely arbitrary type that cannot
be directly “invented” by an algorithm. However, we cannot completely remove the rule, as we
still need to retain the possibility to use computation on types inside derivation trees. Instead, we
distribute computation in two ways: we keep the possibility to use cumulativity between types, but
only at specific places where both types are known; and when not, we still allow reduction in some
other places in order to expose the head constructor of a type when this is required.
Inductive "Σ ; Γ ⊢ _ ▷ _" : term → term → Type :=

| infer_Rel n decl :

nth_error Γ n = Some decl →

Σ; Γ ⊢ tRel n ▷ lift₀ (S n) (decl_type decl)

| infer_Sorts s :

wf_universe Σ s →

Σ; Γ ⊢ tSort s ▷ tSort (Universe.super s)

| infer_Lambda na A t s B :

Σ; Γ ⊢ A ▷ ∎ s →

Σ; Γ , : na A ⊢ t ▷ B →

Σ; Γ ⊢ tLambda na A t ▷ tProd na A B

| infer_App t na A B u :

Σ; Γ ⊢ t ▷ Π (na,A,B) →

Σ; Γ ⊢ u ◀ A →

Σ; Γ ⊢ tApp t u ▷ B{0 := u}

| ... (**Other inference rules are similar**)

with "Σ ; Γ ⊢ _ ▷ Π ( _ , _ , _ )" : term → aname → term → term → Type :=

| infer productions T t na A B :

Σ; Γ ⊢ t ▷ T →

Σ; Γ ⊢ T ↪→ tProd na A B →

Σ; Γ ⊢ t ▷ Π (na,A,B)

with ... (**Other constrained inference judgments are similar**)

with "Σ ; Γ ⊢ _ ◀ _" : term → term → Type :=

| check_Cumul t T T' :

Σ; Γ ⊢ t ▷ T →

Σ; Γ ⊢ T ≤ₐ T' →

Σ; Γ ⊢ t ◀ T'.

<caption>Fig. 7. Bidirectional typing rules (excerpt)</caption>

The precise design of the structure of this type system takes a lot of inspiration from the actual kernel. In particular, we introduce a separation between the checking judgment, which expects a type as input, and the inference one, which instead outputs a type. This separation is the characteristic of so-called bidirectional typing algorithms, see the survey by Dunfield and Krishnaswami [2021] for an overview, and so this is also the name we adopt for this judgment.

Moreover, the kernel of Coq maintains the invariant that inputs to the type checker are always well formed—apart, of course, for the term whose well-formedness is under scrutiny. Conversely, outputs of type inference, and in particular inferred types, are always well formed. Those principles manifest in the proof of equivalence between the bidirectional and undirected system, as we will explain in § 3.3.2.

Standalone work [Lennon-Bertrand 2021, 2022], centered mainly around bidirectional typing in the context of CIC/PCUIC, has already appeared. We present here the most interesting points for META-Coq, but more details and general intuitions pertaining to this section can be found there.
**Definition Edge** := $V * Z * V$.

**Definition RootedGraph** := $(VSet * EdgeSet * V)$.

**Definition EdgeOf** (*G* : RootedGraph) *x* *y* := {*n* : Z & EdgeSet.In (*x*, *n*, *y*) (*E* *G*)}.

**Inductive PathOf** *G* : *V* → *V* → **Type** :=

| pathOf_refl : ∀ *x*, PathOf *G* *x* *x*

| pathOf_step : ∀ *x* *y*, *EdgeOf* *G* *x* *y* → PathOf *G* *y* *y* → PathOf *G* *x* *y*.

**Fixpoint weight** {*x* *y*} (*p* : PathOf *G* *x* *y*) :=

match *p* with

| pathOf_refl *x* ⇒ 0

| pathOf_step *e* *p* ⇒ e.1 + **weight** *p*

end.

**Definition acyclic** *G* := ∀ *x* (*p* : PathOf *G* *x* *x*), **weight** *G* *p* ≤ 0.

<caption>Fig. 4. Definition of acyclicity for a graph</caption>

For an inductive definition to be valid, its allowed eliminations, recorded in the field `ind_kelim`, should be at least as restrictive as the minimal one computed using `elim_sortProp_ind`.

# 4 EQUIVALENT ALGORITHMIC SPECIFICATION OF PCUIC

In order to fill the gap between the abstract declarative specifications of universes, cumulativity and typing given in § 3 and the candidate implementation, this section introduces an equivalent but more algorithmic specification.

For universes, the notion of consistent universe hierarchy based on valuations into natural numbers is shown to be equivalent to an acyclicity criterion on the induced graph. The notion of cumulativity between *t* and *u* is shown to be equivalent to the fact that both terms reduce respectively to terms which are syntactically equal (up to cumulativity on universe levels). In particular, this definition removes the transitivity rule, and we show instead that transitivity is admissible thanks to the confluence of reduction. Finally, the typing judgement is shown to be equivalent to a bidirectional presentation, where the cumulativity rule corresponding to `type.cumul` is only used in a restricted way, giving rise to canonical typing derivations.

## 4.1 Universes: Valuation vs Acyclicity

The specification of universe consistency (§ 3.2) as the existence of a valuation into natural numbers which respects the constraints on the universes does not directly give rise to a decision procedure. In Coq, the implementation of this consistency check is performed using an acyclicity check on the weighted graph induced by the constraints. We thus formalize this notion of weighted graph, the acyclicity condition, and show its equivalence with consistency defined using a valuation.

Our formalization uses finite sets, which we represent using AVL trees from the standard library.<fnref n="17" /> Given a type *A*, we write `ASet` for the type of finite sets with elements in *A*.

Our notion of weighted graph (Fig. 4) is parametrized by a type *V* of nodes (assumed fixed in this explanation, for simplicity). An edge between *x* and *y* of (possibly negative) weight *z* is represented

<footnote n="17">¹⁷https://coq.inria.fr/stdlib/Coq.MSets.MSetAVL.html</footnote>
### 3.3.1 The Bidirectional Typing Judgement.
Some rules of the bidirectional typing judgment are presented in Fig. 7. They are at the same time quite similar to the rules of §2.5 but with subtle albeit important differences, let us go through those.

First, it is an important feature of PCUIC that terms contain enough information to always infer a type—this is not true of e.g., MLTT as implemented in AGDA. In particular, our λ-abstractions are always annotated with their types. This is reflected here by the fact that each typing rule from §2.5—apart from `type_Cumul` that we will treat separately later—gives rise to a type inference rule. Rules for variables, sorts, abstractions and application should be enough to give a feel of how we adapt §2.5. We write inference $Σ ; Γ ⊢ t ▷ T$, and think of $T$ as an output, even though the relation is not a function.

None of the rules for inference, however, play the role that Rule `type_Cumul` plays in undirected typing. This is why we define, mutually with inference, other inductive judgments. Together, those rules will cover what can be achieved in undirected typing using Rule `type_Cumul`, but in a more controlled way.

The first of these judgments is checking, written $Σ ; Γ ⊢ t ▷ T$. This gives the full power of (algorithmic) cumulativity to compare the type inferred for $t$ and the type $T$, but the price to pay is that the type $T$ should be considered an input, and not an output as in inference. Thus, care is taken that this judgment is used only in places where no type has to be invented. For instance, in Rule `infer_App`, the argument can be checked against the domain that has been previously inferred for the function. More generally, checking is only used with a type known from previous hypotheses.

The last kind of judgments we call *constrained inference*, and it is itself divided into three judgments respectively for sorts, product types and inductive types. These stand between inference and checking. They are similar to inference as they output rather than take an input. But they are similar to checking as they constrain the type to have a certain shape: it should respectively be a sort, a product, or an inductive type (applied to a list of arguments). In Fig. 7 we for instance show constrained inference for products, written $Σ ; Γ ⊢ t ▷ Π$ (na,A,B), and its use in Rule `infer_App` to check whether the function inhabits a product type, and if so output a domain type used to further check the argument. Constrained inference for (co)inductive types is similarly used in destructors (pattern-matching and projections) to see whether the destructed term's type has the right shape. Finally, constrained inference for sorts is used in all places where we want to verify that a term is a type, but do not know what its universe level should be, as for instance in Rule `infer_Lambda`.

### 3.3.2 Correctness: Bidirectional Typing Implies Undirected Typing.
For the first direction of the equivalence between the two forms of typing (PCUIC: `BDToPCUIC`), a bidirectional derivation can be directly erased to an undirected one: inference rules are mapped to their undirected counterparts, and the rules for constrained inference and checking are subsumed by the more flexible `type_Cumul`.

**Theorem** `inferringTyping` $Σ Γ t T : wfΣ → wfLocalΣ Γ → Σ ; Γ ⊢ t ▷ T → Σ ; Γ ⊢ t : T$.

There is however one subtlety: the bidirectional judgment follows the information flow of the algorithm, which never re-checks inputs to be valid, as this invariant is maintained throughout the recursive calls. Thus, the bidirectional derivations lack information that is required in the undirected one. For instance, Rule `check_Cumul` in Fig. 7 does not require the target $T'$ to be a well-formed type, while Rule `type_Cumul` in §2.5 does. Similarly, Rule `infer_Rel` does not demand the context to be well formed, contrarily to Rule `type_Rel`.

Thus, the bulk of the work to prove the correctness theorem `inferringTyping` above is to derive the extra hypotheses of the undirected rules, effectively ensuring that the well-formation invariant of the algorithm is maintained. This appears in the statement, as the fact that $Σ ; Γ ⊢ t ▷ T$ implies $Σ ; Γ ⊢ t : T$ only when $Γ$ is well formed. This relies in turn on important meta-theoretical properties of
as a tuple $(x,z,y)$. Such an edge encodes the constraint $Le z$ between $x$ and $y$, i.e., the fact that the valuation should satisfy $x + z \le y$.

Then, a rooted graph $G$ is a weighted graph (whose set of edges is written $E G$) with a distinguished node $s G$ in $V$, the root of the graph. We need our weighted graphs to be rooted because a graph representing a universe hierarchy always contains $lzero$, a level smaller than all the others (apart from $tProp$ which is treated separately and not represented in the graph), and this plays a particular role as we thus know that the graph has a single connected component.

The type of edges between the two nodes $x$ and $y$ is written $EdgeOf G \times y$. And the type of paths between two nodes $x$ and $y$ is written $PathOf G \times y$. It is inductively defined and can either be the reflexive path (using $pathOf_refl$) or the concatenation of an edge in $EdgeOf \times y'$ and a path in $PathOf G y'$ (using $pathOf_step$). The notion of weight is extended to paths by simply taking the sum of the weight of each edge it is composed of.

Acyclicity of a weighted graph can then be stated as the fact that every reflexive path has a non-positive weight, i.e., we only disallow strictly positive weight cycles. This is more relaxed than asking that every reflexive path is of weight 0, because it allows for strictly negative reflexive paths, but it actually captures all valid inequations. For instance, consider the constraints $x \le y+2$ and $y+1 \le x$. These two constraints correspond to edges $(x,-2,y)$ and $(y,1,x)$, which give rise to a reflexive path of weight $-1$ on $x$, encoding the constraint $x-1 \le x$, which is perfectly valid, although useless.

Now, we turn to the formalization that the acyclicity of the graph induced by the constraints is equivalent to the existence of a valuation respecting the constraints. First, it is easy to define a notion of correct labeling of a graph (where labeling := $V \to \mathbb{N}$), which corresponds to the notion of a valuation satisfying the constraints.

**Definition correct_labeling** ($l: labeling$) :=
$$l(sG) = 0 \land \forall x ny, \text{EdgeSet.In}(x,n,y) (E G) \to l x + n \le l y.$$

We now turn to show that acyclicity is equivalent to the existence of a correct labeling. To do so, we use the notion of longest simple path between two nodes, which provides at the same time a characterization of acyclicity and a decision procedure to check acyclicity.

A simple path in $SPath s \times y$ is a path from $x$ to $y$ going only through the nodes in $s$, without visiting twice the same node, except for the last one which can appear twice (thus forming a loop).<fnref n="18" />

**Inductive** $SPath: VSet \to V \to V \to Type :=$
$$\begin{align*}
|spath_refl: V s x, SPath s x x \\
|spath_step: V s s' x y z, DisjointAdd x s s' \to EdgeOf G \times y \to SPath s y z \to SPath s' x z.
\end{align*}$$

From this notion, it is possible to compute the weight of the longest simple path (or simply *lsp*) between two nodes by taking the maximum of all possible simple paths between $x$ and $y$. The difficulty with this definition is that it is recursive, and the recursive call is done on a subset of the original set $s$ of nodes that can be visited, which is not structurally decreasing. To overcome this issue, we use the standard fuel trick, because we know that the number of necessary recursive calls is bounded by the cardinality of $s$.

<footnote n="18">¹⁸The usual notion of simple path does not allow such a repetition, but we need it to handle constraints between a level and itself.</footnote>