Parametricity is a property of various type theories which enables constructing relational interpretations. In dependent type theories, this interpretation may be implemented as a metaprogram, translating well-typed terms in the source language into relatedness proofs, in the same language. E.g. using binary parametricity, two types A, B : □ are related by the translation ⟦□⟧ A B := A → B → □; two functions f : A → B, g : A’ → B’ are related by the translation ⟦A → B⟧ f g if two related inputs a, a’ are taken to two related outputs f a, g a’, etc. This translation has practical applications, as it generates “theorems for free”.

Multiple implementations of parametricity are available for the Rocq proof assistant, but so far records types have been treated as second-class citizens — the record is first translated into its representing inductive, which is then translated using parametricity. The resulting inductive, however, is an indexed inductive type, so it isn’t a direct representation of any record type. I will present the necessary changes to the rocq-elpi implementation of parametricity to support first-class record types.