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

TL;DR

This paper establishes the soundness of an extended version of the pCIC, called pCuIC, which incorporates cumulativity for inductive types to improve consistency in dependent type theories.

Contribution

It introduces and proves the soundness of pCuIC, extending cumulativity to inductive types within the predicative calculus of inductive constructions.

Findings

pCuIC extends pCIC with cumulativity for inductive types

Soundness of pCuIC is formally established

Enhances the consistency of dependent type theories

Abstract

In order to avoid well-know 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), Type$_0$ : Type$_1$ : $\cdots$ . Such type systems are called cumulative if for any type $A$ we have that $A$ : Type$_{i}$ implies $A$ : Type$_{i+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 and establish the soundness of the predicative calculus of cumulative inductive constructions (pCuIC) which extends the cumulativity relation to inductive types.