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