# Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence

Cyril Cohen, Enzo Crance, Assia Mahboubi

► To cite this version:

Cyril Cohen, Enzo Crance, Assia Mahboubi. Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence. ACM Transactions on Programming Languages and Systems (TOPLAS), 2025, pp.1-40. 10.1145/3737283. hal-05192017

HAL Id: hal-05192017

https://inria.hal.science/hal-05192017v1

Submitted on 30 Jul 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence

CYRIL COHEN, Inria, CNRS, ENS de Lyon, Université Claude Bernard Lyon 1, LIP, UMR 5668, France
ENZO CRANCE, Nantes Université, École Centrale Nantes, CNRS, Inria, LS2N, UMR 6004, France and Mitsubishi Electric R&D Centre Europe, France

ASSIA MAHBOUBI, Nantes Université, École Centrale Nantes, CNRS, Inria, LS2N, UMR 6004, France and Vrije Universiteit Amsterdam, The Netherlands

This article presents TROCQ, a new proof transfer framework for dependent type theory. TROCQ is based on a novel formulation of type equivalence, used to generalize the univalent parametricity translation. This framework takes care of avoiding dependency on the axiom of univalence when possible, and may be used with more relations than just equivalences. We have implemented a corresponding plugin for the Rocq/Coq interactive theorem prover, in the Coq-Elpi meta-language.

CCS Concepts: • **Theory of computation** → **Type theory**.

Additional Key Words and Phrases: Parametricity, Representation independence, Univalence, Proof assistants, Proof transfer

**ACM Reference Format:**

Cyril Cohen, Enzo Crance, and Assia Mahboubi. 2025. Trocq: Proof Transfer for Free, Beyond Equivalence and Univalence. ACM Trans. Program. Lang. Syst. ?, ?, Article ? (May 2025), 40 pages. https://doi.org/10.1145/3737283

## 1 Introduction

Machine-checked mathematics provides every object and statement of the mathematical literature with explicit data structures, in a certain choice of foundational formalism. Different application domains may involve rather different natures of data structures, and therefore sharpen different styles of proof automation: for instance, mechanized semantics of programming languages typically involves inductive types with a much larger number of constructors than formalized undergraduate mathematics, while the latter typically involves much larger hierarchies of algebraic structures than the former. However despite the tremendous progress in the technology of interactive theorem proving, writing machine-checked mathematics remains as of today a quite laborious task, plagued by the need to justify numerous proof steps that are left implicit on paper.

A quite significant amount of the bureaucracy of machine-checked proofs consists in justifying that certain changes in a formal statement do not affect its provability. Building blocks of these changes might be non-trivial, such as proving the equivalence of two types, but propagating existing relations between certain types and between certain constants, often amounts to a systematic,

Authors' Contact Information: Cyril Cohen, cyril.cohen@inria.fr, Inria, CNRS, ENS de Lyon, Université Claude Bernard Lyon 1, LIP, UMR 5668, 69342, Lyon cedex 07, France; Enzo Crance, Nantes Université, École Centrale Nantes, CNRS, Inria, LS2N, UMR 6004, F-44000 Nantes, France and Mitsubishi Electric R&D Centre Europe, Rennes, France, enzo.crance@inria.fr; Assia Mahboubi, Nantes Université, École Centrale Nantes, CNRS, Inria, LS2N, UMR 6004, F-44000 Nantes, France and Vrije Universiteit Amsterdam, Amsterdam, The Netherlands, assia.mahboubi@inria.fr.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from permissions@acm.org.

© 2025 ACM.

ACM 1558-4593/2025/5-ART?

https://doi.org/10.1145/3737283
syntax-directed recombination process. Although some existing tools address specific cases of this general question, the lack of sufficiently powerful approaches for automating *proof transfer* is a trans-disciplinary formalization issue, reported by formal proof practitioners in a broad spectrum of areas, including various aspects of mechanized semantics [16, 62, 63] or discrete mathematics [3, 33].

In this paper, we focus on interactive theorem provers based on dependent type theory, such as Rocq/Coq [55, 56], Agda [46] or Lean [26]. These proof management systems are genuine functional programming languages, with full-spectrum dependent types, a context in which representation independence meta-theorems can be turned into concrete instruments for achieving program and proof transfer.

Seminal results on the contextual equivalence of distinct implementations of a same abstract interface were obtained for System F, using logical relations [44] and parametricity meta-theorems [48, 61]. In the context of type theory, such meta-theorems can be turned into syntactic translations of the type theory of interest into itself, automating this way the generation of the statement and proof of parametricity properties for type families and for programs. Such syntactic relational models can accommodate dependent types [14], inductive types [13] and scale to the Calculus of Inductive Constructions, with an impredicative sort [36].

In particular, the *univalent parametricity* translation [53] leverages the univalence axiom [57] so as to transfer statements using established equivalences of types. This approach crucially removes the need for devising an explicit common interface for the types in relation. In presence of an internalized univalence axiom and of higher-inductive types, the *structure identity principle* provides internal representations of independence results, for more general relations between types than equivalences [8]. This last approach is thus particularly relevant in cubical type theory [19, 59]. Indeed, a computational interpretation of the univalence axiom brings computational adequacy to otherwise possibly stuck terms, those defined via an axiomatized univalence principle.

Yet taming the bureaucracy of proof transfer remains hard in practice for users of Rocq/Coq, Lean or Agda: different concrete tools exist for specific classes of applications, but they are incomparable in scope, may assume excessively strong axioms, and are actually unable to address simple examples of data refinements [3] or elementary proofs about monadic data structures. These limitations are in fact of a fundamental nature, and call for a more detailed study of parametricity in dependent type theory.

*Contributions.* This paper presents three contributions:

• A parametricity framework *à la carte*, that generalizes the univalent parametricity translation [53], as well as refinements à la CoqEAL [23] and generalized rewriting [50]. Its pivotal ingredient is a variant of Altenkirch and Kaposi’s symmetrical presentation of type equivalence [5].

• A conservative subtyping extension of $CC_\omega$ [25], used to formulate an inference algorithm for this parametricity framework so as to guide the synthesis of translated terms.

• A parametricity plugin for the Rocq/Coq interactive theorem prover, which implements this parametricity framework using the Coq-Elpi [54] meta-language. This plugin rests on a library of original formal proofs, and it is distributed with a collection of application examples. It comes in two versions. The first one is built on top of the HoTT library [12] and uses the HoTT type of paths. The second one is built on top of the Rocq/Coq' standard library, and accommodates the *Prop* sort. The complete Rocq/Coq development is available at:

https://github.com/rocq-community/trocq

*Prior publications.* This article is a substantial revision of a prior conference publication [21]. The paper was reshaped and presents our work from a different angle. Section 2 is new and provides a
significantly extended gallery of detailed examples. Section 4 was extended with detailed examples as well. Section 7 expands the content of the artefact report [20] by illustrating the shape of the constraint graph and presenting the recently improved user interface for the plugin. Finally, Section 8 has been updated according to the recent changes in the plugin and to the additional examples discussed in the article. The main evolution of the code is the completion of a **Prop** compatible version of the plugin.

*Outline.* Section 2 illustrates the state of the art of proof transfer tools in type theory. We then clarify in Sections 3 and 4 the essence of internal proof transfer in type theory, and we discuss the scope and limits of univalent parametricity. In Section 5, we present an alternative definition of type equivalence, motivating a hierarchy of structures for relations preserved by parametricity. Section 6 then presents the framework behind TROCQ, as well as the synthesis of parametricity translations in this framework, before Section 7 discusses the implementation of the TROCQ plugin. Section 8, revisits and extends the introductory gallery of examples. We discuss related work in Section 9 before concluding in Section 10.

## 2 Proof transfer by example

This section discusses a collection of concrete formalization problems in Rocq/Coq, illustrating various facets of proof transfer, as well as the related formal proof bureaucracy.

A same mathematical concept most often has several equally useful, *equivalent* formal definitions, all the more so when these formal definitions are to be mechanized. This issue is specially acute when a proof involves computational steps. In this case, a machine-checked version usually involves different data structures for the deductive parts of the proof and for the computational ones, the former being well-suited to reasoning, and the latter making computations tractable. Such implementation details are usually irrelevant on paper, but machine-checked proofs need to convince the proof checker that the representation change does not matter. Because of this tension between smooth proofs and tractable computations, the standard library of the Rocq/Coq interactive theorem prover [55, 56] features two data structures for representing non-negative integers. Type $N$ is the base-1 number system and the associated elimination principle $N\_ind$ coincides with the usual recurrence scheme of Peano arithmetic:

Inductive $N$ : Type := $O_N$ : N | $S_N$ (n : N) : N.
$N\_ind$ : $\forall$ P : N $\rightarrow$ $\Box$, P $O_N$ $\rightarrow$ ($\forall$ n : N, P n $\rightarrow$ P ($S$ n)) $\rightarrow$ $\forall$ n : N, P n

On the other hand, type $N$ provides a binary representation *positive* of positive integers, as sequences of bits with a 1 digit in head position, and is thus better suited for coding (more) efficient arithmetic operations. The successor function $S_N : N \rightarrow N$ is no longer a constructor of the type, but can be implemented as a program, via an auxiliary successor function $S_{\text{pos}}$ for type *positive*.

Inductive positive : Type ::= xI : positive $\rightarrow$ positive | xO : positive $\rightarrow$ positive | xH : positive.

Inductive $N$ : Type ::= $O_N$ : N | $Npos$ : positive $\rightarrow$ $N$.

Fixpoint $S_{\text{pos}}$ ($p$ : positive) : positive ::= match $p$ with
| $xH \Rightarrow xO$ $xH$ | $xO$ $p \Rightarrow$ $xI$ $p$ | $xI$ $p \Rightarrow$ $xO$ ($S_{\text{pos}}$ $p$) end.

Definition $S_N$ (n : N) := match n with
| $Npos$ $p \Rightarrow$ $Npos$ ($S_{\text{pos}}$ $p$) | _ $\Rightarrow$ $Npos$ $xH$ end.
This successor function is useful to implement conversions $\uparrow_N : N \to N$ and $\downarrow_N : N \to N$ between the unary and binary representations. These conversion functions are in fact inverses of each other, and types $N$ and $N$ are therefore equivalent.

**Example 2.1 (Transfer of ground facts by equivalence).** Computing the product $100 \times 101 \times 102$ illustrates how inappropriate type $N$ is for representing integers, as soon as a small amount of computation is needed in a proof. By contrast, the implementation of multiplication on type $N$ is efficient enough for a small computational step.<fnref n="1" />

(* Two definition of the finite sequence [100; 101; 102], respectively on types $N$ and $N$ *)
**Definition** $l_N : \text{list } N := [100; 101; 102]$.
**Definition** $l_N : \text{list } N := [100; 101; 102]$%N.

(* Testing that $100 * 101 * 102 < (100 * 101 * 102) * (100 * 101 * 102) *)$
(* triggers a "Stack overflow" error. *)
**Fail Eval compute in Nat.ltb (fold_right mult 1 l_N) (fold_right mult 1 (l_N ++ l_N))**

(* Same test on type $N$ is instantaneous. *)
**Eval compute in N.ltb (fold_right N.mul 1%N l_N) (fold_right N.mul 1%N (l_N ++ l_N))**

Suppose that a proof requires testing that $\prod_{i \in l} i < \prod_{i \in l+1} i$, for $l$ denoting the finite sequence [100; 101; 102] and $+$, the concatenation of sequences. This ground statement, phrased as a property on type $N$, can be transferred to type $N$ using conversions $\uparrow_N$ and $\downarrow_N$, as well as the fact that multiplications and comparisons are related via:

$$ \forall x, y : \mathbb{N}, \quad \downarrow_N (x \times_N y) = (\downarrow_N x) \times_N (\downarrow_N y) \quad \forall x, y : \mathbb{N}, \quad x <_N y \Leftrightarrow \downarrow_N x <_N \downarrow_N y $$

Then, the result of the computation can be transferred back to type $N$, again using the equivalence between the two types and their related operations.

**Example 2.2 (Transfer of arbitrary properties by equivalence).** On the other hand, the structural elimination scheme for type $N$ generated by the proof assistant is actually seldom useful for reasoning about integers:

$N\_ind\_struct : \forall P : N \to \textbf{Prop}, P 0_N \to (\forall p : \text{positive}, P (Npos p)) \to \forall n : N, P n$

but the usual recurrence scheme on integers can be obtained by transferring $N\_ind$ to type $N$:

$N\_ind : \forall P : N \to \textbf{Prop}, P 0_N \to (\forall n : N, P n \to P (S_N n)) \to \forall n : N, P n$

Incidentally, $N\_ind$ can be proved from $N\_ind$ by using only the fact that $\downarrow_N$ is a left inverse of $\uparrow_N$, and the following relations between zeros and successors:

$$ \downarrow_N 0_N = 0_N \quad \text{and} \quad \forall n : \mathbb{N}, \quad \downarrow_N (S_N n) = S_N (\downarrow_N n) $$

Example 2.2 is in fact one of the motivating problems for *univalent parametricity* [52]. Assuming the univalence axiom, the associated prototype plugin is able to synthesize and prove the recurrence principle $N\_ind$ from the statement of $N\_ind$. This plugin relies on type class inference for combining registered proofs of the relations between the two types, their respective zeros and their respective successors. The older CoqEAL library [23] was specifically designed for automating refinements proofs, between proof-oriented data structures and computation oriented ones. Also based on parametricity techniques [36], it can actually synthesize the proof by round trip between type $N$ and type $N$ of Example 2.1.

<footnote n="1">¹This code for computing $(100 * 101 * 102)^2$ is arguably convoluted: this toy example is actually crafted so as to avoid being artificially saved by a lazy evaluation strategy or by parsing optimizations.</footnote>
CoqEAL actually targets a larger class of data refinements, which may involve types that are not equivalent. Automating machine-checked proofs of data refinements is actually an active topic of research. Examples from the literature include lists and AVL trees [27], pair of integers and rational numbers as pairs of coprime integers [23], rational numbers as pairs of coprime integers and arbitrary precision arithmetic (cf Ocaml's bignum) [3], etc. For the sake of conciseness, we provide below a toy, but emblematic example of refinement.

**Example 2.3 (Transfer of ground facts, beyond equivalences).** Type $Z_9$ is a dependent pair whose constructor $mk_{Z_9}$ packs an integer $n$ with a proof that $n$ is smaller than 9:

Inductive $Z_9 := mk_{Z_9} : \forall n : \mathbb{N}, n < 9 \rightarrow Z_9$.

We denote $\downarrow_{(9)} : Z_9 \rightarrow \mathbb{N}$ the first projection of the pair, which just throws away the proof component, so that for instance $\downarrow_{(9)} 0_{Z_9} = 0_{\mathbb{N}}$. We implement a reverse conversion $\uparrow_{(9)} : \mathbb{N} \rightarrow Z_9$, which mods its argument by 9 and is thus a left inverse of $\downarrow_{(9)}$:

$$ \forall x : Z_9, \quad \uparrow_{(9)} \downarrow_{(9)} x = x $$

For the sake of conciseness and when there is no ambiguity we also write $\bar{x} = \uparrow_{(9)} x$.

Note that we assume here that the proof component is irrelevant, which can be achieved either by using a boolean comparison test in the definition of type $Z_9$, or by using a proof-irrelevant sort, such as `hProp` or the recently introduced proof-irrelevant sort `SProp` [31]. Type $Z_9$ can be used as the carrier type of arithmetic modulo 9, and in this case, multiplication on type $Z_9$ is implemented by mod-ing the result of its analogue on type $\mathbb{N}$, so that for any $x y : \mathbb{N}$:

$$ 9 | x \times_{\mathbb{N}} y \iff \overline{x \times_{\mathbb{N}} y} = \overline{0} \iff \bar{x} \times_{Z_9} \bar{y} = \overline{0} $$

Proving that $9$ divides $23649 \times_{\mathbb{N}} 23703$ should easily reduce to the computational test that $23649 \times_{Z_9} 23703$ is $\overline{0}$.

The instance of mechanism involved in Example 2.3, translating type $\mathbb{N}$ into type $Z_9$ before computing, also falls in the scope of the CoqEAL library. It is indeed quite similar to that of Example 2.1, except for the observation that transferring this ground, quantifier-free statement only involves $\uparrow_{(9)}$. The CoqEAL method however suffers from annoying intrinsic limitations. In particular, it cannot deal with general dependent types, and is therefore useless for Examples 2.2 and 2.4, which involve universal quantifications.

**Example 2.4 (Transfer of arbitrary properties, beyond equivalences).** In elementary number theory, certain arithmetical properties on integers become easy to prove when they are reduced to their analogue on $Z_n$, for a well-chosen $n$. The proof of Proposition 2.5, a first step to prove Fermat's last theorem for degree 3, is an emblematic example of this technique.

**PROPOSITION 2.5.** For any nonnegative integers $x, y, z$, if $xyz$ is not divisible by 3 then $x^3 + y^3 \neq z^3$.

**PROOF.** We need to show that $\forall x, y, z \in \mathbb{N}, 3 + xyz \implies x^3 + \mathbb{N} y^3 \neq z^3$. By reduction modulo 9, it suffices to show $\forall x, y, z \in Z_9, 3 + xyz \implies x^3 + Z_9 y^3 \neq z^3$. We conclude by computing the truth value of the statement for each value of $(x, y, z) \in Z_9^3$. $\square$

This proof thus essentially proceeds in two steps: a transfer step to change $\mathbb{N}$ with $Z_9$, and a computational one to compute truth values on a small finite domain. Reusing the notations from Example 2.3, the transfer step essentially consists in propagating conversions $\downarrow_{(9)}$ and $\uparrow_{(9)}$, and in using the relations between the respective addition, multiplication and divisibility by 3, on types $Z_9$ and $\mathbb{N}$.
The current state of affairs is actually quite unsatisfactory. In fact, we are not aware of any tool able to automate the reduction modulo 9 of Example 2.4, in any interactive prover based on dependent type theory, and this despite the similar nature of the bureaucracy involved this example and in the previous ones in this section. Also, none of the implemented frameworks mentioned so far can treat simultaneously all of Example 2.1, Example 2.2 and Example 2.3. Indeed, CoqEAL is useless on Example 2.2, because it is inherently unable to deal with its quantifiers, but univalent parametricity cannot deal with Example 2.3, because it is inherently geared for type equivalences. Finally, up to our knowledge, all the existing methods from the literature for automating Example 2.2, such as univalent parametricity or the structure identity principle [8], pull in the univalence principle in the proof, although it can be obtained by hand by very elementary means.

Unneeded dependencies on the univalence axiom is especially unsatisfactory for developers of libraries formalizing classical mathematics, and notably Lean's mathlib or Rocq/Coq's mathcomp-analysis. These libraries indeed typically assume a strong form of proof irrelevance, which is incompatible with univalence, and thus with univalent parametricity.

In short, existing techniques for transferring results from one type to another, e.g., from $\mathbb{N}$ to $\mathbb{N}$ or from $\mathbb{N}$ to $\mathbb{Z}_\omega$, are either not suitable for dependent types, or too coarse to track the exact amount of data needed in a given proof, and not more. Section 3 provides a more formal analysis of this assessment.

# 3 Strengths and limits of univalent parametricity

We first clarify the essence of proof transfer in dependent type theory (§ 3.1) and briefly recall a few concepts related to type equivalence and univalence (§ 3.2). We then review and discuss the limits of univalent parametricity (§ 3.3).

## 3.1 Proof transfer in type theory

We recall the syntax of the Calculus of Constructions, $CC_\omega$, a $\lambda$-calculus with dependent function types and a predicative hierarchy of universes, denoted $\square_i$:

$$ \mathcal{T}_{CC_\omega} \ni A, B, t, u ::= \square_i | x | t u | \lambda x : A. M \mid \Pi x : A. B $$

We omit the typing rules of the calculus, and refer the reader to standard references (e.g., [45, 47]). We also use the standard equality type, called propositional equality, as well as dependent pairs, denoted $\Sigma x : A. B$. We write $t \equiv u$ for the definitional equality between two terms $t$ and $u$. Interactive theorem provers like Rocq/Coq, Agda and Lean are based on various extensions of this core, notably with inductive types or with an impredicative sort. When the universe level does not matter, we casually remove the annotation and use notation $\square$. Contexts of $CC_\omega$, denoted $C_{CC_\omega}$, are association lists of variables and types: $C_{CC_\omega} \ni \Gamma ::= \langle \rangle \mid \Gamma, x : A$.

In this context, proof transfer from type $S$ to type $T$ roughly amounts to synthesizing a new type former $W : T \to \square$, i.e., a type parametric in some type $T$, from an initial type former $V : S \to \square$, i.e., a type parametric in some type $S$, so as to ensure that for some given relations $R_T : S \to T \to \square$ and $R_\square : \square \to \square \to \square$, there is a proof $w$ that:

$$ \Gamma \vdash w : \forall (s : S)(t : T), R_T s t \to R_\square(V s)(W t) $$

for a suitable context $\Gamma \in C_{CC_\omega}$. This setting generalizes as expected to $k$-ary type formers, and to more pairs of related types. In practice, relation $R_\square$ is often a right-to-left arrow, i.e., $R_\square A B \triangleq B \to A$, as in this case the proof $w$ substantiates a proof step turning a goal clause $\Gamma \vdash V s$ into $\Gamma \vdash W t$.

Phrased as such, this synthesis problem is arguably quite loosely specified. Consider for instance the transfer problem discussed in Example 2.2. A first possible formalization involves the design of
an appropriate common interface structure for types $\mathbb{N}$ and $\mathbb{N}$, for instance by setting both $S$ and $T$ as $\Sigma N : \square.N \times (N \to N)$, and both $V$ and $W$ as: $\lambda X : S. \Pi P : X.1 \to \square.P X.2 \to (\Pi n : X.1. P n \to P (X.3 n)) \to \Pi n : X.1. P n$, where $X.i$ denotes the $i$-th item in the dependent tuple $X$. In this case, relation $R_T$ may characterize isomorphic instances of the structure. Such instances of proof transfer are elegantly addressed in cubical type theories via internal representation independence results [8]. In the context of $CC_\omega$, the hassle of devising explicit structures by hand has been termed the *anticipation* problem [53].

Another option is to consider two different types $S_1 \triangleq \mathbb{N} \times (\mathbb{N} \to \mathbb{N})$ and $T_1 \triangleq \mathbb{N} \times (\mathbb{N} \to \mathbb{N})$ and the following type formers $V_1$ and $W_1$:

$$V_1 \triangleq \lambda X : S_1. \forall P : \mathbb{N} \to \square. P X.1 \to (\forall n : \mathbb{N}, P n \to P(X.2 n)) \to \forall n : \mathbb{N}, P n$$

$$W_1 \triangleq \lambda X : T_1. \forall P : \mathbb{N} \to \square. P X.1 \to (\forall n : \mathbb{N}, P n \to P(X.2 n)) \to \forall n : \mathbb{N}, P n$$

where $X.1$ (resp. $X.2$) denotes the first (resp. second) projection of the pair $X$. In this case, one would typically expect $R_T$ to be a type equivalence between $S_1$ and $T_1$, so as to transport $(V_1 s)$ to $(W_1 t)$, along this equivalence.

Note that some solutions of given instances of proof transfer problems are in fact too trivial to be of interest. Consider for example the case of a *functional relation* between two types $S_2$ and $T_2$, with $R_T s t$ defined as $s = \phi t$, for some $\phi : T_2 \to S_2$. In this case, the composition $V \circ \phi$ is an obvious candidate for $W$, but is often uninformative. Indeed, this composition can only propagate structural arguments, blind to the additional mathematical proofs of program equivalences potentially available in the context. For instance, here is a useless variant of $W$:

$$W_2 \triangleq \lambda X : T_1. \forall P : \mathbb{N} \to \square. P (\uparrow_{\mathbb{N}} X.1) \to (\forall n : \mathbb{N}, P n \to P (\uparrow_{\mathbb{N}} (X.2 (\downarrow_{\mathbb{N}} n)))) \to \forall n : \mathbb{N}, P n.$$

Automation devices dedicated to proof transfer thus typically consist of a meta-program which attempts to compute type former $W$ and proof $w$ by induction on the structure of $V$, by composing registered pairs of related terms, and the corresponding proofs. These tools differ by the nature of relations they can accommodate, and by the class of type formers they are able to synthesize. For instance, *generalized rewriting* [50], which provides essential support to formalizations based on setoids [10], addresses the case of homogeneous (and reflexive) relations, i.e., when $S$ and $T$ coincide. The CoqEAL library [23] provides another example of such transfer automation tool, geared towards *refinements*, typically from a proof-oriented data-structure to a computation-oriented one. It is thus specialized to heterogeneous, functional relations but restricted to closed, quantifier-free type formers. We now discuss the few transfer methods which can accommodate dependent types and heterogeneous relations.

## 3.2 Type equivalences, univalence

Let us first focus on the special case of types related by an *equivalence*, and start with a few standard definitions, notations and lemmas. Omitted details can be found in the usual references, like the *Homotopy Type Theory* book [57]. Two functions $f, g : A \to B$ are *point-wise equal*, denoted $f \doteq g$ when their values coincide on all arguments, that is $f \doteq g \triangleq \Pi a : A. f a = g a$. For any type $A$, $id_A$ denotes $\lambda a : A. a$, the identity function on $A$, and we write $id$ when the implicit type $A$ is not ambiguous.

**Definition 3.1 (Type isomorphism, type equivalence).** A function $f : A \to B$ is an *isomorphism*, denoted $\text{lslso}(f)$, if there exists a function $g : B \to A$ which satisfies the section and retraction properties, i.e., $g$ is respectively a point-wise left and right inverse of $f$. A function $f$ is an *equivalence*,
denoted $IsEquiv(f)$, when it moreover enjoys a coherence property, relating the proofs of the section and retraction properties and ensuring that $IsEquiv(f)$ is proof-irrelevant.

Types A and B are equivalent, denoted $A \simeq B$, when there is an equivalence $f: A \to B$:

$$A \simeq B \quad \doteq \quad \Sigma f : A \to B. \text{IsEquiv}(f)$$

**LEMMA 3.2.** *Any isomorphism $f: A \to B$ is also an equivalence.*

The data of an equivalence $e: A \simeq B$ thus include two transport functions, denoted respectively $\uparrow_e: A \to B$ and $\downarrow_e: B \to A$. They can be used for proof transfer from A to B, using $\uparrow_e$ at covariant occurrences, and $\downarrow_e$ at contravariant ones. The univalence principle asserts that equivalent types are interchangeable, in the sense that all universes are univalent.

**Definition 3.3 (Univalent universe).** A universe $\mathcal{U}$ is univalent if for any two types A and B in $\mathcal{U}$, the canonical map $A = B \to A \simeq B$ is an equivalence.

In variants of $CC_\omega$, the univalence axiom has no explicit computational content: it just postulates that all universes $\square_i$ are univalent, as for instance in the HoTT library for the Rocq/Coq interactive theorem prover [12]. Some more recent variants of dependent type theory [7, 19] feature a built-in computational univalence principle. They are used to implement experimental interactive theorem provers, such as Cubical Agda [59]. In both cases, the univalence principle provides a powerful proof transfer principle from $\square$ to $\square$, as for any two types A and B such that $A \simeq B$, and any $P: \square \to \square$, we can obtain that $PA \simeq PB$ as a direct corollary of univalence. Concretely, $PB$ is obtained from $PA$ by appropriately allocating the transfer functions provided by the equivalence data, a transfer process typically useful in the context of proof engineering [49].

Going back to our example from § 3.1, transferring along an equivalence $\mathcal{N} \simeq \mathcal{N}$ thus produces $W_2$ from $V_1$. Assuming univalence, one may achieve the more informative transport from $V_1$ to $W_1$, using univalent parametricity [53], which we briefly recall in the next section.

## 3.3 Parametricity translations

Univalent parametricity strengthens the transfer principle provided by the univalence axiom by combining it with parametricity. In $CC_\omega$, the essence of parametricity, which is to devise a relational interpretation of types, can be turned into an actual syntactic translation, as relations can themselves be modeled as $\lambda$-terms in $CC_\omega$. The seminal work of Bernardy, Lasson et al. [13, 14, 36] combine in what we refer to as the raw parametricity translation, which essentially defines inductively a logical relation $\llbracket T \rrbracket$ for any type $T$, as described on Figure 1. This presentation uses the standard convention that $t'$ is the term obtained from a term $t$ by replacing every variable $x$ in $t$ with a fresh variable $x'$. A variable $x$ is translated into a variable $x_R$, where $x_R$ is a fresh name. Parametricity follows from the associated fundamental theorem, also called abstraction theorem [48]:

**THEOREM 3.4.** *If $\Gamma \vdash t : T$ holds then $\llbracket \Gamma \rrbracket \vdash t : T$, $\llbracket \Gamma \rrbracket \vdash t' : T'$ and $\llbracket \Gamma \rrbracket \vdash \llbracket t \rrbracket : \llbracket T \rrbracket$ t $t'$ hold.*

**PROOF.** By structural induction on the typing judgment, see for instance [36]. □

A key, albeit mundane ingredient of Theorem 3.4 is the fact that the rules of Figure 1 ensure that:

$$\vdash \llbracket \square_i \rrbracket : \llbracket \square_{i+1} \rrbracket \square_i \square_i \qquad (8)$$

This translation generates precisely the statements expected from a parametric type family or program. For instance, the translation of a $\Pi$-type, given by Equation 7, is a type of relations on functions that relate those producing related outputs from related inputs. Concrete implementations of this translation are available [36, 54]; they generate and prove parametricity properties for type families or for constants, improved induction schemes, etc.
• Context translation:

$$ [[ \langle \rangle ]] = \langle \rangle \qquad (1) $$

$$ [[\Gamma, x : A]] = [[\Gamma]], x : A, x' : A', x_R : [[A]] x x' \qquad (2) $$

• Term translation:

$$ [[ \Box_i ]] = \lambda A B . A \to B \to \Box_i \qquad (3) $$

$$ [[x]] = x_R \qquad (4) $$

$$ [[t u]] = [[t]] u u' [[u]] \qquad (5) $$

$$ [[\lambda x : A . t]] = \lambda(x : A)(x' : A')(x_R : [[A]] x x'). [[t]] \qquad (6) $$

$$ [[\Pi x : A . B]] = \lambda f f' . \Pi(x : A)(x' : A')(x_R : [[A]] x x'). [[B]](f x)(f' x') \qquad (7) $$

<caption>Fig. 1. Raw parametricity translation for $CC_\omega$.</caption>

Univalent parametricity. follows from the observation that the abstraction theorem still holds when restricting to relations that are in fact (heterogeneous) equivalences. This however requires some care in the translation of universes: the univalent parametricity translation of a universe of level i is the term denoted ⋄i and defined as:

$$ [[ \Box_i ]]_u \triangleq \Box_i \triangleq \lambda A B . \Sigma(R : A \to B \to \Box_i)(e : A \simeq B) . \Pi(a : A)(b : B) . R a b \simeq (a = \downarrow_e b) \qquad (9) $$

where [[·]]_u now refers to the univalent parametricity translation. For any two types A and B, [[□_i]]_u A B is a triple that packages a relation R, an equivalence e and a proof that R is equivalent to the functional relation associated with ↓_e. In fact, the following theorem holds [53]:

**THEOREM 3.5.** *Assuming the univalence axiom, [[□_i]]_u is equivalent to type equivalence, that is, for any two types A and B:*

$$ \Box_i A B \simeq (A \simeq B). $$

This observation is actually an instance of a more general technique for constructing syntactic models of type theory [18], based on attaching extra intensional specifications to negative type constructors. In these models, a standard way to recover the abstraction theorem consists in refining the translation into two variants, for any term T : □i, that is also a type. The translation of such a T as a term, denoted [T], is a dependent triple, which equips a relation with the additional data prescribed by the interpretation [[□_i]]_u of the universe. The translation [[T]]_u of T as a type is the relation itself, that is, the first projection of the dependent triple [T] onto its first component, denoted rel([T]). The second component of the triple is an equivalence, and the third one is a coherence data between the first and the second one. For the sake of convenience, Figure 2 recalls the definition of the univalent parametricity translation, as provided in its original presentation [53, Figure 4]. Our figure uses similar notations as the original presentation, in particular, dependent triples are denoted as (; ;), id_{□i} is the identity equivalence on universe □i and Equiv_Π constructs an equivalence between types Πx : A.B and Πx : A'.B' from its arguments. Observe that one recovers the raw parametricity translation by projecting every triple onto its relation, except in the case of □i where there relation part is fundamentally different. The crux of this translation lies in the construction of terms univ_{□i} and univ_Π, which provide the coherence data needed to construct the triple translating a universe and a Π type, respectively.

Theorem 3.6 states the abstraction theorem of the univalent parametricity translation [53], where ⊢_u denotes a typing judgment of $CC_\omega$ assuming univalence:
* Context translation:

$$ [[ \langle \cdot \rangle ] ]_u = \langle \cdot \rangle \qquad (10) $$

$$ [[ \Gamma, x : A ] ]_u = [[ \Gamma ] ]_u, x : A, x' : A', x_R : [[ A ] ]_u x x' \qquad (11) $$

* Term translation:

$$ [ \Box_i ] = p_{\Box_i} \qquad (12) $$

$$ [ x ] = x_R \qquad (13) $$

$$ [ t u ] = [ t ] u u' [ u ] \qquad (14) $$

$$ [ \lambda x : A. t ] = \lambda (x : A)(x' : A')(x_R : [[ A ] ]_u x x'). [ t ] \qquad (15) $$

$$ [ \Pi x : A. B ] = p_{\Pi} [ A ] [ B ] \qquad (16) $$

* Type translation:

$$ [[ A ] ]_u = \text{rel}([ A ]) $$

* With:

$$ p_{\Box_i} = (\Box_i; id_{\Box_i}; \text{univ}_{\Box_i}) $$

$$ \begin{align*} p_{\Pi} A_R B_R &= (\lambda f f'. \Pi(x:A)(x':A')(x_R:\text{rel}(A_R)x x'). \text{rel}(B_R)(f x)(f' x')); \\ \text{Equiv}_{\Pi} A_R B_R; \text{univ}_{\Pi} A_R B_R \end{align*} $$

omitting implicit arguments.

<caption>Fig. 2. Univalent parametricity translation for $CC_\omega$.</caption>

**THEOREM 3.6.** If $\Gamma \vdash t : T$ then $[[\Gamma]]_u \vdash_t [t] : [[T]]_u t t'$.

Note that proving this theorem involves in particular ensuring that:

$$ \vdash_t [ \Box_i ] : [[ \Box_{i+1} ] ]_u \Box_i \Box_i \quad \text{and} \quad \text{rel}([ \Box_i ]) \equiv [[ \Box_i ] ]_u \qquad (17) $$

The univalence axiom makes this possible by allowing to define

$$ \vdash_t \text{univ}_{\Box_i} : \Pi A B : \Box_i. \Box_i A B \approx (A = B) $$

$$ \vdash_t \text{univ}_{\Pi} A_R B_R : \Pi(f : \Pi x : A. B)(f : \Pi x : A'. B'). $$

$$ \begin{align*} & (\Pi(x:A)(x':A')(x_R:\text{rel}(A_R)x x').\text{rel}(B_R)(f x)(f'x')) \\ & \approx (f = \text{\textcolor{red}{\textit{\textit{\textit{\textit{\textit{\textit{\textit{\textit{\textit{Equiv}}}}}}}}\textit{\textit{\textit{\textit{A}}}}\textit{\textit{\textit{R}}}}\textit{\textit{\textit{B}}}}\textit{\textit{g}})). \end{align*} $$

Indeed, assuming the univalence axiom, $\text{univ}_{\Box_i}$ is a corollary of Theorem 3.5, and the definition of term $\text{univ}_{\Pi}$ follows from dependent functional extensionality, which is also a consequence of the univalence axiom. Importantly, this univalent parametricity translation can be seamlessly extended so as to also make use of a global context of user-defined equivalences.

However, because of the interpretation of universes given by Equation 9, univalent parametricity can only automate proof transfer based on type equivalences. This is too strong a requirement in many cases, e.g., to deduce properties of natural numbers from that of integers, or more generally for refinement relations. Moreover, the definition of terms $\text{univ}_{\Box_i}$ and $\text{univ}_{\Pi}$ crucially rely on the univalence principle. Therefore, an execution of the translation which involves cases 12 and 16 may incur unnecessary dependencies on the univalence axiom in the propagation of type equivalences. This problem is illustrated in Example 2.2.
# 4 An operational view on parametricity translations

We propose here a sequent style presentation of translations, which fits closely the type system of $CC_\omega$, while explaining in a consistent way the transformations of terms $T_{CC_\omega}$ and contexts $C_{CC_\omega}$. This choice of presentation departs from the standard literature about parametricity in pure type systems. Yet, it brings the presentation closer to actual implementations, whose necessary management of parametricity contexts is swept under the rug by notational conventions (e.g., the primes of Section 3.3).

## 4.1 Raw parametricity sequents

We introduce parametricity contexts $\mathcal{R}_{CC_\omega}$, under the form of a list of triples packaging two variables $x$ and $x'$ together with a third one $x_R$. The latter $x_R$ is a witness (a proof) that $x$ and $x'$ are related:

$$ \mathcal{R}_{CC_\omega} \ni \Xi ::= \langle \rangle \mid \Xi, x \sim x' \colied x_R $$

We write $(x, x', x_R) \in \Xi$ when $\Xi = \Xi', x \sim x' \colied x_R, \Xi''$ for some $\Xi'$ and $\Xi''$.

We denote $\text{Var}(\Xi)$ the sequence of variables related in a parametricity context $\Xi$, with multiplicities:

$$ \text{Var}(\langle \rangle) = \langle \rangle \quad \text{Var}(\Xi, x \sim x' \colied x_R) = \text{Var}(\Xi), x, x', x_R. $$

A parametricity context $\Xi$ is well-formed, written $\Xi \vdash$, if the sequence $\text{Var}(\Xi)$ is duplicate-free. In this case, we use the notation $\Xi(x) = (x', x_R)$ as a synonym of $(x, x', x_R) \in \Xi$.

A parametricity judgment relates a parametricity context $\Xi$ and three terms $t, t', t_R$ of $CC_\omega$. Parametricity judgments, denoted as:

$$ \Xi \vdash t \sim t' \colied t_R, $$

are defined by rules of Figure 3 and read in context $\Xi$, term $t$ translates to the term $t'$, because $t_R$.

$$
\begin{array}{c}
\begin{array}{c}
\begin{array}{c}
\Xi \vdash \Box_i \sim \Box_i \colied \lambda(AB \colied \Box_i). A \to B \colied \Box_i & \text{(PARAMSORT)} & (x, x', x_R) \in \Xi \quad \Xi \vdash \\
\frac{\Xi \vdash t \sim t' \colied t_R}{\Xi \vdash t u \sim t' u' \colied t_R u u' u_R} & \text{(PARAMAPP)} & (\text{PARAMVAR})
\end{array} \\
\begin{array}{c}
\frac{x, x' \notin \text{Var}(\Xi)}{\Xi \vdash A \sim A' \colied A_R} \quad \Xi, x \sim x' \colied x_R \vdash t \sim t' \colied t_R} & \text{(PARAMLAM)} & (\text{PARAMLAM}) \\
\frac{x, x' \notin \text{Var}(\Xi)}{\Xi \vdash A \sim A' \colied A_R} \quad \Xi, x \sim x' \colied x_R \vdash B \sim B' \colied B_R} & \text{(PARAMPI)} & (\text{PARAMPI})
\end{array} \\
\begin{array}{c}
\frac{x, x' \notin \text{Var}(\Xi)}{\Xi \vdash \Pi x : A. B \sim \Pi x' : A'. B' \colied \lambda f. \Pi x x' x_R. B_R (f x) (g x')} & \text{(PARAMPI)} & (\text{PARAMPI})
\end{array}
\end{array}
$$

<caption>Fig. 3. PARAM: sequent-style binary parametricity translation</caption>

**LEMMA 4.1.** *The relation associating a term $t$ with pairs $(t', t_R)$ such that $\Xi \vdash t \sim t' \colied t_R$ holds, with $\Xi$ a well-formed parametricity context, is functional. More precisely, for any well-formed parametricity*
context $\Xi$:

$$ \forall t, t', u', t_R, u_R, \Xi \vdash t \sim t' \coloneqq t_R \wedge \Xi \vdash t \sim u' \coloneqq u_R \\ \implies (t', t_R) = (u', u_R) $$

PROOF. Immediate by induction on the syntax of $t$. □

This presentation of parametricity thus provides an alternative definition of translation [·] from Figure 1, and accounts for the prime-based notational convention used in the latter.

**Definition 4.2.** A parametricity context $\Xi$ is *admissible* for a well-formed typing context $\Gamma$, denoted $\Gamma \triangleright \Xi$, when $\Xi$ is well-formed as a parametricity context and $\Gamma$ provides coherent type annotations for all terms in $\Xi$, that is,

$$ \overline{\langle \rangle \triangleright \langle \rangle}^{\Gamma \triangleright \Xi} \qquad \frac{\Gamma \triangleright \Xi}{(\Gamma, x : A, x' : A', x_R : A_R, x x') \triangleright (\Xi, x \sim x' \coloneqq x_R)}^{\triangleright, \cdot} $$

We can now state and prove an abstraction theorem:

**THEOREM 4.3 (ABSTRACTION THEOREM).**

$$ \frac{\Gamma \triangleright \Xi \qquad \Gamma \vdash t : A \qquad \Xi \vdash t \sim t' \coloneqq t_R \qquad \Xi \vdash A \sim A' \coloneqq A_R}{\Gamma \vdash t' : A' \qquad \text{and} \qquad \Gamma \vdash t_R : A_R, t t'} $$

PROOF. By induction on the derivation of $\Xi \vdash t \sim t' \coloneqq t_R$. □

**Constants.** Postulating arbitrary axioms, stating the existence of parametricity translations for some constants, easily break the abstraction theorem. We refer to Tabareau et al. [53] for a discussion about the unfortunate interaction of conversion and elimination rules for the types $\mathbb{N}$ and $\mathbb{N}$ of Example 2.1. Giving up on $\delta$-expansion, it is however possible to extend the translation to inert, opaque constants in the following way. Given:

* a set $C$ of symbols;

* for each $c \in C$, a term $T_c \in \mathcal{T}_{CC_\omega}$, such that $\vdash T_c : \Box$;

* a partial translation function $\xi : C \to C^2$ such that for all $c, c'$ and $c_R$ with $\xi(c) = (c', c_R)$, we have

$$ \vdash T_c \sim T_{c'} \coloneqq T_{c_R} \text{ and } \vdash c_R : T_{c_R}, c c' $$

the rules of Figure 4 shall respectively extend those of $CC_\omega$ and of $PARAM$.

$$ \frac{c \in C}{\vdash c : T_c} \qquad \frac{c \in C}{\vdash c \sim c' \coloneqq c_R} \qquad (\text{PARAMCONST}) $$

<caption>Fig. 4. Extension of $CC_\omega$ and its raw parametricity translation with constants.</caption>

The abstraction theorem still holds, as the case of neutral constants can be treated exactly as that of variables.
We now show how to use raw parametricity to deal with Example 2.1. For the sake of conciseness, we provide only the translation of one side of the inequality. Reusing notations from Section 1, we pose

$$N_R m n \triangleq (\downarrow_N m = n)$$

and we have $1_R : N_R \ 1 \% N$, $100_R : N_R \ 100 \ 100\% N$, $101_R : N_R \ 101 \ 101\% N$, and $102_R : N_R \ 102 \ 102\% N$, which can all be obtained by computation within Rocq/Coq. We furthermore assume a proof

$$\mathrm{mult}_R : \forall m_1 n_1, N_R m_1 n_1 \implies \forall m_2 n_2, N_R m_2 n_2 \implies N_R (m_1 \times_N m_2) (n_1 \times_N n_2)$$

which can be read as a proof of multiplicative morphism between $N$ and $\mathbb{N}$.

Let us represent the trace of the execution of the logic program computing the translation $\mathrm{fold\_right} \ N \ \mathrm{mult} \ 1 \ l_N \sim t' \vdots t_R$, which synthesizes both $t'$ and $t_R$, through a top-down derivation tree. We write rules in the reverse order compared to the presentation of the calculus from Figure 1. Since the tree would widen out of the page, we use dashed-boxes to delimit non-leaf subtrees of the derivation.

<figure><img src="image_2.png" /></figure>

Finally, by the abstraction theorem, we get that $\mathrm{fold\_right}_R N_R \mathrm{mult}_R 1_R$ is a proof of the following: $N_R (\mathrm{fold\_right} N \ N \ \mathrm{mult} \ 1 \ l_N) (\mathrm{fold\_right} N \ N \ \mathrm{mult} \ 1\% N \ l_N)$, which by definition of $N_R$, means $\downarrow_N (\mathrm{fold\_right} N \ N \ \mathrm{mult} \ 1 \ l_N) = \mathrm{fold\_right} N \ N \ \mathrm{mul} \ 1\% N \ l_N$. This works well enough for closed statements about values in a given datatype, such as $N$ or $\mathbf{bool}$, but falls short of scaling to $CC_\omega$.

## 4.2 Univalent parametricity sequents

We now propose in Figure 5 a rephrased version of the univalent parametricity translation defined on Figure 2, using the same sequent style. Its parametricity judgments are denoted:

$$\Xi \vdash_u t \sim t' \vdots t_R$$

where $\Xi$ is a parametricity context and $t, t'$, and $t_R$ are terms of $CC_\omega$. The $u$ index is a reminder that typing judgments $\Gamma \vdash_u M : A$ involved in the associated abstraction theorem assume the univalence axiom.

We can now rephrase the abstraction theorem for univalent parametricity.

**THEOREM 4.4 (UNIVALENT ABSTRACTION THEOREM).**

$$\frac{\Gamma \vdash \Xi \qquad \Gamma \vdash t : A \qquad \Xi \vdash_u t \sim t' \vdots t_R \qquad \Xi \vdash_u A \sim A' \vdots A_R \\ \qquad \Gamma \vdash t' : A' \qquad \text{and} \qquad \Xi \vdash_u t_R : \mathrm{rel}(A_R) t t'}$$
$$ \frac{\Xi \vdash_u \Box_i \sim \Box_i \vdash p_{\Box_i}}{\Xi \vdash_u \Box_i \sim \Box_i} \quad (\text{UPARAMSORT}) \qquad \frac{(x, x', x_R) \in \Xi \quad \Xi \vdash}{\Xi \vdash_u x \sim x' \vdash x_R} \quad (\text{UPARAMVAR}) $$

$$ \frac{\Xi \vdash_u t \sim t' \vdash t_R \quad \Xi \vdash_u u \sim u' \vdash u_R}{\Xi \vdash_u t u \sim t' u' \vdash t_R u u' u_R} \quad (\text{UPARAMAPP}) $$

$$ \frac{x, x' \notin \text{Var}(\Xi)}{\Xi \vdash_u A \sim A' \vdash A_R \quad \Xi, x \sim x' \vdash x_R \vdash_u t \sim t' \vdash t_R} \quad (\text{UPARAMLAM}) $$

$$ \frac{x, x' \notin \text{Var}(\Xi)}{\Xi \vdash_u A \sim A' \vdash A_R \quad \Xi, x \sim x' \vdash x_R \vdash_u B \sim B' \vdash B_R} \quad (\text{UPARAMPI}) $$

<caption>Fig. 5. UPARAM: univalent parametricity rules</caption>

PROOF. By induction on the derivation of $\Xi \vdash_u t \sim t' \vdash t_R$. □

Remark 4.5. In Theorem 4.4, rel($A_R$) is a term of type $A \to A' \to \Box$. Indeed:

$$ \frac{\Gamma \vdash_u A : \Box_i \quad \Xi \vdash_u A \sim A' \vdash A_R \quad \Gamma \vdash \Xi}{\Gamma \vdash_u A_R : \text{rel}(p_{\Box_i}) A A'} $$

entails $A_R$ has type

$$ \begin{aligned} \text{rel}(p_{\Box_i}) A A' &\equiv \text{\textcircled{1}} A A' \\ &\triangleq \Sigma(R : A \to B \to \Box_i)(e : A \simeq B) \cdot \Pi(a : A)(b : B) \cdot R a b \simeq (a = \downarrow_e b). \end{aligned} $$

*Constants*. Like in the case of raw parametricity, the univalent parametricity translation can be extended with neutral, opaque constants in the following way. Given,

* a set $C$ of symbols;

* for each $c \in C$, a term $T_c \in \mathcal{T}_{CC_\omega}$, such that $\vdash_u T_c : \Box$;

* a partial translation function $\xi : C \to C^2$ such that for all $c, c'$ and $c_R$ with $\xi(c) = (c', c_R)$, we have

$$ \vdash_u T_c \sim T_{c'} \vdash T_{c_R} \text{ and } \vdash_u c_R : \text{rel}(T_{c_R}) c c' $$

the rules of Figure 6 shall respectively extend those of $CC_\omega$ and UPARAM.

$$ \frac{c \in C}{\vdash_u c : T_c} \quad (\text{CONST}) \qquad \frac{c \in C \quad \xi(c) = (c', c_R)}{\vdash_u c \sim c' \vdash c_R} \quad (\text{UPARAMCONST}) $$

<caption>Fig. 6. Additional constant rules for raw parametricity</caption>

The abstraction theorem still holds, as the case of neutral constants can be treated exactly as that of variables.
We show how to use univalent parametricity to deal with Example 2.2. We introduce abbreviations for the types of the induction principles $indty_N := \forall P : N \to \square, P O_N \to rec_N P \to \forall n : N, P n$ and $indty_N := \forall P : N \to \square, P O_N \to rec_N P \to \forall n : N, P n$ where $rec_N P := \forall n : N, P n \to P (S_N n)$ and $rec_N P := \forall n : N, P n \to P (S_N n)$ for the sake of conciseness.

$$ \vdash_u indty_N \sim indty_N \vdash \omega_1 $$

$$ \vdash_u N \to \square \sim N \to \square \vdash p_{\Pi} N_R p_{\square} $$

$$ \vdash_u N \sim N \vdash N_R \vdash_u \square \sim \square \vdash p_{\square} $$

$$ P \sim P' \vdots P_R \vdash_u P O_N \to rec_N P \to \forall n : N, P n \sim P O_N \to rec_N P \to \forall n : N, P n \vdots \omega_2 $$

$$ P \sim P' \vdots P_R \vdash_u P O_N \sim P O_N \vdots P_R \emptyset_R $$

$$ P \sim P' \vdots P_R \vdash_u P \sim P' \vdots P_R \vdash_u \emptyset_N \sim \emptyset_N \vdots \emptyset_R $$

$$ P \sim P' \vdots P_R \vdash_u rec_N P \to \forall n : N, P n \sim rec_N P \to \forall n : N, P n \vdots \omega_3 $$

$$ P \sim P' \vdots P_R \vdash_u rec_N P \sim rec_N P \vdots \omega_4 $$

$\vdots$

$$ P \sim P' \vdots P_R \vdash_u \forall n : N, P n \sim \forall n : N, P n \vdots p_{\Pi} N_R (P_R n_R) $$

$$ \vdash_u N \sim N \vdash N_R \vdash_u \vdots $$

$$ P \sim P' \vdots P_R, n \sim n' \vdots n_R \vdash_u P n \sim P n \vdots P_R n_R $$

$$ P \sim P' \vdots P_R, n \sim n' \vdots n_R \vdash_u P \sim P' \vdots P_R $$

$$ P \sim P' \vdots P_R, n \sim n' \vdots n_R \vdash_u n \sim n' \vdots n_R $$

where

$$ \omega_1 = p_{\Pi} (p_{\Pi} N_R p_{\square}) \omega_2 $$

$$ \omega_2 = p_{\Pi} (P_R \emptyset_R) \omega_3 $$

$$ \omega_3 = p_{\Pi} \omega_4 (p_{\Pi} N_R (P_R n_R)) $$

$\omega_4$ is the result of the omitted subtree

By the abstraction theorem, $\omega_1$ eventually has type

$$ \forall P : N \to \square, P O_N \to rec_N P \to \forall n : N, P n \quad (\forall P : N \to \square, P O_N \to rec_N P \to \forall n : N, P n) $$

Which means the two terms are equivalent as elements of $\square$.

**Remark 4.6.** If we simply want to replace one goal with the other, proving their equivalence is too strong: we just need an implication.

**Remark 4.7.** Term $\omega_1$ requires univalence, because it features $p_{\square}$ as a subterm.

# 5 Type equivalence in kit form

In this section, we propose (§ 5.1) an equivalent, modular presentation of type equivalence, phrased as a nested sigma type. Then (§ 5.2), we carve a hierarchy of structures on relations out of this dependent tuple, selectively picking pieces, in order to revisit parametricity translations through the lens of this finer grained analysis of the relational interpretations of types in § 6.1.
We make heavy use of the axiom of univalence to prove the lemmas and theorems of this section, and we formalized them thoroughly in the companion material. However, none of these proofs are used in the code generated by the plugin. We comment in § 7 on the possible use of axioms in generated code.

## 5.1 Disassembling type equivalence

Let us start by observing that Definition 3.1, of type equivalence, is quite asymmetrical, although this fact is somehow swept under the rug by the infix $A \approx B$ notation. First, the data of an equivalence $e: A \approx B$ privileges the left-to-right direction, as $\uparrow_e$ is directly accessible from $e$ as its first projection, while accessing the right-to-left transport requires an additional projection. Second, the statement of the coherence property, which we elided in Definition 3.1, is actually:

$$ \Pi a : A. \text{ap}_{\uparrow e}(s a) = r \circ \downarrow e $$

where $\text{ap}_f(t)$ is the term $f = f v$, for any identity proof $t: u = v$. This statement uses proofs $s$ and $r$, respectively of the section and retraction properties of $e$, but not in a symmetrical way, although swapping them leads to an equivalent definition. This entanglement prevents tracing the respective roles of each direction of transport, left-to-right or right-to-left, during the course of a given univalent parametricity translation. Exercise 4.2 in the HoTT book [57] however suggests a symmetrical definition of type equivalence, via functional relations.

**Definition 5.1.** A relation $R: A \to B \to \square_i$, is *functional* when:

$$ \Pi a : A. \text{IsContr}(\Sigma b : B. R a b) $$

where for any type $T$, $\text{IsContr}(T)$ is the standard contractibility predicate $\Sigma t: T$. $\Pi t': T$. $t = t'$. This property is denoted $\text{IsFun}(R)$.

We can now obtain an equivalent but symmetrical characterization of type equivalence, as a functional relation whose symmetrization is also functional.

**LEMMA 5.2.** For any types $A, B: \square$, type $A \approx B$ is equivalent to:

$$ \Sigma R : A \to B \to \square. \text{IsFun}(R) \times \text{IsFun}(R^{-1}) $$

where $R^{-1}: B \to A \to \square$ just swaps the arguments of relation $R: A \to B \to \square$.

We sketch below a proof of this result, left as an exercise in [57]. The essential argument is the following characterization of functional relations:

**LEMMA 5.3.** The type of functions is equivalent to the type of functional relations; i.e., for any types $A, B: \square$, we have $(A \to B) \approx \Sigma R: A \to B \to \square$. $\text{IsFun}(R)$.

**PROOF.** The proof goes by chaining the following equivalences:

$$ \begin{align*} (\Sigma R: A \to B \to \square. \text{IsFun}(R)) &\approx (A \to \Sigma P: B \to \square. \text{IsContr}(\Sigma b : B. P b)) \\ &\approx (A \to B) \end{align*} $$

□
PROOF OF LEMMA 5.2. The proof goes by chaining the following equivalences, where the type of $f$ is always $A \to B$ and the type of $R$ is $A \to B \to \square$:

$$
\begin{align*}
(A \approx B) &\approx \Sigma f : A \to B. \text{IsEquiv}(f) && \text{by definition of } (A \approx B) \\
&\approx \Sigma f. \Pi b : B. \text{IsContr}(\Sigma a. f a = b) && \text{standard result in HoTT} \\
&\approx \Sigma f. \text{IsFun}(\lambda(b:B)(a:A). f a = b) && \text{by definition of } \text{IsFun}(\cdot) \\
&\approx \Sigma (\varphi : \Sigma R. \text{IsFun}(R)). \text{IsFun}(\pi_1(\varphi)^{-1}) && \text{by Lemma 5.3} \\
&\approx \Sigma R. \text{IsFun}(R) \times \text{IsFun}(R^{-1}) && \text{by associativity of } \Sigma.
\end{align*}
$$

□

However, the definition of type equivalence provided by Lemma 5.2 does not expose explicitly the two transfer functions in its data, although this computational content can be extracted via first projections of contractibility proofs. In fact, it is possible to devise a definition of type equivalence which directly provides the two transport functions in its data, while remaining symmetrical. This variant follows from an alternative characterization of functional relations.

*Definition 5.4.* For any types $A, B : \square$, a relation $R : A \to B \to \square$, is a *univalent map*, denoted $\text{IsUmap}(R)$ when there exists a function $m : A \to B$ together with:

$$
\begin{align*}
& g_1 : \Pi(a:A)(b:B) \cdot m a = b \to R a b \\
\text{and} \\
& g_2 : \Pi(a:A)(b:B) \cdot R a b \to m a = b \\
\text{such that} \\
& \qquad \Pi(a:A)(b:B) \cdot (g_1 a b) \circ (g_2 a b) \div id.
\end{align*}
$$

Now comes the crux lemma of this section.

LEMMA 5.5. For any types $A, B : \square$ and any relation $R : A \to B \to \square$

$$
\mathrm{IsFun}(R) \approx \mathrm{IsUmap}(R).
$$

PROOF. The proof goes by rewording the left hand side, in the following way:

$$
\begin{align*}
\Pi x. \text{IsContr}(R x) \\
&\approx \Pi x. \Sigma(r : \Sigma y. R x y). \Pi(p : \Sigma y. R x y). r = p \\
&\approx \Pi x. \Sigma y. \Sigma(r : R x y). \Pi(p : \Sigma y. R x y). (y, r) = p \\
&\approx \Sigma f. \Pi x. \Sigma(r : R x (f x)). \Pi(p : \Sigma y. R x y). (f x, r) = p \\
&\approx \Sigma f. \Sigma(r : \Pi x. R x (f x)). \Pi x. \Pi(p : \Sigma y. R x y). (f x, r x) = p \\
&\approx \Sigma f. \Sigma r. \Pi x. \Pi y. \Pi(p : R x y). (f x, r x) = (y, p) \\
&\approx \Sigma f. \Sigma r. \Pi x. \Pi y. \Pi(p : R x y). \Sigma(e : f x = y). r x =_e p \\
&\approx \Sigma f. \Sigma r. \Sigma(e : \Pi x. \Pi y. R x y \to f x = y). \Pi x. \Pi y. \Pi p. (r x) =_{e x y p} p
\end{align*}
$$

where $t =_e u$ denotes the equality of the transport of term $t$ along equality $e$ with term $u$. After a suitable reorganization of the sigma types we are left to show that

$$
\begin{align*}
& \Sigma(r : \Pi x. \Pi y. f x = y \to R x y). (e x y) \circ (r x y) \div id \\
& \approx \Sigma(r : \Pi x. R x (f x)). \Pi x. \Pi y. \Pi p. r x =_{e x y p} p
\end{align*}
$$

whose proof we do not detail, referring the reader to the corresponding code.

□

As a direct corollary, we obtain a novel characterization of type equivalence:
**THEOREM 5.6.** For any types $A, B : \square_i$, we have:

$$ (A \simeq B) \simeq \sqsubseteq_i^\top A B $$

where the relation $\sqsubseteq_i^\top A B$ is defined as:

$$ \Sigma R : A \to B \to \square_i. \text{IsUmap}(R) \times \text{IsUmap}(R^{-1}) $$

The collection of data packed in a term of type $\sqsubseteq_i^\top A B$ is now symmetrical, as the right-to-left direction of the equivalence based on univalent maps can be obtained from the left-to-right by flipping the relation and swapping the two functionality proofs. If the $\eta$-rule for records is verified, symmetry is even *definitely* involutive.

## 5.2 Reassembling type equivalence

Definition 5.4 of univalent maps and the resulting rephrasing of type equivalence suggest introducing a hierarchy of structures for heterogeneous relations, which explains how close a given relation is to type equivalence. In turn, this distance is described in terms of structure available respectively on the left-to-right and right-to-left transport functions.

**Definition 5.7.** For $n, k \in \{0, 1, 2_a, 2_b, 3, 4\}$, and $\alpha = (n, k)$, relation $\sqsubseteq^\alpha : \square \to \square \to \square$, is defined as:

$$ \sqsubseteq^\alpha \triangleq \lambda(A B : \square) \cdot \Sigma(R : A \to B \to \square) \cdot \text{Class}_\alpha R $$

where the *map class* $\text{Class}_\alpha R$ itself unfolds to a pair type $(M_n R) \times (M_k R^{-1})$, with $M_i$ defined as:<fnref n="2" />

$$ M_0 R \triangleq \dots $$

$$ M_1 R \triangleq (A \to B) $$

$$ M_{2_a} R \triangleq \Sigma m : A \to B. G_{2_a} m R \quad \text{with} \quad G_{2_a} m R \triangleq \Pi a b. m a = b \to R a b $$

$$ M_{2_b} R \triangleq \Sigma m : A \to B. G_{2_b} m R \quad \text{with} \quad G_{2_b} m R \triangleq \Pi a b. R a b \to m a = b $$

$$ M_3 R \triangleq \Sigma m : A \to B. (G_{2_a} m R) \times (G_{2_b} m R) $$

$$ M_4 R \triangleq \Sigma m : A \to B. \Sigma(g_1 : G_{2_a} m R) \cdot \Sigma(g_2 : G_{2_b} m R) \cdot \Pi a b. (g_1 a b) \circ (g_2 a b) \div id $$

For any types $A$ and $B$, and any $r : \sqsubseteq^\alpha A B$ we use notations $\text{rel}(r)$, $\text{map}(r)$ and $\text{comap}(r)$ to refer respectively to the relation, map of type $A \to B$, map of type $B \to A$, included in the data of $r$, for a suitable $\alpha$.

**Definition 5.8.** We denote $\mathcal{A}$ the set $\{0, 1, 2_a, 2_b, 3, 4\}^2$, used to index map classes in Definition 5.7. This set is partially ordered for the product order defined from the partial order $0 < 1 < 2_* < 3 < 4$ for $2_*$ either $2_a$ or $2_b$, and with $2_a$ and $2_b$ being incomparable.

**Remark 5.9.** Relation $\sqsubseteq^{(4,4)}$ of Definition 5.7 indeed coincides with the relation $\sqsubseteq^\top$ introduced in Theorem 5.6. It is equivalent to $\sqsubseteq$ by Theorem 3.5. Similarly, we denote $\sqsubseteq^\perp$ the relation $\sqsubseteq^{(0,0)}$, for which we obviously have $\sqsubseteq_i^\perp A B \simeq (A \to B \to \square_i)$.

**Remark 5.10.** Here is a useful dictionary for specific points in the hierarchy:

**Functions.** For $r$ of type $\sqsubseteq^{(1,0)} A B$, $\text{map}(r)$ is an arbitrary function $f : A \to B$, unrelated to relation $\text{rel}(r)$. This can for instance be used to synthesize the proof of an implication, or the existence of a coercion from type $A$ to type $B$.

**Univalent maps.** For $r$ of type $\sqsubseteq^{(4,0)} A B$, $\text{rel}(r)$ is a univalent map, in the sense of Definition 5.4.

<footnote n="2">²For the sake of readability, we omit implicit arguments, e.g., although $M_i$ has type $\lambda(S T : \square)$. $(S \to T \to \square) \to \square$, we write $M_n R$ for $(M_n A B R)$.</footnote>
**Retractions.** For $r$ of type $\sqsubseteq^{(4,2_\alpha)} A B$, $\mathrm{rel}(r)$ is the graph of a retraction (i.e., a surjective univalent map with an explicit partial left inverse) of type $A \to B$. This is the nature of relation at stake in Example 2.4.

**Sections.** For $r$ of type $\sqsubseteq^{(4,2_\beta)} A B$, $\mathrm{rel}(r)$ is the graph of a section (i.e., an injective univalent map with explicit partial right inverse) of type $A \to B$. This is the nature of relation at stake in Example 2.3.

**Equivalences.** For $r$ of type $\sqsubseteq^{(3,3)}$, $r$ is an isomorphism between $A$ and $B$, and for $r$ of type $\sqsubseteq^{(4,4)}$, $r$ is an equivalence between $A$ and $B$. As isomorphisms can always be promoted to a type equivalences, it is always possible to construct a term of type $\sqsubseteq^{(4,4)}$ from a term of type $\sqsubseteq^{(3,3)}$. This is the nature of relation at stake in Examples 2.1 and 2.2.

Observe that $\sqsubseteq^{(n,m)} A B$ coincides, up to equivalence, with $\sqsubseteq^{(m,n)} B A$. Other classes, while not corresponding to a meaningful mathematical definition, may arise in concrete runs of proof transfer.

# 6 A calculus for proof transfer

This section introduces TROCQ, a framework for proof transfer designed as a generalization of both raw and univalent parametricity translations, so as to allow for interpreting types as instances of the structures introduced in Section 5.2. In this framework, the translation of a term may vary, depending on the strength of the expected result. For instance, we may expect to obtain a univalent translation, or a raw translation, and more generally, we may request a witness of any of the nature of relations introduced in § 5. We thus need to inform the translation with classes from $\mathcal{A}$, so as to guide the synthesis of the output term from the input one.

Therefore, we first explain how to generalize the constants $p_{\square i}$ and $p_{\Pi}$ (from § 4.2) according to those classes (§ 6.1). Then we introduce $CC_\omega^+$ (§ 6.2), a Calculus of Constructions with annotations on sorts and subtyping which reflect lattice $\mathcal{A}$, so as to guide the translation. We finally define (§ 6.3) the TROCQ calculus itself.

## 6.1 Populating the hierarchy of relations

We shall now revisit the parametricity translations of Section 3.3. In particular, recall that Theorem 5.6, together with Equation 17, relies on the existence of a term $p_{\square i}$ such that:

$$ \vdash_u p_{\square i} : \sqsubseteq_{i+1}^\top \square_i \square_i \quad \text{and} \quad \mathrm{rel}(p_{\square i}) \simeq \sqsubseteq_i^\top. $$

Otherwise said, the relation $\sqsubseteq^\top : \square \to \square \to \square$ can be endowed with a $\sqsubseteq^\top$ structure, assuming univalence. Similarly, Equation 8, for the raw parametricity translation, can be read as the fact that relation $\sqsubseteq^\perp$ on universes can be endowed with a $\sqsubseteq^\perp \square \square$ structure.

Now the hierarchy of structures introduced by Definition 5.7 enables a finer grained analysis of the possible relational interpretations of universes. Not only would this put the raw and univalent parametricity translations under the same hood, but it would also allow for generalizing parametricity to a larger class of relations. For this purpose, we generalize the previous observation, on the key ingredient for translating universes: for each $\alpha \in \mathcal{A}$, relation $\sqsubseteq^\alpha : \square \to \square \to \square$ may be endowed with several structures from the lattice, and we need to study which ones, depending on $\alpha$. Otherwise said, we need to identify the pairs $(\alpha, \beta) \in \mathcal{A}^2$ for which it is possible to construct a term $p_{\square}^{\alpha, \beta}$ such that:

$$ \vdash_u p_{\square}^{\alpha, \beta} : \sqsubseteq^\beta \square \square \quad \text{and} \quad \mathrm{rel}(p_{\square}^{\alpha, \beta}) \equiv \sqsubseteq^\alpha \qquad (18) $$

Note that we aim here at a definitional equality between $\mathrm{rel}(p_{\square}^{\alpha, \beta})$ and $\sqsubseteq^\alpha$, rather than at an equivalence. It is easy to see that a term $p_{\square}^{\alpha, \perp}$ exists for any $\alpha \in \mathcal{A}$, as $\sqsubseteq^\perp$ requires no structure on
the relation. On the other hand, it is not possible to construct a term $p_{\square}^{\perp, \top}$, i.e., to turn an arbitrary relation into a type equivalence.

**Definition 6.1.** We denote $\mathcal{D}_{\square}$ the following subset of $\mathcal{A}^2$:

$$ \mathcal{D}_{\square} = \{(\alpha, \beta) \in \mathcal{A}^2 \mid \alpha = \top \lor \beta \in \{0, 1, 2_{\alpha}\}^2\} $$

The corresponding code constructs terms $p_{\square}^{\alpha, \beta}$ for every pair $(\alpha, \beta) \in \mathcal{D}_{\square}$, using a meta-program to generate them from a minimal collection of manual definitions. In particular, assuming univalence, it is possible to construct a term $p_{\square}^{\top, \top}$, which can be seen as an analogue of the translation $[\square]$ of univalent parametricity. More generally, the provided terms $p_{\square}^{\alpha, \beta}$ depend on univalence if and only if $\beta \notin \{0, 1, 2_{\alpha}\}$.

We now turn to the other essential ingredient of the abstraction theorem, and investigate the possible structures $\bar{\alpha}^{\gamma}$ endowing the relational interpretation of a product type $\Pi x : A. B$, given relational interpretations for types A and B respectively equipped with structures $\bar{\alpha}$ and $\bar{\beta}$.

Otherwise said, we need to identify the triples $(\alpha, \beta, \gamma) \in \mathcal{A}^3$ for which it is possible to construct a term $p_{\Pi}^{\gamma}$ such that the following statements both hold:

$$ \frac{\Gamma \vdash A_R : \bar{\alpha} A A' \qquad \Gamma, x : A, x' : A', x_R : A_R x x' \vdash B_R : \bar{\beta} B B'}{\Gamma \vdash p_{\Pi}^{\gamma} A_R B_R : \bar{\alpha}^{\gamma} (\Pi x : A. B) (\Pi x' : A'. B')} $$

$$ \mathrm{rel}(p_{\Pi}^{\gamma} A_R B_R) \equiv \lambda f. \lambda f'. \Pi(x : A)(x' : A')(x_R : \mathrm{rel}(A_R) x x'). \mathrm{rel}(B_R) (fx) (f'x') $$

The corresponding collection of triples can actually be described as a function $\mathcal{D}_{\Pi} : \mathcal{A} \to \mathcal{A}^2$, such that $\mathcal{D}_{\Pi}(\gamma) = (\alpha, \beta)$ provides sufficient requirements on the structures associated with A and B, with respect to the partial order on $\mathcal{A}^2$. The corresponding code provides a corresponding collection of terms $p_{\Pi}^{\gamma}$ for each $\gamma \in \mathcal{A}$, as well as all the associated weakenings. Once again, these definitions are generated by a meta-program. Observe in particular that by symmetry, $p_{\Pi}^{(m,n)}$ can be obtained from $p_{\Pi}^{(m,0)}$ and $p_{\Pi}^{(n,0)}$ by swapping the latter and glueing it to the former. Therefore, the values of $p_{\Pi}^{\gamma}$ and $\mathcal{D}_{\Pi}(\gamma)$ are completely determined by those of $p_{\Pi}^{(m,0)}$ and $\mathcal{D}_{\Pi}(m, 0)$. In particular, for any $(m, n) \in \mathcal{A}$:

$$ \mathcal{D}_{\Pi}(m, n) = ((m_A, n_A), (m_B, n_B)) $$

where the annotations $m_A, n_A, m_B, n_B \in \{0, 1, 2_a, 2_b, 3, 4\}$ are such that $\mathcal{D}_{\Pi}(m, 0) = ((0, n_A), (m_B, 0))$ and $\mathcal{D}_{\Pi}(n, 0) = ((0, m_A), (n_B, 0))$. We sum up in Figure 7 the values of $\mathcal{D}_{\Pi}(m, 0)$.

<table><thead><tr><th>m</th><th>D<sub>Π</sub>(m, 0)<sub>1</sub></th><th>D<sub>Π</sub>(m, 0)<sub>2</sub></th></tr></thead><tbody><tr><td>0</td><td>(0, 0)</td><td>(0, 0)</td></tr><tr><td>1</td><td>(0, 2<sub>a</sub>)</td><td>(1, 0)</td></tr><tr><td>2<sub>a</sub></td><td>(0, 4)</td><td>(2<sub>a</sub>, 0)</td></tr><tr><td>2<sub>b</sub></td><td>(0, 2<sub>a</sub>)</td><td>(2<sub>b</sub>, 0)</td></tr><tr><td>3</td><td>(0, 4)</td><td>(3, 0)</td></tr><tr><td>4</td><td>(0, 4)</td><td>(4, 0)</td></tr></tbody></table>

<table><caption>Fig. 7. Constraints for product and arrow types</caption><thead><tr><th>m</th><th>D<sub>→</sub>(m, 0)<sub>1</sub></th><th>D<sub>→</sub>(m, 0)<sub>2</sub></th></tr></thead><tbody><tr><td>0</td><td>(0, 0)</td><td>(0, 0)</td></tr><tr><td>1</td><td>(0, 1)</td><td>(1, 0)</td></tr><tr><td>2<sub>a</sub></td><td>(0, 2<sub>b</sub>)</td><td>(2<sub>a</sub>, 0)</td></tr><tr><td>2<sub>b</sub></td><td>(0, 2<sub>a</sub>)</td><td>(2<sub>b</sub>, 0)</td></tr><tr><td>3</td><td>(0, 3)</td><td>(3, 0)</td></tr><tr><td>4</td><td>(0, 4)</td><td>(4, 0)</td></tr></tbody></table>

Note that in the case of a non-dependent product, constructing $p_{\rightarrow}^{\gamma}$ requires less structure on the domain A of an arrow type $A \to B$, which motivates the introduction of function $\mathcal{D}_{\rightarrow}(\gamma)$. Using the combinator for dependent products to interpret the special case of an arrow type, albeit correct,
potentially pulls in unnecessary structure (and axiom) requirements. The corresponding code thus includes a construction of terms $p^\gamma$, for any $\gamma \in \mathcal{A}$.

The two tables in Fig.7 show how requirements on levels stay the same on the right hand side of both $\Pi$ and $\to$, stay the same up to symmetries (exchange of variance and of $2_a$ and $2_b$) on the left hand side of a $\to$ and increase on the left hand side of a $\Pi$. This elegant arithmetic justifies our hierarchy of relations. We conjecture that the dependencies given in Figure 7 are minimal.

## 6.2 Annotated type theory

We are now ready to generalize the relational interpretation of types provided by the univalent parametricity translation, so as to allow for interpreting sorts with instances of weaker structures than equivalence. For this purpose, we introduce a variant $CC_\omega^+$ of $CC_\omega$ where each universe is annotated with a label indicating the structure available on its relational interpretation. Recall from Section 5.2 that we have used annotations $\alpha \in \mathcal{A}$ to identify the different structures of the lattice disassembling type equivalence: these are the labels annotating sorts of $CC_\omega^+$, so that if $A$ has type $\square^\alpha$, then the associated relation $A_R$ has type $\sqcup^\alpha A A'$. On concrete applications, where type $A'$ is synthesized together with $A_R$, annotation $\alpha$ indicates the nature of parametricity translation expected by the user. For instance, if $A$ has type $\square^\perp$, then the framework will compute the raw translation of $A$, and if $A$ has type $\square^\top$, it will compute the univalent one. But the framework also offers a palette of other options, put to good use in the corresponding implementations to the examples of Section 2. The syntax of $CC_\omega^+$ is thus:

$$ \mathcal{T}_{CC_\omega^+} \ni M, N, A, B ::= \Box_i^\alpha | x | M N | \lambda x : A. M | \Pi x : A. B \\ \alpha \in \mathcal{A} = \{0, 1, 2_a, 2_b, 3, 4\}^2 \quad i \in \mathbb{N} $$

Before completing the actual formal definition of the TROCQ proof transfer framework, let us informally illustrate how these annotations shall drive the interpretation of terms, and in particular, of a dependent product $\Pi x : A. B$. In this case, before translating $B$, three terms representing the bound variable $x$, its translation $x'$, and the parametricity witness $x_R$ are added to the context. The type of $x_R$ is $rel(A_R) \times x$ where $A_R$ is the parametricity witness relating $A$ to its translation $A'$. The role of annotation $\alpha$ on the sort typing type $A$ is thus to govern the amount of information available in witness $x_R$, by determining the type of $A_R$. This intent is reflected in the typing rules of $CC_\omega^+$, which rely on the definition of the loci $D_\square$, $D_\to$ and $D_\Pi$, introduced in §6.1.

Contexts are defined as usual, but typing terms in $CC_\omega^+$ requires defining a *subtyping* relation $\leq$, defined by the rules of Figure 8. The typing rules of $CC_\omega^+$ are available in Figure 9 and follow standard presentations [9]. The $\equiv$ relation in the (SUBCONV) rule is the *conversion* relation, defined as the closure of $\alpha$-equivalence and $\beta$-reduction. The two types of judgment in $CC_\omega^+$ are thus:

$$ \Gamma \vdash_+ A \leq B \quad \text{and} \quad \Gamma \vdash_+ M : A $$

where $M, A$ and $B \in \mathcal{T}_{CC_\omega^+}$ are terms in $CC_\omega^+$ and $\Gamma \in \mathcal{C}_{CC_\omega^+}$ is a context in $CC_\omega^+$.

We show that our extension is conservative over $CC_\omega$, by defining an erasure function for terms $| \cdot |^\gamma : \mathcal{T}_{CC_\omega^+} \to \mathcal{T}_{CC_\omega}$ and for contexts, defined in Figure 10.

We show that the erasure of subtyping is convertibility in $CC_\omega$:

**LEMMA 6.2 (CONSERVATIVITY OF CONVERSION IN $CC_\omega^+$).**

$$ \Gamma \vdash_{CC_\omega^+} A \leq B \implies |\Gamma|^{-} \vdash_{CC_\omega} |A|^{-} \equiv |B|^{-} $$

**PROOF.** By induction on the derivation. $\square$

Finally we show that $CC_\omega^+$ is a conservative extension over $CC_\omega$:
<figure><img src="image_3.png" /><figcaption>Fig. 8. Subtyping rules for $CC_{\omega}^{+}$</figcaption></figure>

<figure><img src="image_4.png" /><figcaption>Fig. 9. Typing rules for $CC_{\omega}^{+}$</figcaption></figure>

<figure><img src="image_5.png" /><figcaption>Fig. 10. Erasure function from $CC_{\omega}^{+}$ to $CC_{\omega}$</figcaption></figure>

THEOREM 6.3 (CONSERVATIVITY OF $CC_{\omega}^{+}$).

$$ \forall \Gamma \in \mathcal{C}_{CC_{\omega}^{+}}, \forall t, A \in \mathcal{T}_{CC_{\omega}^{+}}, \Gamma \vdash_{CC_{\omega}^{+}} t : A \implies |\Gamma|^{-} \vdash_{CC_{\omega}} |t|^{-} : |A|^{-} $$

PROOF. By induction on the derivation.

□
## 6.3 The TROCQ calculus

The final stage of the announced generalization consists in building an analogue to the parametricity translations available in pure type systems, but for the annotated type theory of § 6.2. This analogue is geared towards proof transfer, as discussed in § 3.1, and therefore designed to synthesize the output of the translation from its input, rather than to check that certain pairs of terms are in relation. However, splitting up the interpretation of universes into a lattice of possible relation structures means that the source term of the translation is not enough to characterize the desired output: the translation needs to be informed with some extra information about the expected amount of data in the output of the translation. In the TROCQ calculus, this extra information is a type of $CC_{\omega}^{+}$.

We thus define TROCQ contexts $\mathcal{R}_{CC_{\omega}^{+}}$ as lists of quadruples:

$$ \Delta ::= \langle \rangle \mid \Delta, x @ A \sim x' \vdots x_R \quad \text{where } A \in \mathcal{T}_{CC_{\omega}^{+}}. $$

We denote $\text{Var}(\Delta)$ the sequence of variables related in a parametricity context $\Xi$, with multiplicities:

$$ \text{Var}(\langle \rangle) = \langle \rangle \quad \text{Var}(\Delta, x @ A \sim x' \vdots x_R) = \text{Var}(\Delta), x, x', x_R. $$

A TROCQ context $\Delta$ is well-formed, written $\Delta \vdash_+$, if the sequence $\text{Var}(\Delta)$ is duplicate-free. In this case, we use the notation $\Delta(x) = (A, x', x_R)$ as a synonym of $(x, A, x', x_R) \in \Xi$.

Now, a TROCQ judgment is a 4-ary relation of the form $\Delta \vdash_t t @ A \sim t' \vdots t_R$, which is read in context $\Delta$, term $t$ of annotated type $A$ translates to term $t'$, because $t_R$ and $t_R$ is called a parametricity witness. TROCQ judgments are defined by the rules of Figure 11. This definition involves a weakening function for parametricity witnesses, defined as follows.

**Definition 6.4.** For all $p, q \in \{0, 1, 2_a, 2_b, 3, 4\}$, such that $p \ge q$, we define map $\downarrow_q^p: M_p \to M_q$, which forgets the fields from class $M_p$ that are not in $M_q$.

For all $\alpha, \beta \in \mathcal{A}$, such that $\alpha \ge \beta$, function $\mathcal{W}_{\beta}^{\alpha}: \mathcal{A} B \to \mathcal{B} A$ is defined by:

$$ \mathcal{W}_{(p,q)}^{(m,n)} \langle R, M \rhd, M \rhd \rangle := \langle R, \downarrow_p^m M \rhd, \downarrow_q^n M \rhd \rangle. $$

The weakening function on parametricity witnesses is defined on Figure 12 by extending function $\mathcal{W}_{\beta}^{\alpha}$ to all relevant pairs of types of $CC_{\omega}^{+}$, i.e., $\mathcal{W}_{U}^{T}$ is defined for $T, U \in \mathcal{T}_{CC_{\omega}^{+}}$ as soon as $T \le U$.

We first show the following standardization lemma for TROCQ judgments.

**LEMMA 6.5.** If $\Delta \vdash_t u @ A \sim u' \vdots u_R$ holds, then there exists a derivation of this judgment where the TROCQCONV rule is used only on variables, i.e., with $t, t'$ and $t_R$ variables.

**PROOF.** By induction on the derivation. The only interesting case is the TROCQCONV rule. By induction hypothesis the premise can be turned into a derivation $D$ which ends either with TROCQCONV rule on a variable or ends with any rule but the TROCQCONV rule. There are then four nontrivial cases for this last rule of $D$:

* TROCQCONV rule on a variable: the two successive TROCQCONV rules collapse into a single one by composing weakenings;

* TROCQSORT rule: the TROCQCONV rule can be omitted as, by construction, $\mathcal{W}_{\delta}^{\beta} p_{\square}^{\alpha, \beta} = p_{\square}^{\alpha, \delta}$;

* TROCQPI rule: similar, since by construction $\mathcal{W}_{\delta}^{\beta} p_{\Pi}^{\beta} = p_{\Pi}^{\delta}$;

* TROCQARROW rule: similar, since by construction $\mathcal{W}_{\delta}^{\beta} p_{\downarrow}^{\beta} = p_{\downarrow}^{\delta}$.

□
LEMMA 6.6. The relation associating a pair (t, A) ∈ CC<sub>ω</sub><sup>+2</sup> with a pair (t', t<sub>R</sub>) ∈ CC<sub>ω</sub><sup>+2</sup> such that Δ ⊢<sub>t</sub> t @ A ~ t' :: t<sub>R</sub> holds, with Δ a well-formed TROCQ context, is functional. More precisely, for any well-formed TROCQ context Δ:

$$
\begin{align*}
& \forall \Delta, t, A, t', u', t_R, u_R, \Delta \vdash t @ A \sim t' :: t_R \wedge \Delta \vdash t @ A \sim u' :: u_R \\
& \implies (t', t_R) = (u', u_R)
\end{align*}
$$

PROOF. First we use Lemma 6.5 to normalise the derivations. Then we reason by induction on the syntax of *t*. Because the derivation is normal, there is only one possible rule for each syntactic construction, except for the TROCQARROW and TROCQPI rules, but $p_{\Pi}^{\delta}$ and $p_{\neg}^{\delta}$ happen to coincide when they are both applicable. □

We introduce a conversion function $\gamma$ from TROCQ contexts to $CC_{\omega}^{+}$ contexts:

$$
\begin{align*}
\gamma(\langle\rangle) &= \langle\rangle \\
\gamma(\Delta, x @ A \sim x' :: x_R) &= \gamma(\Delta), x : A, x' : A', x_R : \text{rel}(A_R) \ x \ x' \\
&\qquad \text{where } \Delta \vdash_t A @ \Box_i^{\alpha} \sim A' :: A_R.
\end{align*}
$$

Note that $\gamma$ is well defined because of Lemma 6.6.

$$
\begin{align*}
\frac{\substack{(\alpha, \beta) \in \mathcal{D} \\ \Delta \vdash_t \Box_i^\alpha \@ \Box_{i+1}^\beta \sim \Box_i^\alpha \vdash p_{\Box i}^{\alpha, \beta}}}{\Delta \vdash_t \Box_i^\alpha \@ \Box_{i+1}^\beta \sim \Box_i^\alpha \vdash p_{\Box i}^{\alpha, \beta}} \quad (\text{TROCQSORT})
&\qquad
\frac{\substack{(x, A, x', x_R) \in \Delta \\ \Delta \vdash_t x @ A \sim x' \vdash x_R}}{\Delta \vdash_t x @ A \sim x' \vdash x_R} \quad (\text{TROCQVAR}) \\[1.5em]
\frac{\substack{\Delta \vdash_t t @ \Pi x : A.B \sim t' \vdash t_R \\ \Delta \vdash_t t u @ B[x := u] \sim t' u' \vdash t_R u u' u_R}}{\Delta \vdash_t \lambda x : A.t @ \Pi x : A.B \sim \lambda x' : A'.t' \vdash \lambda x x' x_R.t_R} \quad (\text{TROCQAPP}) \\[1.5em]
\frac{\substack{\Delta \vdash_t A @ \Box_i^\alpha \sim A' \vdash A_R \\ \Delta, x @ A \sim x' \vdash x_R \vdash_t t @ B \sim t' \vdash t_R}}{\Delta \vdash_t \lambda x : A.t @ \Pi x : A.B \sim \lambda x' : A'.t' \vdash \lambda x x' x_R.t_R} \quad (\text{TROCQLAM}) \\[1.5em]
\frac{\substack{(\alpha, \beta) = \mathcal{D} \rightarrow (\delta) \\ \Delta \vdash_t A @ \Box_i^\alpha \sim A' \vdash A_R \\ \Delta \vdash_t B @ \Box_i^\beta \sim B' \vdash B_R}}{\Delta \vdash_t A \rightarrow B @ \Box_i^\delta \sim A' \rightarrow B' \vdash p_{\rightarrow}^\delta A_R B_R} \quad (\text{TROCQARROW}) \\[1.5em]
\frac{\substack{(\alpha, \beta) = \mathcal{D}_\Pi(\delta) \\ \Delta \vdash_t A @ \Box_i^\alpha \sim A' \vdash A_R \\ \Delta, x @ A \sim x' \vdash x_R \vdash_t B @ \Box_i^\beta \sim B' \vdash B_R}}{\Delta \vdash_t \Pi x : A.B @ \Box_i^\delta \sim \Pi x' : A'.B' \vdash p_{\Pi}^\delta A_R B_R} \quad (\text{TROCQPI}) \\[1.5em]
\frac{\substack{\Delta \vdash_t t @ A \sim t' \vdash t_R \\ \Delta \vdash_t t @ B \sim t' \vdash \mathcal{J}_B^A t_R}}{\Delta \vdash_t t @ B \sim t' \vdash \mathcal{J}_B^A t_R} \quad (\text{TROCQCONV})
\end{align*}
$$

<caption>Fig. 11. TROCQ rules</caption>

An abstraction theorem relates TROCQ judgments and typing in $CC_{\omega}^{+}$.
$$
\begin{align*}
\mathop{\mathcal{V}}\limits_{\Box_i^{\alpha'}} t_R &:= \mathop{\mathcal{V}}\limits_{\Box_{\alpha'}^{\alpha}} t_R &
\mathop{\mathcal{V}}\limits_{A'u'}^{A u} t_R &:= \mathop{\mathcal{V}}\limits_{A'}^{A} u u' t_R &
\mathop{\mathcal{V}}\limits_{\lambda x:A'. B'}^{\lambda x:A.B} u u' t_R &:= \mathop{\mathcal{V}}\limits_{B'[x:=u']}^{B[x:=u]} t_R \\
\mathop{\mathcal{V}}\limits_{\Pi x:A'. B'} t_R &:= \lambda x x' x_R &
\mathop{\mathcal{V}}\limits_{B'}^{B} (t_R x x' (\mathop{\mathcal{V}}\limits_{A}^{A'} x_R)) & &
\mathop{\mathcal{V}}\limits_{A'}^{A} t_R &:= t_R
\end{align*}
$$

<caption>Fig. 12. Weakening of parametricity witnesses</caption>

THEOREM 6.7 (TROCQ ABSTRACTION THEOREM).

$$
\frac{\gamma(\Delta) \vdash_+ \gamma(\Delta) \vdash_+ t : A \quad \Delta \vdash_t t @ A \sim t' \vdots t_R \quad \Delta \vdash_t A @ \Box_i^{\alpha} \sim A' \vdots A_R}{\gamma(\Delta) \vdash_+ t' : A' \quad \text{and} \quad \gamma(\Delta) \vdash_+ t_R : \text{rel}(A_R) t t'}
$$

PROOF. By induction on derivation $\Delta \vdash_t t @ A \sim t' \vdots t_R$.

□

Note that type A in the typing hypothesis $\gamma(\Delta) \vdash_+ t : A$ of the abstraction theorem is exactly the extra information passed to the translation. The latter can thus also be seen as an inference algorithm, which infers annotations for the output of the translation from that of the input.

Remark 6.8. Since by definition of $p_{\square}^{\alpha,\beta}$ (Equation 18), we have $\vdash_t \square^\alpha @ \square^\beta \sim \square^\alpha \vdash p_{\square}^{\alpha,\beta}$, by applying Theorem 6.7 with $\gamma(\Delta) \vdash_+ A : \square^\alpha$, we get:

$$
\frac{\gamma(\Delta) \vdash_+ A : \Box^\alpha \quad \Delta \vdash_t A @ \Box^\alpha \sim A' \vdots A_R}{\gamma(\Delta) \vdash_+ A_R : \mathrm{rel}(p_{\Box}^{\alpha,\beta}) A A'}
$$

Now by the same definition, for any $\beta \in A$, $\mathrm{rel}(p_{\square}^{\alpha,\beta}) = \beta^\alpha$, hence $\gamma(\Delta) \vdash A_R : \beta^\alpha A A'$, as expected by the type annotation $A : \square^\alpha$ in the premise of the rule.

Remark 6.9. By applying Remark 6.8 with $\vdash_+ \square^\alpha : \square^\beta$, we indeed obtain that $\vdash_+ p_{\square}^{\alpha,\beta} : \square^\beta \square^\alpha \square^\alpha$ as expected, provided that $(\alpha, \beta) \in \mathcal{D}_\square$.

6.4 Conservativity over raw and univalent parametricity

We show that TROCQ entails raw parametricity and univalent parametricity by defining minimal and maximal annotations $|\cdot|^{\top} : \mathcal{T}_{CC_{\omega}} \rightarrow \mathcal{T}_{CC_{\omega}^{+}}$ and $|\cdot|^{\bot} : \mathcal{T}_{CC_{\omega}} \rightarrow \mathcal{T}_{CC_{\omega}^{+}}$ as in Figure 13, which are two obvious right inverses of $|\cdot|^{\bot}$. We then have the following theorems.

THEOREM 6.10 (TROCQ CONSERVATIVITY OVER RAW PARAMETRICITY).

$$
\forall \Gamma \in \mathcal{C}_{CC_{\omega}}, \forall \Xi \in \mathcal{R}_{CC_{\omega}}, \forall t, A, t', t_R \in \mathcal{T}_{CC_{\omega}}, \Gamma \triangleright \Xi \wedge \Gamma \vdash t : A \wedge \Xi \vdash t \sim t' \vdots t_R \\
\implies \exists t_{\perp}, |\Gamma; \Xi|^\perp \vdash_t |t|^\perp @ |A|^\perp \sim |t'|^\perp \vdots t_{\perp}
$$

and

$$
\forall \Gamma \in \mathcal{C}_{CC_{\omega}}, \forall \Xi \in \mathcal{R}_{CC_{\omega}}, \forall t, A, t', t_{\perp} \in \mathcal{T}_{CC_{\omega}}, \Gamma \triangleright \Xi \wedge \\
|\Gamma; \Xi|^\perp \vdash_t |t|^\perp @ |A|^\perp \sim |t'|^\perp \vdots t_{\perp} \\
\implies \exists t_R, \Gamma \vdash t : A \wedge \Xi \vdash t \sim t' \vdots t_R
$$

PROOF. By induction on the derivation.

□
### THEOREM 6.11 (TROCQ CONSERVATIVITY OVER UNIVALENT PARAMETRICITY).

$$ \forall \Gamma \in \mathcal{C}_{CC_\omega}, \forall \Xi \in \mathcal{R}_{CC_\omega}, \forall t, A, t', t_u \in \mathcal{T}_{CC_\omega}, \Gamma \triangleright \Xi \wedge \Gamma \vdash t : A \wedge \Xi \vdash_u t \sim t' \therefore t_u \\ \implies \exists t_\tau, \quad |\Gamma; \Xi|^\top \vdash_t |t|^\top @ |A|^\top \sim |t'|^\top \therefore t_\tau $$

and

$$ \forall \Gamma \in \mathcal{C}_{CC_\omega}, \forall \Xi \in \mathcal{R}_{CC_\omega}, \forall t, A, t', t_\tau \in \mathcal{T}_{CC_\omega}, \Gamma \triangleright \Xi \wedge \\ |\Gamma; \Xi|^\top \vdash_t |t|^\top @ |A|^\top \sim |t'|^\top \therefore t_\tau \\ \implies \exists t_u, \quad \Gamma \vdash t : A \wedge \Xi \vdash_u t \sim t' \therefore t_u $$

*PROOF.* By induction on the derivation. □

<figure><img src="image_6.png" /></figure>

For the sake of simplicity we do not formally state the relation between witnesses $t_R$ and $t_\perp$ on one hand, and witnesses $t_u$ and $t_\tau$ on the other. But they pairwise have the same underlying relation when it makes sense. This is a consequence of Remark 5.9.

For $\alpha \in \{\tau, \perp\}$, we define

$$ \begin{align*} |\Box_i|^\alpha &:= \Box_i^\alpha \\ |\Pi x : A. B|^\alpha &:= \Pi x : |A|^\alpha . |B|^\alpha \\ |\lambda x : A. B|^\alpha &:= \lambda x : |A|^\alpha . |B|^\alpha \\ |M N|^\alpha &:= |M|^\alpha |N|^\alpha \\ |x|^\alpha &:= x \\ |\langle \rangle|^\alpha &:= \langle \rangle \\ |\Gamma, x : A, x' : A', x_R : A_R x x'|^\alpha &:= |\Gamma|^\alpha, x : |A|^\alpha \\ |\langle \rangle; \langle \rangle|^\alpha &:= \langle \rangle \\ |(\Gamma, x : A, x' : A', x_R : A_R x x') ; (\Xi, x \sim x' \vdash x_R)|^\alpha &:= |\Gamma; \Xi|^\alpha, x @ |A|^\alpha \sim x' \vdash x_R \end{align*} $$

<caption>Fig. 13. Annotation function from $CC_\omega$ to $CC_\omega^+$</caption>

## 6.5 Constants and constraints

As was the case for the raw and univalent parametricity translations, concrete applications require extending TROCQ with constants. In this case as well, we treat constants in a similar way as variables, except that the latter are stored in a global context instead of a typing context. A crucial difference though is that a same constant may lead to several copies in this global $CC_\omega^+$ context, with different annotated types.

Consider for example, a constant list, standing for the type of polymorphic lists. As list A is the type of lists with elements of type A, list can be annotated with type $\Box^\alpha \to \Box^\alpha$ for any $\alpha \in \mathcal{A}$. We thus need to extend the typing of constants to allow for sets of annotated types. Hence, given
* a set $\mathcal{C}$ of symbols,

* for each $c \in \mathcal{C}$, a term $T_c \in \mathcal{T}_{CC_\omega}$, such that $\vdash T_c : \square$,

* for each $c \in \mathcal{C}$, a subset $T_c^+ \subset \mathcal{T}_{CC_\omega}^+$ of annotated types, such that for all $c$ and for all $A \in T_c^+$, $\vdash |A|^{-} \equiv T_c$,

* a partial translation function $\mathcal{D} : \mathcal{C} \to \mathcal{T}_{CC_\omega}^+ \to \mathcal{C}^2$ such that if for all $c, c', c_R \in \mathcal{C}$ and $A \in \mathcal{CC}_\omega^+$ such that $\mathcal{D}_c(A) = (c', c_R)$, $\vdash T_c @ \square^\alpha \sim T_{c'} \vdash T_{c_R}$ holds for some $\alpha$ and $\vdash c_R : \text{rel}(T_{c_R}) c c'$ holds,

the rules of Figure 14 shall respectively extend $\mathcal{CC}_\omega^+$ and TROCQ.

$$ \frac{c \in \mathcal{C} \quad A \in T_c^+}{\Gamma \vdash c : A} (\text{CONST}^+) \qquad \frac{\mathcal{D}_c(A) = (c', c_R)}{\Delta \vdash_t c @ A \sim c' \vdash c_R} (\text{TROCQCONST}) $$

<caption>Fig. 14. Additional constant rules for $\mathcal{CC}_\omega^+$ and TROCQ</caption>

Every constant declared in the global environment thus has an associated collection of possible annotated types $T_c^+ \subset \mathcal{T}_{CC_\omega}^+$. We require that all the annotated types of a same constant share the same erasure in $\mathcal{CC}_\omega$, i.e., $\forall c, \forall A, \forall B, A, B \in T_c^+ \Rightarrow |A|^{-} = |B|^{-}$, by making sure their erasure coincides with the $\mathcal{CC}_\omega$ type of the constant $c$. For example, $T_{\text{list}}^+ = \{\square^\alpha \to \square^\alpha | \alpha \in \mathcal{A}\}$.

In addition, we provide translations $\mathcal{D}_c(A)$ for each possible annotated type $A$ of each constant $c$ in the global context. For example, the translation $\mathcal{D}_{\text{list}}(\square^{(1,0)} \to \square^{(1,0)})$ of the list inductive type is equal to $(\text{list}, \lambda A A' A_R$. $(\text{List.All2} A_R, \text{List.map} (\text{map} A_R)))$, where relation $\text{List.All2} A_R$ relates lists of the same length, whose elements are pair-wise related via $A_R$, $\text{List.map}$ is the usual map function on lists and $\text{map} A_R : A \to A'$ extracts the map projection of the tuple $A_R$ of type $\sqcap^{(1,0)} A A' \equiv \Sigma R. A \to A'$. Part of these translations can be generated automatically by weakening.

Note that for an input term featuring constants, an unfortunate choice of annotation in the derivation tree may lead to a stuck translation. For example, we cannot pick the annotated type $\square^{(1,0)} \to \square^{(1,0)}$ in order to translate list $A$ @ $\square^{(2a,0)}$. We describe in Section 7 the algorithm which picks correct levels for each constant annotation.

# 7 Implementation

The TROCQ plugin [22] turns the material presented in Section 6 into an actual tactic, called trocq, for automating proof transfer in Rocq/Coq. This tactic synthesizes a new goal from the current one, as well as a proof that the former implies the latter. Otherwise said, the tactic operates a translation at level (1, 0) of the current goal. User-defined relations between constants, registered via specific vernacular commands, inform this synthesis. The core of the plugin implements each rule of the TROCQ calculus in the Elpi meta-programming language [29, 54], on top of Rocq/Coq libraries formalizing the contents of Section 5. In the logic programming paradigm of Elpi, each rule of Figure 11 translates gracefully into a corresponding $\lambda$Prolog predicate, making the corresponding source code very close to the presentation of §6.3. However, the TROCQ plugin also implements a much less straightforward annotation inference algorithm, so as to hide the management of sort annotations to Rocq/Coq users completely.

The algorithm proceeds in three phases. First, it annotates terms, with unknown annotations left as meta-variables (§7.1). Second, it runs the direct translation of the TROCQ calculus as a logic program, leaving meta-variables for every term which relies on unknown annotations, while storing constraints on annotations in a graph (§7.2). Last, it solves the constraint graph by assigning the minimal possible value for each annotation, and fills the remaining holes accordingly (§7.3). In addition, the plugin is relying on user given translations for constants (§7.4).
Two variants of the plugin are currently available, one based on the HoTT library<fnref n="3" /> [57], and the other based on Rocq/Coq's standard library<fnref n="4" />. Since some translations are only possible in the presence of the axiom of univalence or functional extensionality, we provide two commands, namely `Trocq Register Univalence u` and `Trocq Register Funnext f` for users wanting to rely on these axioms. Naturally, the standard library version of Rocq/Coq is incompatible with the use of the former.

## 7.1 Encoding $CC_\omega^+$.

To implement the annotation calculus $CC_\omega^+$, we simply annotate Rocq/Coq's sort `Type` with a pair $(n, m)$ using *convertible synonyms* `PType n m`, where `PType ::= fun (_ _ : map_class) => Type`. The two thrown-away arguments code for the parametricity class annotations using the `map_class` inductive type with values ranging from `map0` to `map4`, representing the values in $\mathcal{A}$. They are phantom values whose single purpose is that we can match them syntactically in the plugin. Since `PType m n` is definitionally equal to `Type` the annotation can be erased in a step of $\delta$-reduction and annotated terms are valid Rocq/Coq terms, which means Rocq/Coq typechecker will be unaffected.

The plugin first translates all occurrences of `Type` into `PType _ _`, and during the run of the second part of the algorithm, the two holes of each `PType` will be related to other levels in the constraint graph, according to the rules given by $D_\square$, $D_\Pi$, and $D_c$ for any constant $c$.

## 7.2 Synthesis

The logic programming paradigm on which Elpi is based, is ideal to implement algorithms expressed as inference rules, as each rule can be associated to an instance of a predicate. The linear traversal of the input term at the core of the TROCQ plugin is operated by the predicate `param`, of arity 4, where `param X T X' XR` stands for the parametricity sequent $\Delta \vdash_t x @ T \sim x' \therefore x_R$ for a certain context $\Delta$. In this sequent, $x$ and $T$ are input values (initially, the source goal and the annotated sort $\square^{(0,1)})$, and the synthesized term $x'$ and witness $x_R$ are outputs. Each construct of $CC_\omega$ leads to one instance of the predicate. As an example, let us inspect the instance of the `param` predicate for dependent products, which implements the rule TROCQPI of the TROCQ calculus. For the sake of readability, we removed lines related to logs, pretty-printing, and fresh universe instance generation. The head of the predicate is:

```
param (prod N A B) (app [pglobal (const PType)_, M1, M2]) Prod' ProdR :-
    param.db.ptype PType, !,
    cstr.univ-link C M1 M2,
```

which matches an input term $\Pi x : A. B$ and our Rocq/Coq encoding of its annotated type $\square^{(M_1, M_2)}$. Then, following the hypotheses in the inference rule, the predicate computes the prescribed annotation $(C_A, C_B) = D_\Pi(C)$, and does two recursive calls on $A$ and $B$ with classes $C_A$ and $C_B$:

```
cstr.dep-pi C CA CB,
cstr.univ-link CA M1A M2A,
param A (app [pglobal (const PType)_, M1A, M2A]) A' AR,
cstr.univ-link CB M1B M2B,
TB = app [pglobal (const PType)_, M1B, M2B],
@annot-pi-decl N A a\ pi a' aR\ param.store a A a' aR =>
param (B a) TB (B' a') (BR a a' aR),
```

<footnote n="3">³https://github.com/coq-community/trocq/releases/tag/0.1.6</footnote>

<footnote n="4">⁴https://github.com/coq-community/trocq/releases/tag/0.1.8%2Bprop</footnote>
The HOAS encoding of Rocq/Coq terms saves us from an otherwise tricky management of bound variables.

The last step (omitted in the above snippet) is to build the output proof $p_{\Pi}^{C} A_{R} B_{R}$. As the axioms (univalence, functional extensionality) that might be involved in some proofs are not assumed globally, they are used as an additional argument albeit only in the building blocks that require them. Therefore, we check whether the requested rule requires the addition of an axiom to the list of arguments (in the case of the dependent product, function extensionality). If this axiom is not present in the context at the time of calling this part of the code, the tactic rightfully fails, because the translation is impossible.

*Exploiting symmetries.* TROCQ provides several distinct rules per language construct (such as Π) and per relation structure among the 36 items in the hierarchy: for a same construct, these rules differ by the annotations required on the input of the rule, and by the structure of the relation relating the input term and the synthesized one. For each such rule, a Rocq/Coq function provides the corresponding rule building block. Making the most of symmetries, the 495 rule building blocks are generated by meta-programming from only 9 manually defined ones.

## 7.3 Solving constraints

Finally, the traversal of the input term collects constraints on the annotations, as multiple valid solutions might exist: for instance, an implication might be obtained from weakening an equivalence.

The constraints are stored as a graph where nodes are either variable or constant parametricity classes, and different types of edges exist, based on the constraints involved in the translation. An example of constraint graph is available in Figure 15. For instance, the edges from $X_1$ to $X_2$ and $X_3$ represent the constraint $D_{\Pi}(X_1) = (X_2, X_3)$, and the edge from $X_6$ to the constant class $(3, 2_b)$ represents the constraint $(3, 2_b) \ge X_6$.

<figure><img src="image_7.png" /><figcaption>Fig. 15. Example of constraint graph</figcaption></figure>

The algorithm strives to minimize the requirements on the user-defined building blocks, which also amounts to minimizing the dependency on axioms.

This inference procedure is formalized as a *finite domain constraint solving problem*, and implemented using *Constraint Handling Rules* (CHR) language [30], as available in Elpi. It allows suspending goals and turning them into syntactic constraints, to be reduced with meta-level rules or resumed when some variables are instantiated. The CHR language is well suited to prototype constraint solvers because the core ingredient of such solvers, constraint propagation and consistency checking, can be implemented as CHR reduction rules.

## 7.4 Handling of constants

In order to handle constants, we provide a vernacular command `Trocq Use` to insert new TROCQ quadruples in the database of known rules. Given a term $t_R$ of type $R \ t \ t'$, we insert an annotated type $A$ from $R$ and insert the rule $t \ @ \ A \sim t' \vdots t_R$ in the database.
We provide an API to create new relations out of section retraction pairs, reflecting Remark 5.10.

```
Record SplitSurj.type (A B : Type) : Type := Build {
  retract :> A → B;
  section : B → A;
  sectionK : ∀ x : B, retract (section x) = x
}.

Record SplitInj.type (A B : Type) : Type := Build {
  section :> A → B;
  retract : B → A;
  sectionK : ∀ x : A, retract (section x) = x
}.

Definition SplitSurj.toParam {A B : Type} : SplitSurj.type A B → Param42a.Rel A B := ...

Definition SplitInj.toParam {A B : Type} : SplitInj.type A B → Param42b.Rel A B := ...
```

Here, `Param42a.Rel` is the Rocq/Coq definition for $\sqsubseteq^{(4,2a)}$, and `Param42b.Rel` for $\sqsubseteq^{(4,2b)}$.

We also provide various helper lemmas, including lemmas that exploit the symmetry of relations to derive more structure on them.

# 8 Examples

This section illustrates the usage of the `trocq` tactic on various concrete examples. They rely on the manual `TROCQ` translation of the following inductive types and their constructors and sometimes eliminators, seen as constants: `Empty`, `bool`, `nat`, `option`, `prod`, `sum`, `sigma`, `list`, `eq` / `paths` and `vector`.

All the examples from this section can be dealt with `TROCQ` without using axioms, neither univalence nor functional extensionality.

## 8.1 Isomorphisms

Bitvectors (code). Here are two possible encodings of bitvectors in Rocq/Coq:

```
bounded_nat (k : nat) := {n : nat & n < pow 2 k}. (* n < 2^k *)
bitvector (k : nat) := Vector.t Bool k. (* size k vectors of booleans *)
```

We can prove that these representations are equivalent by combining two proofs by transitivity: the proof that `bounded_nat k` is related to `bitvector k` for a given `k`, and the proof that `Vector.t` is related to itself. We also make use of the equivalence relations `natR` and `boolR`, which respectively relate type `nat` and `bool` with themselves:

```
Rk : ∀ (k : nat), Param44.Rel (bounded_nat k) (bitvector k)
vecR : ∀ (A A' : Type) (AR : Param44.Rel A A') (k k' : nat)
       (kR : natR k k'), Param44.Rel (Vector.t A k) (Vector.t A' k')
(* equivalence between types (bounded_nat k) and (bitvector k') *)
bvR : ∀ (k k' : nat) (kR : natR k k'),
       Param44.Rel (bounded_nat k) (bitvector k')
(* informing Trocq with these equivalences *)
Trocq Use vecR natR boolR bvR.
```

Now, suppose we would like to transfer the following result from the bounded natural numbers to the vector-based encoding:
∀ (k : nat) (v : bounded_nat k) (i : nat) (b : Bool), i < k →
get (set v i b) i = b

As this goal involves `get` and `set` operations on bitvectors, and the order and equality relations on type `nat`, we inform `TROCQ` with the associated operations `getv` and `setv` on the vector encoding. E.g., for `get` and `getv`, we prove:

getR : ∀ (k k' : nat) (kR : natR k k')
(v : bounded_nat k) (v' : bitvector k') (vR : bvR k k' kR v v')
(n n' : nat) (nR : natR n n'), boolR (get v n) (getv v' n')

We can now use proof transfer from bitvectors to bounded natural numbers:

Trocq Use `eqR ltR`. (* where `eq` and `lt` are translated to themselves *)

Trocq Use `getR setR`.

Lemma `setBitGetSame`: $\forall (k : nat) (v : bitvector k)$,

$\forall (i : nat) (b : Bool), i < k \rightarrow getv (setv v i b) i = b.$

Proof. trocq. exact `setBitGetSame'`. (* same lemma, on bitvector *) Qed.

*Induction principle on integers. (code).* Recall that the problem from Example 2.2 is to obtain the following elimination scheme, from that available on type $\mathbb{N}$:

$\mathbb{N}_{ind} : \forall P : N \to \square, P \mathbb{O}_{N} \to (\forall n : N, P n \to P (S_{N} n)) \to \forall n : N, P n$

We first inform `TROCQ` that $\mathbb{N}$ and $\mathbb{N}$ are isomorphic, by providing proofs that the two conversions $\uparrow_{\mathbb{N}}: N \to \mathbb{N}$ and $\downarrow_{\mathbb{N}}: \mathbb{N} \to N$ are mutual inverses. Using lemma `Iso.toParam`, we can deduce an equivalence `Param44.Rel N N`, i.e., $\Box^{(4,4)} N N$. We also prove and register that zeros and successors are related:

Definition $N_R : Param44.Rel N N := ...$

Lemma $O_R : \text{rel } N_R O_N O_N$.

Lemma $S_R : \forall m n, \text{rel } N_R m n \to \text{rel } N_R (S_N m) (S_N n)$.

Trocq Use $N_R O_R S_R$.

`TROCQ` is now able to generate, prove and apply the desired implication:

Lemma $N_{ind} : \forall P : N \to \square, P \mathbb{O}_{N} \to (\forall n : N, P n \to P (S_{N} n)) \to \forall n : N, P n$.

Proof.

trocq. (* in the goal, N, O_N, S_N have been replaced by N, O_N, S_N *)

exact `nat_rect`.

Qed.

Inspecting this proof confirms that only information up to level (2<sub>a</sub>, 3) has been extracted from the equivalence proof $N_R$. It is thus possible to run the exact proof transfer, but with a weaker relation, as illustrated in the code for an abstract type *I* with a zero and a successor constants, and a retraction $\mathbb{N} \to I$.

## 8.2 Sections, retractions

*Modular arithmetic (code).* A typical application of modular arithmetic is to show that some statement on $\mathbb{Z}$ can be reduced to statements on $\mathbb{Z}/p\mathbb{Z}$, as pointed out by Example 2.4. Let us show how `TROCQ` can substitute $\mathbb{Z}$ for $\mathbb{Z}_9$ in the following statement:
Lemma `flt3_step : ∀ m n p : Z, (m * n * p % 3 ≠ 0 → m³ + n³ ≠ p³)%Z.`

where ` scope %Z ` is for the usual product, sum, modulo 3 and zero on type ` Z ` , and ` = ` is an equality test modulo 9 on type ` Z ` . A call to the ` trocq ` tactic turns the main goal of the proof into

∀ m n p : Z$_{9}$ , (m * n * p % 3 ≠ 0 → m³ + n³ ≠ p³)%Z$_{9}$ .

where ` scope %Z9 ` is for the usual product, sum, modulo 3 and zero on type ` Z9 ` . The ` trocq ` tactic automatically generated the following implication, which deduces a proof on ` Z from ` its modular analogues, reducing the quantification on all integers to a bounded quantification:

(∀ m n p : Z9 , m * n * p % 3 ≠ 0 → m³ + n³ ≠ p³)%Z9 →
(∀ m n p : Z , m * n * p % 3 ≠ 0 → m³ + n³ ≠ p³)%Z .

Types `Z9` and `Z` are obviously not equivalent, but a *retraction* is actually enough for this proof transfer. We have:

modp : Z → Z9
reprp : Z9 → Z
reprpK : ∀ (x : Z9), modp (reprp x) = x
Rp : Param42a.Rel Z Z9

where `Rp`, (a proof that `Φ<sup>(4,2a)</sup>Z Z9`), is obtained from `reprpK` via lemma `SplitSurj.toParam`. Performing this first step of the proof of lemma `flt3_step` by `trocq` now just requires relating the respective zeroes, additions, multiplications, reduction modulo 3 and equalities of the two types:

R0 : Rp 0%Z 0%Z9.
Radd : ∀ (m : Z) (x : Z9) (xR : Rp m x) (n : Z) (y : Z9) (yR : Rp n y), Rp (m + n)%Z (x + y)%Z9.
Rmul : ∀ (m : Z) (x : Z9) (xR : Rp m x) (n : Z) (y : Z9) (yR : Rp n y), Rp (m * n)%Z (x * y)%Z9.
Rmod3 : ∀ (n : Z) (x : Z9) (xR : Rp n x), Rp (n % 3)%Z (x % 3)%Z9.
Reqmodp : ∀ (m : Z) (x : Z9) (xR : Rp m x) (n : Z) (y : Z9) (yR : Rp n y),
Param01.Rel (m = n) (x = y).
Trocq Use Rp R0 Radd Rmul Rmod3 Reqmodp. (* informing Trocq with these relations *)

where `Param01.Rel P Q` (`Param01.Rel` is the Rocq/Coq name for `Φ<sup>(0,1)</sup>` ) is `Q → P` . Note that by definition of the relation given by `Rp`, lemma `Rmul` amounts to:

∀ (m n : Z), modp (m * n)%Z = (modp m * modp n)%Z9.

Summable sequences. (code). Given a sequence $(u_n)_{n \in \mathbb{N}}$ of non-negative real numbers, i.e., a function $u : \mathbb{N} \to [0, +\infty[$, $u$ is said to be *summable* when the sequence $(\sum_{k=0}^{n} u_k)_{n \in \mathbb{N}}$ has a finite limit, denoted $\sum u$. Now for two summable sequences $u$ and $v$, it is easy to see that $u + v$, the sequence obtained by point-wise addition of $u$ and $v$, is also a summable sequence, and that:

$$
\sum (u + v) = \sum u + \sum v \tag{19}
$$

As expression $\sum u$ only makes sense when $u$ is a summable sequence, any algebraic operation “under the sum”, e.g., rewriting $\sum (u+(v+w))$ into $\sum ((w+u)+v)$, a priori requires a proof of summability for every rewriting step. In a classical setting, the standard approach rather assigns a default value to the case of an infinite sum, and introduces an extended domain $[0, +\infty]$. Algebraic operations on real numbers, like addition, are extended to the extra $+\infty$ case. Now for a sequence $u : \mathbb{N} \to [0, +\infty]$, the limit $\sum u$ is always defined, as increasing partial sums either converge to a finite limit, or diverge to $+\infty$. The road map is then to first prove that Equation 19 holds for any two sequences of extended
non-negative numbers. The result is then transferred to the special case of summable sequences of non-negative numbers. Major libraries of formalized mathematics including Lean's mathlib [43], Isabelle/HOL's Archive of Formal Proofs, coq-interval [42] or Rocq/Coq's mathcomp-analysis [1], resort to such extended domains and transfer steps, notably for defining measure theory. Yet, as reported by expert users [33], the associated transfer bureaucracy is essentially done manually and thus significantly clutters formal developments in real and complex analysis, probabilities, etc. We show how to deal with this example with TROCQ.

This example involves two instances of subtypes: type $\overline{\mathbb{R}}_{\ge 0}$ extends a type $\mathbb{R}_{\ge 0}$ of positive real numbers with an abstract element and type `summable` is for provably convergent sequences of positive real numbers:

Inductive $\overline{\mathbb{R}}_{\ge 0}$: Type := Fin : $\overline{\mathbb{R}}_{\ge 0} \to \overline{\mathbb{R}}_{\ge 0}$ | Inf : $\overline{\mathbb{R}}_{\ge 0}$.

Definition seq$_{\overline{\mathbb{R}}_{\ge 0}}$ := nat $\to \overline{\mathbb{R}}_{\ge 0}$. Definition seq$_{\overline{\mathbb{R}}_{\ge 0}}$ := nat $\to \overline{\mathbb{R}}_{\ge 0}$.

Record summable := {to_seq :> seq$_{\overline{\mathbb{R}}_{\ge 0}}$; _ : isSummable to_seq}.

Type $\overline{\mathbb{R}}_{\ge 0}$ and $\mathbb{R}_{\ge 0}$ are related at level (4, 2<sub>b</sub>): e.g., truncate : $\overline{\mathbb{R}}_{\ge 0} \to \mathbb{R}_{\ge 0}$ provides a partial inverse to the Fin injection by sending the extra Inf to zero. Types summable and seq$_{\overline{\mathbb{R}}_{\ge 0}}$ are also related at level (4, 2<sub>b</sub>), via the relation:

Definition Rrseq (u : summable) (v : seq$_{\overline{\mathbb{R}}_{\ge 0}})$ : Type := seq_extend u = v.

where `seq_extend` transforms a summable sequence into a sequence of extended positive reals in the obvious way. Now $\Sigma_{\overline{\mathbb{R}}_{\ge 0}} u : \overline{\mathbb{R}}_{\ge 0}$ is the sum of a sequence $u : \text{seq}_{\overline{\mathbb{R}}_{\ge 0}}$ of extended positive reals, and we also define the sum of a sequence of positive reals, as a positive real, again by defaulting infinite sums to zero. For the purpose of the example, we only do so for summable sequences:

Definition $\Sigma_{\overline{\mathbb{R}}_{\ge 0}}$ ($u$ : summable) : $\overline{\mathbb{R}}_{\ge 0}$ := truncate ($\Sigma_{\overline{\mathbb{R}}_{\ge 0}}$ ($\text{seq_extend}$ $u$)).

These two notions of sums are related via `Rrseq`, and so are the respective additions of positive (resp. extended positive) reals and the respective pointwise additions of sequences. Once `TROCQ` is informed of these relations, the tactic is able to transfer the statement from the much easier variant on extended reals:

(* relating type $\overline{\mathbb{R}}_{\ge 0}$ and $\mathbb{R}_{\ge 0}$ and their respective equalities *)

Trocq Use Param01_paths Param42b_nnr.

(* relating sequence types, sums, addition, addition of sequences *)

Trocq Use Param4a_rseq R_sum_xnnR R_add_xnnR seq_nnr_add.

Lemma sum_xnnR_add : ∀ (u v : $\overline{\mathbb{R}}_{\ge 0}$), $\Sigma_{\overline{\mathbb{R}}_{\ge 0}}$ (u + v) = $\Sigma_{\overline{\mathbb{R}}_{\ge 0}}$ u + $\Sigma_{\overline{\mathbb{R}}_{\ge 0}}$ v.

Proof. (...) Qed. (* easy, as no convergence proof is needed *)

Lemma sum_nnr_add : ∀ (u v : $\overline{\mathbb{R}}_{\ge 0}$), $\Sigma_{\overline{\mathbb{R}}_{\ge 0}}$ (u + v) = $\Sigma_{\overline{\mathbb{R}}_{\ge 0}}$ u + $\Sigma_{\overline{\mathbb{R}}_{\ge 0}}$ v.

Proof. trocq; exact sum_xnnR_add. Qed.

## 8.3 Polymorphic, dependent types

*Polymorphic parameters (code)*. Suppose we want to transfer a goal involving lists along an equivalence between the types of the values contained in the lists. We first prove that the `list` type former is equivalent to itself, and register this fact:
listR : ∀ A A' (AR : Param44.Rel A A'), Param44.Rel (list A) (list A')
Trocq Use listR.

We also need to relate with themselves all operations on type `list` involved in the goal, including constructors, and to register these facts, before `TROCQ` is able to transfer any goal, e.g., about `list N` to its analogue on `list N`.

Note that lemma `listR` requires an *equivalence* between its parameters. If this does not hold, as in the case of type `Z` and `Z₉` from Section 8.2, the translation is stuck: weakening does not apply here. In order to avoid stuck translation, we need several versions of `listR` to cover all cases. For instance, the following lemma is required for proof transfers from `list Z₉` to `list Z`.

listR2a4 : ∀ A A' (AR : Param2a4.Rel A A'), Param2a4.Rel (list A) (list A').

*Dependent and polymorphic types (code)*. Fixed-size vectors can be represented by iterated tuples, an alternative to the inductive type `Vector.t`, from Rocq/Coq's standard library, as follows.

Definition tuple (A : Type) : nat → Type := fix F n ::= match n with O => Unit | S n' => F n' * A end.

On the following mockup example, `TROCQ` transfers a lemma on `Vector.t` to its analogue on `tuple`, about a function `head : ∀ A n, tuple A (S n) → A`, and a function `const : ∀ A, A → ∀ n, tuple A n` creating a constant vector, and simultaneously refines integers into the integers modulo `p` from Section 8.1:

Lemma head_cst (n : nat) (i : Z) : Vector.hd (Vectorigation const i (S n)) = i.
Proof. destruct n; simpl; reflexivity. Qed. (* easy proof *)

Lemma head_cst' : ∀ (n : nat) (z : Z₉), head (const z (S n)) = z.
Proof. trocq. exact head_const. Qed.

This automated proof only requires proving (and registering) that `head` and `const` are related to their analogue `Vector.hd` and `Vectorigation`, from Rocq/Coq's standard library. Note that the proof uses the equivalence between `Vector.t` and `tuple` but only requires a retraction between parameter types.

## 9 Related work

The literature dealing with proof transfer in interactive theorem proving roughly falls in two camps. A first line of work concerns the design of practical tools for automating the synthesis of mundane parts of formal developments by *reusing* some pre-existing formal proofs to inform this synthesis. The tools may operate on proof scripts or on proof terms, the latter being more directly connected to the present work.

In this context, the synthesis procedure is most often heuristic. In particular, it is not expected to produce any formal guarantee of the relation between the pre-existing proof term and the synthesized one, as type-checking suffices to validate a candidate proof term. Barthe and Pons [11] already noticed that the computational content of type isomorphisms can serve proof transfer. The first implementation report of a tool based on this idea appeared soon after [41]. This meta-program implemented a proof rewriting heuristic producing, from an existing proof term of a certain statement, a candidate proof term of a modified statement, with no formal guarantee – not even that of being well-typed. The rise of interactive theorem proving for program verification,
in particular outside academia, highlighted the crucial need for better formal proof engineering methods and tools. In particular, *proof repair* techniques aim at providing a better support for synchronizing an evolving code base with its formal guarantees of correctness. This question is taken in a broader sense than the formalization of proof transfer provided in Section 3.1, as it may concern programs written outside of the logic, and may involve inferring program alignments, invariants, etc. [32]. Some of the corresponding tools however are designed to repair proofs of internal programs to the type theory backing the interactive prover. For instance, Pumpkin Pi provides a comprehensive proof repair toolset for *repairing* proofs after changing certain datatypes for equivalent ones [49, 60].

A second line of work corresponds to proof transfer in the sense of Section 3.1: by contrast with the previous angle, a central issue in this case is the synthesis of a proof term witnessing that two certain terms are related. Generalized rewriting [50], which generalizes setoid rewriting to preorders, is actually a variant of proof transfer, albeit within the same type. As such, it allows in particular rewriting under binders. The restriction to homogeneous relations however excludes more general instances of proof transfer. For instance, datatype representation change and quasi-PERs (QPER, or zig-zag complete relations) [37] are inherently heterogeneous.

The other proof transfer methods we are aware of all address the case of heterogeneous relations. Incidentally, they can thus also be used for the homogeneous case, and therefore for generalized rewriting, although this special case is seldom emphasized. The Coq Effective Algebra Library (CoqEAL) [23, 28] and the Isabelle/HOL transfer package [34, 35, 38, 39], pioneered the use of parametricity-based methods for proof transfer, motivated by the refinement of proof-oriented data-structures to computation-oriented counterparts. Together with a subsequent generalization of the CoqEAL approach [64], these tools address the case of a transfer between a subtype of a certain type A and a quotient of a certain type B, i.e., the case of a trivial QPER in which the zig-zag morphism is a surjection from A to B.

Modern approaches to proof transfer rely on univalence, either as an axiom, in the case of univalent parametricity [53] or as a computing primitive [8]. Key ingredients of univalent parametricity were already present in earlier seemingly unpublished work [6], implemented using an ancestor of the MetaCoq library [51]. Another recent line of work consists in studying to which extent the structural propagation of certain relations can be internalized in a type theory [4, 40, 58].

The columns of Table 1 list the aforementioned tools in chronological order, and they indicate when the features listed as lines are available (✔), not available (X) or only partially available (✔). By partially available we mean that the given tool may handle subcases of the given feature (for example TROCQ currently only handles subrelations in our hierarchy). The first line distinguishes methods than can address heterogeneous relations from those restricted to homogeneous ones. While the oldest tool operates via a monolithic translation of an input proof term, others rather prove an internal implication lemma. *Anticipation* [53] refers to the need to define a dedicated structure for the signature to be transported. *Binders* (V) can prevent transfer, as well as dependent types. The latter generally requires a univalence principle, which can be a global assumption or, as in the case of TROCQ, an optional ingredient.

# 10 Conclusion

The TROCQ framework can be seen as a generalization of both the raw [15, 36] and the univalent [53] parametricity translations. In particular, it allows for combining and for synthesizing proofs of a whole palette of relations between arbitrary types, when the univalent translation can only deal with equivalences. This framework implements a fine-grained analysis of the resources needed to compute an expected translation. Incidentally, the framework actually provides a better variant of univalent parametricity, since the latter is able to detect when the univalence axiom is not needed,
<table><caption>Table 1. Comparison of proof transfer automation devices</caption><thead><tr><th></th><th>Magaud [41]</th><th>Setoid rewrite [50]</th><th>CoqEAL [23]</th><th>Transfer [38]</th><th>Zimmermann et al. [64]</th><th>UPARAM [53]</th><th>Int. Repr. Indep. [8]</th><th>Trackt [17]</th><th>TROCQ</th></tr></thead><tbody><tr><td>Heterogen. rel.</td><td>✓</td><td>✗</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Internal</td><td>✗</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>No anticipation</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✗</td><td>✓</td><td>✓</td></tr><tr><td>Under ∀</td><td>✓</td><td>✓</td><td>✗</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td>Dep. types</td><td>✓</td><td>✗</td><td>✗</td><td>✗</td><td>✗</td><td>✓</td><td>✓</td><td>✗</td><td>✓</td></tr><tr><td>Univalence-free</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✓</td><td>✗</td><td>✗</td><td>✓</td><td>✓</td></tr><tr><td>Subrelations</td><td>✗</td><td>✓</td><td>✗</td><td>✗</td><td>✗</td><td>✗</td><td>✗</td><td>✗</td><td>✓</td></tr><tr><td>QERs</td><td>✗</td><td>✓</td><td>✓</td><td>✓</td><td>✗</td><td>✓</td><td>✓</td><td>✗</td><td>✓</td></tr><tr><td>Subtyping</td><td>✗</td><td>✗</td><td>✓</td><td>✓</td><td>✗</td><td>✗</td><td>✓</td><td>✓</td><td>✓</td></tr><tr><td></td><td>Coq</td><td>Coq</td><td>Coq</td><td>Isabelle/HOL</td><td>Coq</td><td>HoTT</td><td>Cubical Agda</td><td>Rocq/Coq</td><td>Rocq/Coq or HoTT</td></tr></tbody></table>

when the original variant pulls it in by default. This scrutiny allows in particular to get rid of the univalence axiom for a larger class of equivalence proofs [52], and to deal with refinement relations for arbitrary terms, unlike the CoqEAL library [23].

This analysis is enabled by skolemizing the usual symmetrical presentation of equivalence, so as to expose the data, and by introducing a hierarchy of algebraic structures for relations. Altenkirch and Kaposi already proposed a symmetrical, skolemized phrasing of type equivalence [5], but for different purposes. Definition 5.4 however slightly differs from theirs: by reducing the amount of transport involved, it eases formal proofs significantly in practice, both in the internal library of TROCQ and for end-users of the tactic. In practice, an important feature of the resulting hierarchy of structures for relations is that weaker structures are literally *included* in richer ones. This feature is indeed a crucial invariant for hierarchies implemented in intensional dependent type theory, which should preserve the definitional confluence of inheritance paths [2]. As such, it fulfills the standards enforced by principled instruments for the management of hierarchies [24], although current, independent technical limitations of the latter regarding universe polymorphism prevented us from using them in our plugin. We conjecture that this hierarchy can be enriched further with more interesting structures for relations.

Another obvious future direction of improvement for TROCQ is to extend it to the full calculus of constructions with inductive types (CIC). This requires providing an automated way to produce families of TROCQ translations for inductive types, indexed by the desired output annotations. Raw parametricity translations of for CIC have been described for several variants of inductive type presentations [13, 14, 36], but not their extension to univalent parametricity. The gallery of examples available with the TROCQ plugin includes a manual translation for several inductive types with parameters and indices such as `Empty`, `bool` (enumerated), `nat` (recursive, no parameter), `option`, `prod`, `sum`, `sigma` (non recursive, with parameters), `list` (recursive with parameters), `eq` / `paths` (non recursive, with parameter and index) and `vector` (recursive with parameter and index). These examples strongly suggest that this generation could be automated.
Using TROCQ in a context featuring axioms is possible but classical axioms should be handled with
care. Indeed, TROCQ is conservative over raw parametricity, and some classical axioms are known
not to be parametric. For instance, postulating the existence of a (raw) parametricity translation for
the Law of Excluded Middle is inconsistent. This means that one cannot hope in general to use
TROCQ on statements that mention classical axioms explicitly. Specific cases might work however:
if they only occur in proofs but not in statements, or if definitions featuring such axioms remain
parametric. From our experience, this remark makes TROCQ useful in most scenarios, even when
formalizing classical mathematics.

The concrete output of this work is a plugin [22] that consists of about 3000 l. of Rocq/Coq
proofs and 1200 l. of meta-programming, in the Elpi meta-language, excluding white lines and
comments. This plugin goes beyond the state of the art in two ways. First, it demonstrates that a
single implementation of this parametricity framework covers the core features of several existing
other tactics, for refinements [23, 28], generalized rewriting [50], and proof transfer [53]. Second,
it addresses use cases, such as those of Section 8.2, that are beyond the skills of any existing tool
in any proof assistant based on type theory. The logic programming paradigm provided by the
Elpi meta-language proved perfectly well-suited for implementing this nature of proof search.
The prototype plugin however arguably still needs an improved user interface so as to reach the
maturity of some of the aforementioned existing tactics. It would also benefit from an automated
generation of equivalence proofs, such as Pumpkin Pi [49].

Acknowledgments

The authors are extremely grateful to András Kovács, Kenji Maillard, Enrico Tassi, Quentin Ver-
mande, Théo Winterhalter, to anonymous members of the ESOP 2024 program committee and to
the anonymous reviewers of the present submission for their helpful comments and suggestions.

References

[1] Reynald Affeldt and Cyril Cohen. 2023. Measure Construction by Extension in Dependent Type Theory with Application to Integration. arXiv:2209.02345 [cs.LO] accepted for publication in JAR.

[2] Reynald Affeldt, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, and Kazuhiko Sakaguchi. 2020. Competing inheritance paths in dependent type theory: a case study in functional analysis. In *IJCAR 2020 - International Joint Conference on Automated Reasoning*. Paris, France, 1–19. doi:10.1007/978-3-030-51054-1_1

[3] Xavier Allamigeon, Quentin Canu, and Pierre-Yves Strub. 2023. A Formal Disproof of Hirsch Conjecture. In *Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023*, Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic (Eds.). ACM, 17–29. doi:10.1145/3573105.3575678

[4] Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, and Michael Shulman. 2024. Internal Parametricity, without an Interval. *Proc. ACM Program. Lang.* 8, POPL (2024), 2340–2369. doi:10.1145/3632920

[5] Thorsten Altenkirch and Ambrus Kaposi. 2015. Towards a Cubical Type Theory without an Interval. In *TYPES (LIPIcs, Vol. 69)*. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 3:1–3:27. doi:10.4230/LIPIcs.TYPES.2015.3

[6] Abhishek Anand and Greg Morrisett. 2017. Revisiting Parametricity: Inductives and Uniformity of Propositions. *CoRR* abs/1705.01163 (2017). arXiv:1705.01163 http://arxiv.org/abs/1705.01163

[7] Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), and Daniel R. Licata. 2021. Syntax and models of Cartesian cubical type theory. *Math. Struct. Comput. Sci.* 31, 4 (2021), 424–468. doi:10.1017/S0960129521000347

[8] Carlo Angiuli, Evan Cavallo, Anders Mörtberg, and Max Zeuner. 2021. Internalizing representation independence with univalence. *Proc. ACM Program. Lang.* 5, POPL (2021), 1–30. doi:10.1145/3434293

[9] David Aspinall and Adriana B. Compagnoni. 2001. Subtyping dependent types. *Theor. Comput. Sci.* 266, 1-2 (2001), 273–309. doi:10.1016/S0304-3975(00)00175-4

[10] Gilles Barthe, Venanzio Capretta, and Olivier Pons. 2003. Setoids in type theory. *J. Funct. Program.* 13, 2 (2003), 261–293. doi:10.1017/S0956796802004501

[11] Gilles Barthe and Olivier Pons. 2001. Type Isomorphisms and Proof Reuse in Dependent Type Theory. In *Foundations of Software Science and Computation Structures*, Furio Honsell and Marino Miculan (Eds.). Springer Berlin Heidelberg,
Berlin, Heidelberg, 57–71.

[12] Andrej Bauer, Jason Gross, Peter LeFanu Lumsdaine, Michael Shulman, Matthieu Sozeau, and Bas Spitters. 2017. The HoTT library: a formalization of homotopy type theory in Coq. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, Yves Bertot and Viktor Vafeiadis (Eds.). ACM, 164–172. doi:10.1145/3018610.3018615

[13] Jean-Philippe Bernardy, Patrik Jansson, and Ross Paterson. 2012. Proofs for free - Parametricity for dependent types. J. Funct. Program. 22, 2 (2012), 107–152. doi:10.1017/S0956796812000056

[14] Jean-Philippe Bernardy and Marc Lasson. 2011. Realizability and Parametricity in Pure Type Systems. In Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings (Lecture Notes in Computer Science, Vol. 6604), Martin Hofmann (Ed.). Springer, 108–122. doi:10.1007/978-3-642-19805-2_8

[15] Jean-Philippe Bernardy and Guilhem Moulin. 2012. A Computational Interpretation of Parametricity. In Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, LICS 2012, Dubrovnik, Croatia, June 25-28, 2012. IEEE Computer Society, 135–144. doi:10.1109/LICS.2012.25

[16] Sandrine Blazy. 2024. On Mechanized Semantics for Verified Compilation. Interview at the occasion of her invited talk at the ESOP 2024 conference. https://etaps.org/blog/017-sandrine-blazy/.

[17] Valentin Blot, Denis Cousineau, Enzo Crance, Louise Dubois de Prisque, Chantal Keller, Assia Mahboubi, and Pierre Vial. 2023. Compositional Pre-processing for Automated Reasoning in Dependent Type Theory. In Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023, Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, and Steve Zdancewic (Eds.). ACM, 63–77. doi:10.1145/3573105.3575676

[18] Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. 2017. The next 700 syntactical models of type theory. In Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, Paris, France, January 16-17, 2017, Yves Bertot and Viktor Vafeiadis (Eds.). ACM, 182–194. doi:10.1145/3018610.3018620

[19] Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. 2018. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In 21st International Conference on Types for Proofs and Programs (TYPES 2015) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 69), Tarmo Uustalu (Ed.). Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany, 5:1–5:34. doi:10.4230/LIPIcs.TYPES.2015.5

[20] Cyril Cohen, Enzo Crance, and Assia Mahboubi. 2024. Artifact Report: Trocq: Proof Transfer for Free, With or Without Univalence. In Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 14576), Stephanie Weirich (Ed.). Springer, 269–274. doi:10.1007/978-3-031-57262-3_11

[21] Cyril Cohen, Enzo Crance, and Assia Mahboubi. 2024. Trocq: Proof Transfer for Free, With or Without Univalence. In Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I (Lecture Notes in Computer Science, Vol. 14576), Stephanie Weirich (Ed.). Springer, 239–268. doi:10.1007/978-3-031-57262-3_10

[22] Cyril Cohen, Enzo Crance, and Assia Mahboubi. 2025. rocq-community/trocq: Trocq 0.1.8+prop. doi:10.5281/zenodo.14846664

[23] Cyril Cohen, Maxime Dénès, and Anders Mörtberg. 2013. Refinements for Free!. In Certified Programs and Proofs - Third International Conference, CPP 2013, Melbourne, VIC, Australia, December 11-13, 2013, Proceedings (Lecture Notes in Computer Science, Vol. 8307), Georges Gonthier and Michael Norrish (Eds.). Springer, 147–162. doi:10.1007/978-3-319-03545-1_10

[24] Cyril Cohen, Kazuhiko Sakaguchi, and Enrico Tassi. 2020. Hierarchy Builder: algebraic hierarchies made easy in Coq with Elpi. In FSCD 2020 - 5th International Conference on Formal Structures for Computation and Deduction. Paris, France, 34:1–34:21. doi:10.4230/LIPIcs.FSCD.2020.34

[25] Thierry Coquand and Gérard P. Huet. 1988. The Calculus of Constructions. Inf. Comput. 76, 2/3 (1988), 95–120. doi:10.1016/0890-5401(88)90005-3

[26] Leonardo de Moura and Sebastian Ullrich. 2021. The Lean 4 Theorem Prover and Programming Language. In Automated Deduction - CADE 28 - 28th International Conference on Automated Deduction, Virtual Event, July 12-15, 2021, Proceedings (Lecture Notes in Computer Science, Vol. 12699), André Platzer and Geoff Sutcliffe (Eds.). Springer, 625–635. doi:10.1007/978-3-030-79876-5_37

[27] Benjamin Delaware, Clément Pit-Claudel, Jason Gross, and Adam Chlipala. 2015. Fiat: Deductive Synthesis of Abstract Data Types in a Proof Assistant. In Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2015, Mumbai, India, January 15-17, 2015, Sriram K. Rajamani and David Walker (Eds.).
ACM, 689–700. doi:10.1145/2676726.2677006

[28] Maxime Dénès, Anders Mörtberg, and Vincent Siles. 2012. A Refinement-Based Approach to Computational Algebra in Coq. In *Interactive Theorem Proving*, Lennart Beringer and Amy Felty (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 83–98. doi:10.1007/978-3-642-32347-8_7

[29] Cvetan Dunchev, Ferruccio Guidi, Claudio Sacerdoti Coen, and Enrico Tassi. 2015. ELPI: Fast, Embeddable, λProlog Interpreter. In *Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015*, Suva, Fiji, November 24-28, 2015, *Proceedings (Lecture Notes in Computer Science, Vol. 9450)*, Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov (Eds.). Springer, 460–468. doi:10.1007/978-3-662-48899-7_32

[30] Thom Frühwirth and Frank Raiser. 2011. Constraint Handling Rules: Compilation, Execution, and Analysis.

[31] Gaëtan Gilbert, Jesper Cockx, Matthieu Sozeau, and Nicolas Tabareau. 2019. Definitional proof-irrelevance without K. *Proc. ACM Program. Lang.* 3, POPL (2019), 3:1–3:28. doi:10.1145/3290316

[32] Kiran Gopinathan, Mayank Keoliya, and Ilya Sergey. 2023. Mostly Automated Proof Repair for Verified Libraries. *Proc. ACM Program. Lang.* 7, PLDI (2023), 25–49. doi:10.1145/3591221

[33] Sébastien Gouëzel. 2021. Vitali-Carathódory theorem in mathlib. https://leanprover-community.github.io/mathlib_docs/measure_theory/integral/vitali_caratheodory.html.

[34] Florian Haftmann, Alexander Krauss, Ondřej Kunčar, and Tobias Nipkow. 2013. Data Refinement in Isabelle/HOL. In *Interactive Theorem Proving*, Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 100–115.

[35] Brian Huffman and Ondřej Kunčar. 2013. Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL. In *Certified Programs and Proofs*, Georges Gonthier and Michael Norrish (Eds.). Springer International Publishing, Cham, 131–146.

[36] Chantal Keller and Marc Lasson. 2012. Parametricity in an Impredicative Sort. In *Computer Science Logic (CSL’12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, September 3-6, 2012, Fontainebleau, France (LIPIcs, Vol. 16)*, Patrick Cégnielski and Arnaud Durand (Eds.). Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 381–395. doi:10.4230/LIPIcs.CSL.2012.381

[37] Neelakantan R. Krishnaswami and Derek Dreyer. 2013. Internalizing Relational Parametricity in the Extensional Calculus of Constructions. In *Computer Science Logic 2013 (CSL 2013) (Leibniz International Proceedings in Informatics (LIPIcs), Vol. 23)*, Simona Ronchi Della Rocca (Ed.). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, Dagstuhl, Germany, 432–451. doi:10.4230/LIPIcs.CSL.2013.432

[38] Peter Lammich. 2013. Automatic Data Refinement. In *Interactive Theorem Proving*, Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 84–99.

[39] Peter Lammich and Andreas Lochbihler. 2019. Automatic Refinement to Efficient Data Structures: A Comparison of Two Approaches. *J. Autom. Reason*, 63, 1 (2019), 53–94. doi:10.1007/s10817-018-9461-9

[40] Théo Laurent, Meven Lennon-Bertrand, and Kenji Maillard. 2024. Definitional Factoriality for Dependent (Sub)Types. In *Programming Languages and Systems - 33rd European Symposium on Programming, ESOP 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software*, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, *Proceedings, Part I (Lecture Notes in Computer Science, Vol. 14576)*, Stephanie Weirich (Ed.). Springer, 302–331. doi:10.1007/978-3-031-57262-3_13

[41] Nicolas Magaud. 2003. Changing Data Representation within the Coq System. In *TPHOLs’2003*, Vol. 2758. LNCS, Springer-Verlag. http://www.springerlink.com/openurl.asp?genre=article&issn=0302-9743&volume=2758&spage=87 © Springer-Verlag.

[42] Érik Martin-Dorel and Guillaume Melquiond. 2016. Proving Tight Bounds on Univariate Expressions with Elementary Functions in Coq. *J. Autom. Reason*, 57, 3 (2016), 187–217. doi:10.1007/s10817-015-9350-4

[43] The mathlib Community. 2020. The Lean mathematical library. In *Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, New Orleans, LA, USA, January 20-21, 2020*, Jasmin Blanchette and Catalin Hritcu (Eds.). ACM, 367–381. doi:10.1145/3372885.3373824

[44] John C. Mitchell. 1986. Representation Independence and Data Abstraction. In *Conference Record of the Thirteenth Annual ACM Symposium on Principles of Programming Languages*, St. Petersburg Beach, Florida, USA, January 1986. ACM Press, 263–276. doi:10.1145/512644.512669

[45] Rob Nederpelt and Herman Geuvers. 2014. *Type Theory and Formal Proof: An Introduction*. Cambridge University Press. doi:10.1017/CBO9781139567725

[46] Ulf Norell. 2008. Dependently Typed Programming in Agda. In *Advanced Functional Programming, 6th International School, AFP 2008, Heijen, The Netherlands, May 2008, Revised Lectures (Lecture Notes in Computer Science, Vol. 5832)*, Pieter W. M. Koopman, Rinus Plasmeijer, and S. Doaitse Swierstra (Eds.). Springer, 230–266. doi:10.1007/978-3-642-04652-0_5

[47] Christine Paulin-Mohring. 2015. Introduction to the Calculus of Inductive Constructions. In *All about Proofs, Proofs for All*, Bruno Woltzenlogel Paleo and David Delahaye (Eds.). Studies in Logic (Mathematical logic and foundations), Vol. 55. College Publications. https://inria.hal.science/hal-01094195
[48] John C. Reynolds. 1983. Types, Abstraction and Parametric Polymorphism. In *Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, France, September 19-23, 1983*, R. E. A. Mason (Ed.). North-Holland/IFIP, 513-523.

[49] Talia Ringer, RanDair Porter, Nathaniel Yazdani, John Leo, and Dan Grossman. 2021. Proof repair across type equivalences. In *PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, Virtual Event, Canada, June 20-25, 2021*, Stephen N. Freund and Eran Yahav (Eds.). ACM, 112-127. doi:10.1145/3453483.3454033

[50] Matthieu Sozeau. 2009. A New Look at Generalized Rewriting in Type Theory. *J. Formaliz. Reason.* 2, 1 (2009), 41-62. doi:10.6092/issn.1972-5787/1574

[51] Matthieu Sozeau, Abhishek Anand, Simon Boulier, Cyril Cohen, Yannick Forster, Fabian Kunze, Gregory Malecha, Nicolas Tabareau, and Théo Winterhalter. 2020. The MetaCoq Project. *J. Autom. Reason.* 64, 5 (2020), 947-999. doi:10.1007/s10817-019-09540-0

[52] Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau. 2018. Equivalences for free: univalent parametricity for effective transport. *Proc. ACM Program. Lang.* 2, ICFP, Article 92 (jul 2018), 29 pages. doi:10.1145/3236787

[53] Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau. 2021. The Marriage of Univalence and Parametricity. *J. ACM* 68, 1, Article 5 (jan 2021), 44 pages. doi:10.1145/3429979

[54] Enrico Tassi. 2019. Deriving proved equality tests in Coq-elpi: Stronger induction principles for containers in Coq. In *ITP 2019 - 10th International Conference on Interactive Theorem Proving*. Portland, United States. doi:10.4230/LIPIcs.CVIT.2016.23

[55] The Coq Development Team. 2024. *The Coq Proof Assistant*. doi:10.5281/zenodo.14542673

[56] The Rocq Development Team. 2025. *The Rocq Prover*. doi:10.5281/zenodo.15149629

[57] The Univalent Foundations Program. 2013. *Homotopy Type Theory: Univalent Foundations of Mathematics*. https://homotopytypetheory.org/book, Institute for Advanced Study.

[58] Antoine Van Muylder, Andreas Nuyts, and Dominique Devriese. 2024. Internal and Observational Parametricity for Cubical Agda. *Proc. ACM Program. Lang.* 8, POPL (2024), 209-240. doi:10.1145/3632850

[59] Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. 2019. Cubical agda: a dependently typed programming language with univalence and higher inductive types. *Proc. ACM Program. Lang.* 3, ICFP (2019), 87:1-87:29. doi:10.1145/3341691

[60] Cosmo Viola, Max Fan, and Talia Ringer. 2024. Proof Repair across Quotient Type Equivalences. (2024). https://arxiv.org/abs/2310.06959v5

[61] Philip Wadler. 1989. Theorems for Free! In *Proceedings of the fourth international conference on Functional programming languages and computer architecture, FPCA 1989, London, UK, September 11-13, 1989*, Joseph E. Stoy (Ed.). ACM, 347-359. doi:10.1145/99370.99404

[62] Conrad Watt, Maja Trela, Peter Lammich, and Florian Märkl. 2023. WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly. *Proc. ACM Program. Lang.* 7, PLDI (2023), 100-123. doi:10.1145/3591224

[63] Yu Zhang, Jérémie Koenig, Zhong Shao, and Yuting Wang. 2025. Unifying Compositional Verification and Certified Compilation with a Three-Dimensional Refinement Algebra. *Proc. ACM Program. Lang.* 9, POPL (2025), 1903-1933. doi:10.1145/3704900

[64] Théo Zimmermann and Hugo Herbelin. 2015. Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant. In *Conference on Intelligent Computer Mathematics*. Washington, D.C., United States. https://hal.science/hal-01152588