Friday 12 January 2024, 13:00, room 1Z76: Trocq: Proof Transfer for Free, With or Without Univalence, Enzo Crance (Gallinette, Inria Rennes, LS2N, Mitsubishi Electric), Cyril Cohen (Inria Sophia-Antipolis), Denis Cousineau (Mitsubishi Electric R&D Centre Europe)

Formalisation projects make use of a possibly broad range of different representations for a same mathematical concept. Yet, substantial manual input often remains necessary to switch from a representation to another, even though it is typically left implicit on paper. In this talk, we will present Trocq, a new proof transfer framework for dependent type theory. It is based on a generalisation of univalent parametricity, able to avoid dependency on the univalence axiom when possible, and able to exploit more relations that just equivalences. We will also present the implementation of Trocq, a plugin for the Coq proof assistant, written using the Coq-Elpi meta-language.