Reconciling Impredicative Axiom and Universe

Overview & Synopsis

Impredicativity and type theory share a long history since Russel introduced the notion of types specifically to try and rule out the logical inconsistency that can be derived from arbitrary impredicative quantification. In modern type theory, impredicativity is most commonly (re)introduced in one of two ways : the traditional way found in systems like the Calculus of Constructions, Lean, Coq, and System F, is to make the bottom universe impredicative, typically called Prop ; the other way, used in HoTT [15], is to provide a propositional resizing axiom that makes it possible to move proof-irrelevant types to a lower universe.Coq's Prop and HoTT's propositional resizing axiom both restrict the use of impredicative quantification to the definition of proof-irrelevant propositions, which suggests they may be closely related, yet the actual mechanism by which they allow it is very different, making it unclear how they compare to each other in terms of expressiveness and interactions with other axioms.In this article we try to provide an answer to this question by axiomatizing a Prop universe. More specifically, we describe a predicative type theory augmented with a set of axioms inspired by HoTT's propositional resizing axiom and then show a quasi-equivalence between this system and a similar type theory augmented with a Prop universe. We start with a small PTS and then grow the system to UTT-style inductive types.In practical terms, the syntactic nature of the proof means that such an approach can be used also to translate code between systems. Furthermore, this final result suggests that the kind of impredicativity provided by Coq's Prop universe is closely related to that offered by HoTT's propositional resizing.