Equality, Quasi-Implicit Products, and Large Eliminations

TL;DR

This paper introduces a type theory with equality reflection allowing coercions based on provable equalities, develops its metatheory, and extends it to handle large eliminations through quasi-implicit products.

Contribution

It presents a novel type theory with equality reflection, unifies coercions and annotations, and extends the system to large eliminations with quasi-implicit products.

Findings

Decidable system with annotated terms justified by unannotated system

Metatheory developed for an undecidable version

Extension to large eliminations using quasi-implicit products

Abstract

This paper presents a type theory with a form of equality reflection: provable equalities can be used to coerce the type of a term. Coercions and other annotations, including implicit arguments, are dropped during reduction of terms. We develop the metatheory for an undecidable version of the system with unannotated terms. We then devise a decidable system with annotated terms, justified in terms of the unannotated system. Finally, we show how the approach can be extended to account for large eliminations, using what we call quasi-implicit products.