package coq-trocq-hott

Trocq is a modular parametricity plugin for Coq. It can be used to achieve proof transfer by both translating a user goal into another, related, variant, and computing a proof that proves the corresponding implication.

The plugin features a hierarchy of structures on relations, whose instances are computed from registered user-defined proof via parametricity. This hierarchy ranges from structure-less relations to an original formulation of type equivalence. The resulting framework generalizes raw parametricity, univalent parametricity and CoqEAL, and includes them in a unified framework.

The plugin computes a parametricity translation "à la carte", by performing a fine-grained analysis of the requires properties for a given proof of relatedness. In particular, it is able to prove implications without resorting to full-blown type equivalence, allowing this way to perform proof transfer without necessarily pulling in the univalence axiom.

The plugin is implemented in Coq-Elpi and the code of the parametricity translation is fairly close to a pen-and-paper sequent-style presentation.