Consistency of the Predicative Calculus of Cumulative Inductive Construction (pCuIC)

Amin Timany and Matthieu Sozeau: Consistency of the Predicative Calculus of Cumulative Inductive Construction (pCuIC). Hosted on arXiv and HAL, October 2017.
arXiv HAL
Technical Report
Keywords: Coq, Proof Assistants, Inductive Types, Universes, Cumulativity
Abstract.

In order to avoid well-known paradoxes associated with self-referential definitions, higher-order dependent type theories stratify the theory using a countably infinite hierarchy of universes (also known as sorts), Type0 : Type1 : ···. Such type systems are called cumulative if for any type A we have that A : Typei implies A : Typei+1. The Predicative Calculus of Inductive Constructions (pCIC) which forms the basis of the Coq proof assistant, is one such system. In this paper we present the Predicative Calculus of Cumulative Inductive Constructions (pCuIC) which extends the cumulativity relation to inductive types. We discuss cumulative inductive types as present in Coq 8.7 and their application to formalization and definitional translations.

The bibtex source for this publication:
@misc{1710.03912,
 Author = {Amin Timany and Matthieu Sozeau},
 Title = {Consistency of the Predicative Calculus of Cumulative Inductive Constructions (pCuIC)},
  Year = {2017},
  Eprint = {arXiv:1710.03912},
  url = {https://arxiv.org/abs/1710.03912}
 }