Trocq - Proof Transfer for Free, Beyond Equivalence and Univalence

Learn about Trocq, a proof transfer framework for dependent type theory that extends beyond traditional equivalence and univalence approaches in this conference talk by Cyril Cohen from Inria. Discover how this novel framework generalizes the univalent parametricity translation through a new formulation of type equivalence, enabling proof transfer while minimizing dependency on the axiom of univalence when possible. Explore how Trocq works with a broader range of relations beyond just equivalences and examine its implementation as a plugin for the Rocq interactive theorem prover using the Rocq-Elpi meta-language. Gain insights into this collaborative research with Enzo Crance and Assia Mahboubi that advances the field of formal verification and type theory by providing more flexible and efficient proof transfer mechanisms.