Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence
摘要
Trocq [5] is both the name of a calculus, describing a parametricity framework, and of a Coq plugin [6] that provides tactics for performing representation changes in goals, as well as vernacular commands for specifying the expected translations.