In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. In the dependently-typed setting, however, we would like to appeal to such invariance results within a language itself, in order to transfer theorems from simple to complex implementations. Homotopy type theorists have noted that Voevodsky's univalence principle equates isomorphic structures, but unfortunately many instances of representation independence are not isomorphisms.

In this talk, we describe a technique for establishing internal relational representation independence results in Cubical Agda by using higher inductive types to simultaneously quotient two related implementation types by a heterogeneous correspondence between them. The correspondence becomes an isomorphism between the quotiented types, thereby allowing us to obtain an equality of implementations by univalence. Joint work with Evan Cavallo, Anders Mörtberg, and Max Zeuner. Available at https://dl.acm.org/doi/10.1145/3434293.