Nicolas Tabareau

Éric Tanter

Matthieu Sozeau

The Marriage of Univalence and Parametricity

Keywords: CCS Concepts:, Theory of computation → Type theory, Type structures, Program reasoning Type Equivalence, Univalence, Parametricity, Proof Assistants, Coq positive → Bin Inductive positive : Set := | xI : positive → positive | xO : positive → positive | xH : positive

Reasoning modulo equivalences is natural for everyone, including mathematicians. Unfortunately, in proof assistants based on type theory, which are frequently used to mechanize mathematical results and carry out program verification efforts, equality is appallingly syntactic and, as a result, exploiting equivalences is cumbersome at best. Parametricity and univalence are two major concepts that have been explored in the literature to transport programs and proofs across type equivalences, but they fall short of achieving seamless, automatic transport. This work first clarifies the limitations of these two concepts when considered in isolation, and then devises a fruitful marriage between both. The resulting concept, called univalent parametricity, is an extension of parametricity strengthened with univalence that fully realizes programming and proving modulo equivalences. Our approach handles both type and term dependency, as well as type-level computation. In addition to the theory of univalent parametricity, we present a lightweight framework implemented in the Coq proof assistant that allows the user to transparently transfer definitions and theorems for a type to an equivalent one, as if they were equal. For instance, this makes it possible to conveniently switch between an easy-to-reason-about representation and a computationally-efficient representation, as soon as they are proven equivalent. The combination of parametricity and univalence supports transport à la carte: basic univalent transport, which stems from a type equivalence, can be complemented with additional proofs of equivalences between functions over these types, in order to be able to transport more programs and proofs, as well as to yield more efficient terms. We illustrate the use of univalent parametricity on several examples, including a recent integration of native integers in Coq. This work paves the way to easier-to-use proof assistants by supporting seamless programming and proving modulo equivalences.

INTRODUCTION

If mathematics is the art of giving the same name to different things, programming is the art of computing the same thing with different means. That sameness notion ought to be equivalence. Unfortunately, in programming languages as well as proof assistants such as Coq [Coq Development Team 2019] and Agda [START_REF] Norell | Dependently Typed Programming in Agda[END_REF]], the notion of sameness or equality is appallingly syntactic. In dependently-typed languages that also serve as proof assistants, equivalences can be stated and manually exploited, but they cannot be used as transparently and conveniently as syntactic or propositional equality. The benefits we ought to get from having equivalence as the primary notion of sameness include the possibility to state and prove results about a data structure (or mathematical object) that is convenient to formally reason about, and then automatically transport these results to other structures, for instance ones that are computationally more efficient, albeit less convenient to reason about.

Let us consider two equivalent representations of natural numbers available in the Coq proof assistant (Figure 1): Peano natural numbers N, with constructors O and S, and binary natural numbers Bin, which denote a sequence of bits with a leading 1. Defining functions over N and reasoning about them is simple. For instance, + N : N → N → N is a simple induction on the first argument, and proving that addition is commutative is similarly direct. Conversely, addition on binary natural numbers + Bin : Bin → Bin → Bin is defined with three functions-two mutuallyrecursive functions on positive and a simple function-making most reasoning much more involved. The other side of the comparison is that computing with N is much less efficient (if at all possible!) than computing with Bin. Ideally, one would want to apply easy inductive reasoning on N to establish properties of efficient functions defined on Bin.

The Challenge of Automatic Transport. An equivalence between N and Bin consists of two transport functions ↑ N : Bin → N and ↑ Bin : N → Bin together with the proof that they are inverse of each other. Manually exploiting such an equivalence in order to transport properties on N to properties on Bin is however challenging, even for simple properties.

Consider the commutativity of addition on N:

Definition + N _comm : ∀ (n m : N), n + N m = m + N n. (* simple inductive proof *)
from which one would like to deduce the commutativity of addition on Bin:

Definition + Bin _comm : ∀ (n m : Bin). n + Bin m = m + Bin n.

A proof of + Bin _comm that exploits + N _comm and the N-Bin equivalence would proceed as follows: Observe how one is forced to explicitly rewrite and reason about transports at each step. In particular, step 3 requires to show that ↑ Bin is a monoid homomorphism between + N and + Bin . This

1. (↑ N n) + N (↑ N m) = (↑ N m) + N (↑ N n) (* by + N _comm (↑ N n) (↑ N m) *) 2. ↑ Bin ((↑ N n) + N (↑ N m)) = ↑ Bin ((↑ N m) + N (↑ N n)) (* by congruence *) 3. (↑ Bin ↑ N n) + Bin (↑ Bin ↑ N m) = (↑ Bin ↑ N m) + Bin (↑ Bin ↑ N n) (* ↑ Bin
The Marriage of Univalence and Parametricity 1:3

does not follow from the type equivalence between N and Bin, and therefore needs to be manually proven.

From this simple example, it is easy to imagine the difficulty of transporting entire libraries of structures and lemmas about their properties. The promise of automatic transport across type equivalences is to seamlessly allow users to operate with the most-suited representation as needed. In particular, deriving + Bin _comm ought to be as simple as transporting + N _comm (using a general transport operator ↑whose source and target types are inferred from context):

Definition + Bin _comm : ∀ (n m : Bin). n + Bin m = m + Bin n := ↑+ N _comm.

In the literature, two major concepts have been explored to achieve automatic transport across equivalences: parametricity and univalence. This article demonstrates that both of them are insufficient taken in isolation, and that it is possible to devise a marriage of univalence and parametricity that leverages both in order to fully realize programming and proving modulo equivalences.

Parametricity. Since the seminal work of [START_REF] Magaud | Changing Data Structures in Type Theory: A Study of Natural Numbers[END_REF] on translating proofs between different representations of natural numbers in Coq, there has been a lot of work in this direction, motivated by both program verification and mechanized mathematics, with several libraries available for either Isabelle/HOL [START_REF] Huffman | Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL[END_REF] or Coq [START_REF] Cohen | Refinements for Free![END_REF][START_REF] Zimmermann | Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant[END_REF]. At their core, these approaches build on the notion of parametricity [START_REF] Reynolds | Types, Abstraction and Parametric Polymorphism[END_REF]] and its potential for free theorems about observational equivalences [START_REF] Wadler | Theorems for Free![END_REF]], in order to obtain results such as data refinements for free [START_REF] Cohen | Refinements for Free![END_REF]] and proofs for free [START_REF] Bernardy | Proofs for free: Parametricity for dependent types[END_REF].

Such a parametric transport is essentially a white-box approach that structurally rewrites observationally-equivalent terms. The previous example of Bin_comm can be handled by parametric transport. However, as we will demonstrate, the approach does not fully apply in the dependently-typed setting where computation at the type level is essential. (The Bin_comm example luckily does not rely on any type-level computation.)

Univalence. Univalence [START_REF] Voevodsky | The Equivalence Axiom and Univalent Models of Type Theory[END_REF]] is a novel principle for mathematics and type theory that postulates that equivalence is equivalent to equality. Leaving aside the most profound mathematical implications of Homotopy Type Theory (HoTT) and univalence [Univalent Foundations Program 2013], this principle should fulfill the promise of automatic transport of programs, theorems, and proofs across equivalences. There are currently two major approaches to realize univalence in a type theory. In Martin-Löf Type Theory (MLTT) [START_REF] Martin-Löf | An Intuitionistic Theory of Types: Predicative Part[END_REF], and related theories such as the Calculus of (Inductive) Constructions [START_REF] Coquand | The Calculus of Constructions[END_REF][START_REF] Paulin-Mohring | Introduction to the Calculus of Inductive Constructions[END_REF], univalence can only be expressed as an axiom. However, by the Curry-Howard correspondence, axioms have no computational content, since they correspond to free variables. Therefore an axiomatic general univalent transport is not effective. In concrete terms, this means that using axiomatic univalent transport will yield a "stuck term", stuck at the use of the axiom. There are several recent developments to build a dependent type theory with a computational account of univalence, most notably cubical type theories [START_REF] Altenkirch | Towards a Cubical Type Theory without an Interval[END_REF][START_REF] Angiuli | Cartesian Cubical Computational Type Theory: Constructive Reasoning with Paths and Equalities[END_REF][START_REF] Cohen | Cubical Type Theory: a constructive interpretation of the univalence axiom[END_REF], and concrete implementations such as Cubical Agda [START_REF] Vezzosi | Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types[END_REF]] have started to appear. Cubical type theories fully achieve the consequences of realizing univalence, such as giving computational content to both functional and propositional extensionality.

Irrespective of how univalence is realized, univalent transport allows exploiting an equivalence between two types A and B in order to establish an equivalence between P A and P B, for any arbitrary predicate P. But univalent transport alone does not address a major challenge for automatic transport, namely that of inferring, from basic equivalences, the common predicate P out of arbitrarily complex dependent types. Additionally, while it is universally applicable as a black-box approach, univalent transport can yield unsatisfactory transported terms, as explained next.

Transport à la Carte. With univalent transport, one can always convert any development that uses N into one that uses Bin, both in computationally-relevant parts and in parts that deal with reasoning and formal properties. However, univalent transport does not necessarily reconcile ease of reasoning with efficient computation. Indeed, univalently transporting a function N → N to a function Bin → Bin yields a function that first converts its binary argument to a natural number, performs the original (slow) computation and finally converts the result back to a binary number. Dually, if one starts from a Bin → Bin function and transports it to N → N, the resulting function will still execute efficiently, but simple N-based inductive reasoning will not be applicable to it.

The problem is that univalent transport across the N-Bin equivalence does not magically exploit the correspondence between different implementations of functions that operate on these types, such as between + N and + Bin . Such term-level correspondences are exploited in parametricity-based approaches, and require additional proof and engineering effort.

Therefore, in addition to addressing the limitations of parametricity and univalence when taken in isolation, an essential component of automatic transport is the tradeoff between the cost of manually establishing equivalences (between both types and functions that operate on them), and the ease of automatic univalent transport. One wishes for an automatic transport mechanism à la carte, which exploits user-provided equivalences between terms when available, and falls back to univalent transport otherwise.

Univalent Parametricity. This article proposes a marriage of univalence and parametricity that enables automatic transport à la carte across equivalences. It deeply connects and intertwines (whitebox) parametric transport and (black-box) univalent transport in a fruitful manner. Essentially, univalent parametricity is a strengthening of the parametricity translation for dependent types that demands the relation on the universe to be compatible with equivalences. This paper is structured as follows. We first recall parametricity in type theory and present its limitations to transport definitions across equivalences ( §2). We then proceed similarly with univalence, highlighting the complementarity between both approaches ( §3). Next, we illustrate how univalent parametricity achieves seamless automatic transport across equivalences from a user point of view ( §4). We develop the theory of univalent parametricity for the Calculus of Constructions with universes CC ω ( §5), and for the Calculus of Inductive Constructions CIC ( §6). We present the realization of univalent parametricity in the Coq proof assistant as a shallow embedding that exploits the typeclass mechanism ( §7). Note that this implementation in Coq does not give any computational content to univalence and extensionality axioms; instead, it brings automatic univalent transport to programmers, using such axioms sparingly in order to disrupt computation as little as possible. We explain how the illustration of §4 is effectively implemented in Coq ( §8). We end by describing a case study related to the recent integration of native integers in Coq ( §9). §10 discusses related work, and §11 concludes.

The complete Coq development (compatible with Coq v8.10) is available online: https://github.com/coqhott/univalent_parametricity Prior publication. This paper is a substantial extension of a prior conference publication [START_REF] Tabareau | Equivalences for Free: Univalent Parametricity for Effective Transport[END_REF]. First, we explain in details the limitations of both parametricity and univalence when considered in isolation ( §2- §3). Second, we extend our original proposal to integrate user-defined correspondences between terms of different (related) types, which is absolutely necessary to reconcile ease of reasoning and efficient computation, and to realize transport à la carte. The The Marriage of Univalence and Parametricity 1:5 illustrations of §4 and §8 are therefore novel as well, as they take advantage of this new feature, in addition to providing a detailed user perspective on the Coq framework. §7 is extended accordingly to deal with transport à la carte. §5 clarifies the two reasoning principles, white-box and black-box, supported by univalent parametricity, and explains how they support transport à la carte. Finally, the case study of reasoning about/with native integers ( §9) is entirely new.

[[Type i ]] p A B ≜ A → B → Type i [[Πa : A.B]] p f д ≜ Π(a : A)(a ′ : A ′ )(a ε : [[A]] p a a ′ ).[[B]] p (f a) (д a ′ ) [[x]] p ≜ x ε [[λx : A.t]] p ≜ λ(x : A)(x ′ : A ′ )(x ε : [[A]] p x x ′ ).[[t]] p [[t u]] p ≜ [[t]] p u u ′ [[u]] p [[•]] p ≜ • [[Γ, x : A]] p ≜ [[Γ]] p , x : A, x ′ : A ′ , x ε : [[A]] p x x ′

PARAMETRICITY IS NOT ENOUGH

We first review the development of parametricity in dependently-typed theories ( §2.1), and discuss its use and limitations for transporting some programs and proofs ( §2.2). Finally, we consider an extension of parametricity that addresses some limitation, but is still limited when type-level computation is involved ( §2.3).

Parametricity for Dependent Types

Reynolds originally formulated the relational interpretation of types to establish parametricity of System F [START_REF] Reynolds | Types, Abstraction and Parametric Polymorphism[END_REF]]. More recently, [START_REF] Bernardy | Proofs for free: Parametricity for dependent types[END_REF] generalized the approach to pure type systems, including the Calculus of Constructions with universes CC ω , and its extension with inductive types, the Calculus of Inductive Constructions CIC, which is at the core of proof assistants like Coq. 1The syntax of CC ω includes a hierarchy of universes Type i , variables, applications, lambda expressions and dependent function types:

A, B, M, N ::= Type i | x | M N | λx : A. M | Πx : A. B
Its typing rules are standard, and hence omitted here-see [START_REF] Paulin-Mohring | Introduction to the Calculus of Inductive Constructions[END_REF] for a recent presentation.

Parametricity for CC ω can be defined as a logical relation [[A]] p for every type A. Specifically, [[A]] p a 1 a 2 states that a 1 and a 2 are related at type A. The essence of Bernardy et al.'s approach is to express parametricity as a translation from terms to the expression of their relatedness within the same theory; indeed, the expressiveness of CC ω allows the logical relation to be stated in CC ω itself. Note that because terms and types live in the same world, [[-]] p is defined for every term.

Figure 2 presents the definition of [[-]] p for CC ω , based on the work of [START_REF] Bernardy | Proofs for free: Parametricity for dependent types[END_REF]. For the universe Type i , the translation is naturally defined as (arbitrary) binary relations on types. For the dependent function type Πa : A.B, the translation specifies that related inputs at A, as witnessed by e, yield related outputs at B.

Following Bernardy et al., the prime notation (e.g., A ′ ) denotes duplication with renaming, where each free variable x is replaced with x ′ . Similarly, the translation of a lambda term λx : A.t is a function that takes two arguments and a witness x ε that they are related; a variable x is translated to x ε ; a translated application passes the original argument, its renamed duplicate, along with its translation, which denotes the witness of its self-relatedness. The translation of type environments follows the same augmentation pattern, with duplication-renaming of each variable as well as the addition of the relational witness x ε .

Armed with this translation, it is possible to prove an abstraction theorem à la Reynolds, saying that a well-typed term is related to itself (more precisely, to its duplicated-renamed self):

Theorem 2.1 (Abstraction theorem). If Γ ⊢ t : A then [[Γ]] p ⊢ [[t]] p : [[A]] p t t ′ .
In particular, this means that the translation of a term [[t]] p is itself the proof that t is relationally parametric.

The abstraction theorem is proven by showing the fundamental property of the logical relation for each constructor of the theory. In particular, for the cumulative hierarchy of universes, ⊢ Type i : Type i+1 . This means that we have a kind of fixpoint property for the relation on Type i :

⊢ [[Type i ]] p : [[Type i+1 ]] p Type i Type i .
For parametricity, this property holds because the following is a proof term: λ(A B : Type i ). Type i : Type i → Type i → Type i+1 .

Note that this necessary fixpoint property is not necessarily trivial to satisfy in any variant of parametricity, as we will see later ( §5).

Using Parametricity to Transport Programs and Proofs

The parametricity translation together with the abstraction theorem (Theorem 2.1) are powerful tools to derive free theorems (and proofs) [START_REF] Bernardy | Proofs for free: Parametricity for dependent types[END_REF]]. However, the abstraction theorem is only concerned with what we can call reflexive homogeneous instances of the logical relation, i.e., relating a term with itself (i.e., reflexive) and hence at the same type (i.e., homogeneous). Thus, in order to be able to relate functions and theorems over different types, such as N and Bin, the standard solution is to define functions manipulating a common abstraction of their algebraic structure-in the case of natural numbers, a type with a zero and a successor function-together with an elimination principle. Then, by parametricity, we know that such a function defined on the common abstraction behaves the same if we instantiate it with N or Bin, because it must preserve any relation between N and Bin, in particular equivalences. This is for instance the approach taken in the CoqEAL framework [START_REF] Cohen | Refinements for Free![END_REF].

Parametricity presents two important issues, which we call the anticipation problem and the computation problem. The anticipation problem is that, in order to reap the benefits of parametricity to transport programs and proofs, one must anticipate and explicitly exhibit a priori an interface that is common to the types dealt with, and to define all functions generically in terms of this common interface. Engineering-wise, this anticipation might be problematic. Furthermore, defining the right interface might be challenging. Of course, in the case of the addition on natural numbers 2 , The Marriage of Univalence and Parametricity 1:7

it is fairly straightforward to define the common interface, because the definition of plus is only using the successor function and the eliminator.

Definition plus (n m : N) :

N := N_rect (fun _ ⇒ N) m (fun _ res ⇒ S res) n.
Similarly, as already noticed by [START_REF] Cohen | Refinements for Free![END_REF], finding the right interface is direct when dealing with primitive inductive types, but it becomes quite challenging when dealing with types defined using a combination of several type constructors.

The computation problem is that parametricity does not scale to computation at the type level. To illustrate this, consider the proof that O is different from S n, for every natural number n.

Definition diff n (e : O = S n) : False := let P N := N_rect (fun _ ⇒ Type) (O = O) (fun n _ ⇒ False) in eq_rect N O (fun n' _ ⇒ P N n') (eq_refl O) (S n) e.
This definition uses the elimination principle of equality over a predicate that is defined by elimination on natural numbers. It typechecks because in the branch for O, P N O reduces to O = O and in the branch S n, e, P N (S n) reduces to False. Now, if one tries to generalize this definition of this function by making it modular with respect to any type of natural numbers with zero, successor and a constant for the elimination principle, the result is ill-typed, because the abstraction P_abs of P N does not compute and so P_abs O is not definitionally equal to O = O. This issue can be sidestepped by adding the computational laws of the eliminator on natural numbers as propositional equalities in the generalized version. But then, one needs to deal with rewriting explicitly where otherwise everything was handled implicitly by conversion.3 This rewriting phase is not at all handled by parametricity.

Heterogeneous Parametricity Translation

To address the anticipation problem described above, we would like to be able to relate N or Bin directly-i.e., without relying on a common interface that captures their algebraic structure-simply because they are equivalent as types.

Observe that the definition of the parametricity translation of Bernardy et al. given in Figure 2 is homogeneous, in that terms are related at the same type, i.e., [[A]] p a 1 a 2 . This allows us to provide instances of the parametricity relation such as [[Type i ]] p N Bin. But once N and Bin are related as types, we will want to relate some of their inhabitants, such as O and O Bin , which means we also need to consider heterogeneous instances, i.e., over terms of different (related) types.

But actually, parametricity itself is eminently heterogeneous: modifying the parametricity translation to reflect this is, in fact, straightforward. It suffices to additionally consider a global context Ξ of defined constant triples, where each triple consists of two constants (such as O and O Bin ) and a witness that they are parametrically related. The global context Ξ is defined as the following telescope Ξ n :

Ξ 0 = • Ξ 1 = (c • 1 : A • 1 ; c • 1 : A • 1 ; c ⊗ 1 : [[A 1 ]] Ξ 0 p c • 1 c 1 • )
. . .

Ξ n = Ξ n-1 , (c • n : A • n ; c • n : A • n ; c ⊗ n : [[A n ]] Ξ n-1 p c • n c • n )
Note that in the definition above, we have extended the parametricity translation to additionally take the global context into account,

[[•]] Ξ
p . The definition of Figure 2 is accordingly extended on constants as follows: To state the fundamental theorem of parametricity in this setting, we need to define a notion of white box translation of a given term, [a] Ξ □ , which is essentially the identity function except for constants in Ξ, which are translated as

[[c • ]] Ξ p ≜ c ⊗ when (c • : _ ; c • : _ ; c ⊗ : _) ∈ Ξ We note |Ξ| • , |Ξ| • ,
[c • ] Ξ □ ≜ c • when (c • : _ ; c • : _ ; c ⊗ : _) ∈ Ξ We can now state the "White Box" Fundamental Property (FP): when a term a is well-typed in the context | Ξ | • , its white box translation [a] Ξ
□ is also well-typed in the context | Ξ | • , and the parametricity translation of a provides a witness that a is related to

[a] Ξ □ . Corollary 2.2 (White Box Fundamental property). If |Ξ| • ⊢ a : A then |Ξ| • ⊢ [a] Ξ □ : [A] Ξ □ and |Ξ| ⊢ [[a]] Ξ p : [[A]] Ξ p a [a] Ξ □ . Proof. From a (global) context |Ξ|, one can construct a substitution σ from |Ξ| to [[|Ξ| • ]] p by associating the triple (c • , c • , c ⊗ ) → (c • , c • ′ , c •ε ).
We note σ (t) the application of the substitution σ to a term t. By the abstraction theorem, we have that

[[|Ξ| • ]] p ⊢ [[a]] p : [[A]] p a a ′ .
The corollary follows from the fact that σ (

[[a]] p ) ≡ [[a]] Ξ p and σ (a ′ ) ≡ [a] Ξ □ . □
Note that this property is only valid in a closed world (i.e., no variables but potentially global constants), because, as parametricity is not internalized in the theory, there is no witness that variables or (equivalently) axioms are parametric.

The introduction of the global context Ξ allows us to provide a direct heterogeneous extension to the parametricity translation, however mentioning it explicitly in the translation makes the notation heavy. For instance, to show that N and Bin are parametrically related, one needs to provide a relation R NBin between N and Bin. While there are several equivalent ways of defining this relation, the canonical one reuses the transport function ↑ N that comes from the equivalence between N and Bin:

Definition R NBin := fun n m ⇒ n = ↑ N m.
Then, in order to make explicit that Bin behaves the same as N, one can define a successor function S Bin : Bin → Bin := fun n ⇒ n + 1 and show that O and O Bin are parametrically related in the global context which contains (N,Bin,R NBin ), as well as S and S Bin , which amounts to providing inhabitants for the following types:

O ⊗ : O ≈ p O Bin : N ▷◁ p Bin ≜ O = ↑ N O Bin S ⊗ : S ≈ p S Bin : N → N ▷◁ p Bin → Bin ≜ ∀ n m, n = ↑ N m → S n = ↑ N (S Bin m)
Additionally, one also needs to show that Bin satisfies an induction principle corresponding to the induction principle of N. Recall that the induction principle of N has type Definition N_rect: ∀ P : N → Type, P O → (∀ n, P n → P (S n)) → ∀ n : N, P n.

Thus, the corresponding induction principle for Bin ought to have type Definition N_rect Bin : ∀ P : Bin → Type, P O Bin → (∀ n, P n → P (S Bin n)) → ∀ n : Bin, P n.

Note that this induction principle is very different from Bin_rect, the canonical induction principle derived for the inductive definition of Bin (Figure 1). Finally, we also need to prove that N_rect Bin is parametrically related to N_rect in the global context:

Ξ N = (N;Bin;R NBin ), (O;O Bin ;O ⊗ ), (S;S Bin ;S ⊗ ) Using these definitions, it becomes possible to use parametricity to automatically convert a definition over N that uses the induction principle N_rect to an equivalent one over Bin. For instance, consider the definition of plus defined on N. By Corollary 2.2, it is possible to automatically deduce that the function Definition plus NBin (n m : Bin) : Bin := N_rect Bin (fun _ ⇒ Bin) m (fun _ res ⇒ S Bin res) n.

is parametrically related to plus, and thus behaves in the same way, because plus NBin is equal to [plus] Ξ N □ . This means that for all n m : N and n' m' : Bin, the following holds:

n ≈ p n' : N ▷◁ p Bin → m ≈ p m' : N ▷◁ p Bin → plus n m ≈ p plus NBin n' m' : N ▷◁ p Bin.
That is, using the heterogeneous version of the parametricity translation addresses the anticipation problem identified above, because we do not need to rely on a common interface between N and Bin and define all functions over this interface, as would be required in CoqEAL [START_REF] Cohen | Refinements for Free![END_REF].

The Limits of Parametricity. However, using the heterogeneous parametricity translation to obtain automatic transport still does not scale to dependent types, because of the computational problem of parametricity: parametrically-related functions behave the same propositionally but not definitionally.

Let us go back to the diff example of Section 2.2. Using the white box FP to get a parametricallyrelated definition of diff over Bin, we could expect to get

Fail Definition diff Bin n (e : O Bin = S Bin n) : False := let P Bin := N_rect Bin (fun _ ⇒ Type) (O Bin = O Bin ) (fun n _ ⇒ False) in eq_rect Bin O Bin (fun n' _ ⇒ P Bin n') (eq_refl O Bin ) (S Bin n) e.
But this term does not typecheck, as the Coq error message explains:

The term "..." has type "P Bin (S Bin n)" while it is expected to have type "False". This is because even though N_rect and N_rect Bin are parametrically related, they are not equal by conversion. And indeed, the equality N_rect Bin _ P O PS (S Bin n) = PS n only holds propositionally, but not definitionally. This means that the premise of Corollary 2.2 does not hold here: the term diff does not typecheck in the context Ξ N where each constant, and in particular the constant N_rect, is considered as a black box and does not come with associated computational rules. So, while moving to a heterogeneous presentation seems promising with respect to the anticipation problem, it is insufficient to deal with the computation problem of parametricity.

UNIVALENCE IS NOT ENOUGH

We now briefly review the notion of type equivalences ( §3.1) and the univalence principle ( §3.2), and explain why univalence alone is not sufficient for automatic transport across equivalences ( §3.3).

Type Equivalences

A function f : A → B is an equivalence iff there exists a function д : B → A together with proofs that f and д are inverse of each other. More precisely, the section property states that ∀a : A, д(f (a)) = a, and the retraction property dually states that ∀b : B, f (д(b)) = b. An additional condition between the section and the retraction, called here the adjunction condition, expresses that the equivalence is uniquely determined by the function f (and hence that being an equivalence is proof irrelevant). Definition 3.1 (Type equivalence). Two types A and B are equivalent, noted A ≃ B, iff there exists a function f : A → B that is an equivalence.

A type equivalence therefore consists of two transport functions (i.e., f and д), as well as three properties. The transport functions are obviously computationally relevant, because they actually construct terms of one type based on terms of the other type. Note that from a computational point of view, there might be different ways to witness the equivalence between two types, which would yield different transports.

Armed with a type equivalence A ≃ B, one can therefore manually port a library that uses A to a library that uses B, by using the A → B function in covariant positions and the B → A function in contravariant positions. However, with type dependencies, all uses of transport at the term level can leak at the type level. This leakage requires not only the use of sections or retractions to deal

The Marriage of Univalence and Parametricity 1:11 with type mismatches, but also additional properties relating existing functions, as illustrated in §1 with the fact that the equivalence is a homomorphism with respect to the addition on natural numbers. This also means that while the properties of an equivalence are not used computationally for transporting from A to B or vice versa, their computational content can matter when one wants to exploit the equivalence of constructors that are indexed by A or by B. For instance, to establish that a term of type T (д(f (a)) actually has type T a, one needs to rewrite the term using the section of the equivalence-which means applying it as a (computationally-relevant) function.

Univalence

Univalence is a principle that aligns type equivalence with propositional equality [START_REF] Voevodsky | The Equivalence Axiom and Univalent Models of Type Theory[END_REF]].

Definition 3.2 (Univalence). For any two types A, B, the canonical map

(A = B) → (A ≃ B) is an equivalence.
In particular, this means that (A = B) ≃ (A ≃ B). Therefore, univalence allows us to generalize Leibniz's principle of indiscernibility of identicals, to what we call the principle of Indiscernibility of Equivalents.

Theorem 3.3 (Indiscernibility of Eqivalents). For any P : Type → Type, and any two types A and B such that A ≃ B, we have P A ≃ P B.

Proof. Direct using univalence:

A ≃ B =⇒ A = B =⇒ P A = P B =⇒ P A ≃ P B □
In particular, univalence promises immediate transport: if A and B are equivalent, then we can always convert some P A to some (equivalent) P B, for every inhabitant of P A, even axioms. Corollary 3.4 (Black Box Fundamental Property). For any P : Type → Type, and any two types A and B such that A ≃ B, there exists a function ↑ ■ : P A → P B.

We call this result the "Black Box" Fundamental Property because it can be used to blindly transport a term of type P A to a term of type P B, without looking at its particular syntactical structure. As such, it is very useful to solve the computational issue of parametricity.

Realizing Univalence. In CIC and MLTT, univalence cannot be proven and is therefore defined as an axiom. Because the proof of Theorem 3.3 starts by using the univalence axiom to replace type equivalence with propositional equality, before proceeding trivially with rewriting, it has no computational content, and hence we cannot exploit (axiomatic) univalence to reap the benefits of automatic transport of programs and their properties across equivalent types. It is important for transport to be effective, i.e., that it has computational content.

Intuitively, an effective function ensures canonicity: it never gets stuck due to the use of an axiom. Conversely, a function that uses an axiom and hence "does not compute" is called ineffective. By extension, a type equivalence A ≃ B consisting of two functions f : A → B and д : B → A is said to be effective iff both f and д are effective functions.

To solve the issue of effectiveness, Cubical Type Theory has recently been proposed [START_REF] Cohen | Cubical Type Theory: a constructive interpretation of the univalence axiom[END_REF][START_REF] Vezzosi | Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types[END_REF]]. This theory is an extension of MLTT in which n-dimensional cubes can be directly manipulated, making it possible to define a notion of equality between two terms as the type of the line (1-dimensional cube) between those two terms. This way, the induced notion of equality is more extensional than the usual Martin-Löf identity type, and it satisfies univalence computationally, so the induced transports are effective.

Univalence vs. Automatic Lifting

However, even when it is effective, univalence alone is not enough to support the automatic transport of functions that are defined on equivalent types.

Let us go back to the example of addition on natural numbers. There exists a complicated but efficient definition of addition on binary natural numbers, plus Bin :4

Definition plus Bin (n m : Bin) : Bin := (* complex definition *).

Showing most properties of plus Bin , such as associativity and commutativity, is much more involved than their counterparts on N. Ideally, after proving once and for all that plus Bin is "equal" to plus, one would like to be able to obtain these theorems for free by transporting the proofs for plus on N, i.e., rewriting through this "equality".

The problem is that even in a univalent type theory, plus Bin and plus cannot be proven equal directly, because they are not defined on the same type. Indeed, the "equality" between plus Bin and plus is heterogeneous and only makes sense because there is an equivalence between N and Bin. This means that technically, the actual equality e NBin that can be stated and proven is between the pairs (N; plus) and (Bin; plus Bin ) at the telescope type Σ (A : Type), (A → A → A). Then to transport the proof of commutativity of plus Definition plus_comm : ∀ (n m : N), plus m n = plus n m.

to a proof of commutativity of plus Bin , one needs to exhibit the predicate This generalization step, which can quickly become complex, cannot in general be automatically inferred, and so needs to be explicitly provided by the user.

P_comm := fun X _ ⇒ ∀ (n m : X.1), X.2 m n = X.
In Cubical Type Theory [START_REF] Vezzosi | Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types[END_REF], one would rather rely on the primitive notion of dependent path and transport the proof as depicted in Figure 3. In that case, one must still explicitly specify an abstraction of the lemma statement to give to the transport function, and produce a dependent path between the two notions of addition. In this example, the addition on binary

The Marriage of Univalence and Parametricity 1:13 numbers _+Bin_ is defined by a "naive" transport of the addition on unary numbers. The direct proof addp shows that it is related to addition of unary numbers through the type equivalence N≡Bin. Note that the proof of this equality for the efficient addition on binary numbers would be much more involved, but this is not the point here. The point we want to stress is that transporting the proof term +-assoc to the proof term +Bin-assoc requires the user to exhibit the predicate λi → (m n o :

N≡Bin i) → addp i m (addp i n o) ≡ addp i (addp i m n) o.
We believe that, even in this simple example, a user would arguably appreciate some help from an automatic tool. This issue is very similar to the anticipation problem of parametricity described in Section 2.2. Indeed, the technique of using telescopes or dependent path types to encode heterogeneity is akin to finding the right interface for the algebraic structure of a type. But again, this does not scale to automation, and this limitation is independent of whether we are in a univalent type theory or not.

However using univalence does solve the computation issue of parametricity, as the function diff can be transported as a black box, by simply using an equality e' NBin between (N; (0,S)) and

(Bin; (O Bin ,S Bin )) at type Pack := Σ A : Type, A * (A → A). Definition diff Bin : ∀ (n:Bin) (e : O Bin = S Bin n), False := eq_rect Pack (N; (0,S)) (fun X _ ⇒ ∀ (n:X.1) (e : fst X.2 = snd X.2 n), False) diff (Bin; (O Bin ,S Bin )) e' NBin .
Therefore, it seems that a combination of parametricity and univalence could address all the issues identified thus far.

UNIVALENT PARAMETRICITY IN ACTION

This article develops the notion of univalent parametricity as a fruitful marriage of univalence and parametricity, which leverages their strengths while overcoming their limitations when taken in isolation. Specifically, univalent parametricity solves the anticipation problem of parametricity by using (a variant of) the heterogeneous parametricity translation, and solves the computation problem of parametricity by using univalence.

Given two equivalent types, univalent parametricity can be used to automatically transport properties defined on one type-e.g., an easy-to-reason-about representation such as N-to their counterparts on the other type-e.g., a computationally-efficient representation such as Bin. Univalent parametricity provides the best of both parametricity and univalence in that, to transport a term, we can use either the White Box FP (Th 2.2) or the Black Box FP (Th 3.4), depending on the situation. In fact, the interplay between both modes is subtle in that white-box transport can automatically build univalent relations between two arbitrarily complex types based on user-provided relations, thereby inducing an equivalence that provides black-box transport for their inhabitants.

Univalent parametricity is a variant of the heterogeneous parametricity translation a ≈ p b :

A ▷◁ p B introduced in §2, simply noted a ≈ b : A ▷◁ B. When a ≈ b : A ▷◁ B is inhabited,
we say that a and b are univalently related. We sometimes omit A and B when they are clear from context.

The full development of univalent parametricity is in the following sections. In this section, we briefly illustrate univalent parametricity in action with programs and proofs over N and Bin. First, we illustrate transport à la carte, i.e., the possibility to refine automatic transport by establishing additional univalent relations ( §4.1). Second, we show that univalent parametricity allows us to transport properties proven on N to properties proven on Bin automatically ( §4.2), and vice versa ( §4.3).

Automatic Transport à la Carte

Having proven the type equivalence between N and Bin, we can prove that they are univalently related, i.e., N ≈ Bin : Type ▷◁ Type. Doing so induces an automatic transport function, corresponding to the Black Box FP of univalence (Th 3.4). For instance we can transport a square function on N to an equivalent function on Bin:5 Definition square (x : N) : N := x * x. Definition square Bin■ : Bin → Bin := ↑ ■ square.

Note that from this section on, in code examples we use a general black-box transport operator ↑ ■ whose source and target types are inferred from context, and whose underlying equivalence is computed automatically, as will be explained in §7.

While square Bin■ is an effective function that can be used to compute the square of any binary natural number, it is inherently inefficient computationally, because of the black-box nature of the transport: when applied, square Bin■ first converts its Bin argument to an equivalent N, applies the (slow) multiplication operation on N, and finally converts back the N result to a Bin:

Check eq_refl : square Bin■ = (fun x:Bin ⇒ ↑ ■ (square (↑ ■ x))).
At the cost of an additional proof effort, it is possible to establish that mult and mult Bin are univalently related, mult ≈ mult Bin : N → N ▷◁ Bin → Bin (and likewise for plus and plus Bin ):

Definition univrel_mult : mult ≈ mult Bin .
A first pay-off for this additional proof effort is that transport can now automatically exploit such a relation, so that we can transport square using the White Box FP of univalent parametricity, i.e., rewriting its body and exploiting the univalent relation between mult and mult Bin :

Definition square Bin□ : Bin → Bin := ↑ □ square.
The notation ↑ □ corresponds to the [•] Ξ □ notation of the White Box FP (Th 2.2), where the global context Ξ is implicit. The management of the global context and the definition of this (ad hoc) polymorphic operator are realized in Coq through typeclasses, as will also be explained in §7.

The transported function square Bin□ now computes directly on Bin, instead of converting back and forth and using the (slow) multiplication operation on N.

Check eq_refl : square Bin□ = (fun x ⇒ (x * x)%Bin).

Automatic Transport of Properties

Establishing that two terms like plus and plus Bin are univalently related is not only valuable from a computational point of view. It also enables the automatic transport of properties that involve such terms.

Without presenting the details of univalent parametricity yet, suffice it to say that the type plus ≈ plus Bin actually unfolds to

The Marriage of Univalence and Parametricity 1:15

∀ (x : N) (y : Bin), x = ↑ ■ y → ∀ (x' : N) (y' : Bin), x' = ↑ ■ y' → x + x' = ↑ ■ (y + y')
which gives an extensional interpretation of the heterogeneous equality between plus and plus Bin , using univalent transport ↑ ■ on terms of type Bin. Then, thanks to the univalent relation plus ≈ plus Bin , it is possible to automatically infer the type equivalence between the type ∀ n m : N, n + m = m + n and the type ∀ n m : Bin, n + m = m + n. Consequently, the proof of commutativity for plus can automatically be transported to a proof of commutativity for plus Bin :

Definition plus Bin _comm : ∀ n m : Bin, n + m = m + n := ↑ ■ plus_comm.
Note that here, we do not face the computation issue encountered by using only parametricity ( §2.2) because the term plus_comm is transported as a black box, i.e., without recursively diving into its syntax.

In the same way, we can define the power function on both N and Bin and show that they are univalently related. Then, the following very simple proof of an additive property of the power function: In contrast, because adding 1 to a binary natural number is not an operation that preserves the inductive structure of that number, a direct proof of this lemma by induction on the binary natural number is much more involved.

Definition pow_prop : ∀ n:N, 3 ^(n + 1) = 3 * 3 ^n.

Automatically Computing in the Equivalent Representation

Univalent parametricity can also be used the other way around to prove properties by computation on a type representation that is not always effective. Consider for instance the definition of a polynomial on natural numbers

Definition poly : N → N := fun n ⇒ 12 * n + 51 * n ^4 -n ^5.
and consider proving that poly 50 is bigger than some given value, say 1000. 6 One would like to prove this by computation, i.e., by actually calculating the value of poly 50 and then simply comparing the result with 1000. However, because the unary representation is very inefficient, evaluating poly at 50 already exceeds the stack capacity of the Coq runtime.

Eval compute in poly 50.

Error Stack overflow

Therefore, the proof that poly 50 is bigger than 1000 cannot be done by computation. Univalent parametricity can overcome this issue by transporting the inequality to be proven to an equivalent one that uses the binary number representation.

Goal poly 50 ≥ 1000.

replace_goal; now compute. Defined.

The tactic replace_goal automatically infers, from poly 50 ≥ 1000, the univalently-related proposition on binary natural numbers using the White Box FP. Once the goal has been transported to a property on binary natural numbers, it is possible to proceed by computation, which produces a goal that can be solved automatically.

Note that automatic transport also works if we consider a slightly more complex example, where polynomials are encoded as a list of natural numbers representing its coefficients, together with a recursive evaluation function evalPoly:

Definition polyType := list N. Fixpoint evalPoly (p : polyType) (n : N) (degree : N) : N := match p with | [] ⇒ 0 | coef :: p ⇒ coef * n ^degree + evalPoly p n (S degree) end.
Infix "@@" := (fun p n ⇒ evalPoly p n 0).

Then, defining the polynomial poly in this setting and evaluating it at 50 leads to the exact same issue.

Definition poly' : polyType := [0;12;0;0;51;1].

Eval compute in poly' @@ 50.

Error Stack overflow

And the univalent parametricity framework allows again to transfer the goal to binary numbers in order to solve it by computation.

Goal poly' @@ 50 ≥ 1000.

replace_goal; now compute. Defined.

Because univalent parametricity is defined on all of CIC, this proof technique also scales to the definitions of fixpoints. For instance, consider the following sequence definition:

Fixpoint sequence (acc n : N) := match n with
The Marriage of Univalence and Parametricity 1:17

0 ⇒ acc | 1 ⇒ 2 * acc | 2 ⇒ 3 * acc | S n ⇒ (sequence acc n) ^acc end.
Indeed, one can generically show that fixpoints preserve univalently-related arguments, which means that sequences producing unary natural numbers can be transported automatically to equivalent sequences producing binary natural numbers.

Definition sequence_prop : sequence 2 5 ≥ 1000.

replace_goal; now compute. Defined.

In summary, univalent parametricity follows the structural, white-box approach of parametricity to infer new univalent relations from existing ones, and can then exploit the induced equivalences as computational black boxes, as in univalence, to transport proofs and terms. The following sections develop the theory of univalent parametricity for CC ω ( §5) and CIC ( §6), and its realization in the Coq proof assistant ( §7). Then, we revisit the examples of this section, explaining how each step is implemented ( §8), and discuss a case study for integrating native datatypes in Coq ( §9).

UNIVALENT PARAMETRICITY

We now turn to the formal development of univalent parametricity. In this section, we focus on CC ω -extension to CIC is in §6. We consider a type theory with the minimum requirements, namely the Calculus of Constructions with universes and the univalence axiom.

We first discuss in Section 5.1 the proper way to extend the parametricity translation in the universe to take equivalences into account. We then provide the complete univalent translation for CC ω and present the Abstraction Theorem and its proof ( §5.2). Note that the development here is largely independent of any particular realization of univalence, whether axiomatic or computational. In our axiomatic setting, let us insist that sometimes, a direct use of the univalence axiom would trivialize a proof but it would also suppress its computational content, thus leading to a useless framework in practice. In a setting where univalence is fully realized, such as in Cubical Type Theory, those simpler proofs could be used (see also §10).

In § 5.3, we extend the translation by taking a global context as input, which allows us to formulate the White Box Fundamental Property for CC ω (Corollary 5.3). This property can relate terms of completely different types, such as inductively-defined and binary-encoded naturals, providing the global environment provides witnesses that they are in univalent relation. This is important because we want to be able to let programmers define their own equivalences and thus get univalent transport à la carte ( §5.4). Univalent parametricity on types also entails type equivalence, which allows us to also state a Black Box Fundamental Property (Proposition 5.4), which says that when two types A and B are in univalent relation, any open term t : A is in univalent relation with its (black-box) transport of type B.

Univalent Parametricity on the Universe

To strengthen parametricity to deal with equivalences, the univalent parametricity translation [[-]] u must strengthen the parametricity translation on the universe Type i . Several intuitive solutions come to mind, which however are not satisfactory.

First, we could simply replace the relation demanded by parametricity to be type equivalence itself, i.e., [[Type i ]] u A B ≜ A ≃ B. However, by doing so, the abstraction theorem fails on ⊢ Type i : Type i+1 . We would need to establish the fixpoint on the universe, i.e., [

[Type i ]] u : [[Type i+1 ]] u Type i Type i , but we have [[Type i ]] u : Type i → Type i → Type i+1 Type i ≃ Type i .
In words, on the left-hand side we have an arbitrary relation on Type i , while on the right-hand side, we have an equivalence. Another intuitive approach is to state that [[Type i ]] u A B requires both a relation on A and B and an equivalence between A and B. While this goes in the right direction, it is insufficient because there is no connection between the two notions. This in particular implies that, when scaling up from CC ω to CIC, the identity type-which defines the notion of equality-will not satisfy the abstraction theorem of univalent parametricity. We need to additionally demand that the relation coincides with propositional equality once the values are at the same type.

Therefore, an inhabitant of [[Type i ]] u is given by a relation R : A → B → Type i and an equivalence e : A ≃ B, together with a coherence condition between the relation and the equivalence.7 This (crucial!) condition stipulates that the relation does coincide with propositional equality up to a transport using the equivalence, i.e., for all a : A and b : B, the following should hold:8

R a b ≃ (a = ↑ e b)
This coherence condition allows us to show that once the relation is fixed, the rest of the data is a mere proposition. That is, the fact that there exists an equivalence satisfying the coherence condition just characterizes the kind of relations that can be used, but it does not provide additional structure. This way, univalent parametricity is really just a restriction of parametricity to relations that correspond to equivalences.

Therefore, for Type i , we want the translation to be:

[[Type i ]] u A B ≜ Σ(R : A → B → Type i )(e : A ≃ B). Πa b.(R a b) ≃ (a =↑ e b)
That is, the translation of a type (when seen as a term) needs to include a relation plus the fact that there is an equivalence, and that the relation is coherent with equality.

We therefore need to distinguish between the translation of a type T occurring in a term position (i.e., left of the ":"), translated as [T ] u and the translation of a type T occurring in a type position (i.e., right of the ":"), translated as [[T ]] u . 9 The abstraction theorem on Type i enforces the definition The Marriage of Univalence and Parametricity 1:19 of the translation on the universe hierarchy to satisfy:10

[Type i ] u : [[Type i+1 ]] u Type i Type i ≡ Σ(R : Type i → Type i → Type i+1 )(e : Type i ≃ Type i ). Πa b.(R a b) ≃ (a =↑ e b).
That is, [Type i ] u must be itself a triple given by

[Type i ] u ≜ (λ (A B : Type i ), Σ(R : A → B → Type i )(e : A ≃ B). Πab.(R a b) ≃ (a =↑ e b); id Type i ; univ Type i )
where id Type i is simply the identity equivalence on the universe and univ Type i is a proof that the univalent relation in the universe is coherent with equality on the universe as given below.

Proposition 5.1. There exists a term univ Type

i : ΠA B. [[Type i ]] u A B ≃ (A = B).
Proof. The definition of univ Type i crucially relies on univalence (and actually is equivalent to it), so this equivalence is not effective.

This result requires functional extensionality, i.e., the fact that the canonical map

f = д → Π(x : A).f x = д x
is an equivalence. This property is in fact a consequence of univalence [Univalent Foundations Program 2013].

By univalence and rearrangement of dependent sums, the type

[[Type i ]] u A B is equivalent to Σ(e : Type i ≃ Type i )(R : Type i → Type i → Type i+1 ). Πa b.R a b = (a =↑ e b)
which by functional extensionality is equivalent to Σ(e : Type i ≃ Type i )(R :

Type i → Type i → Type i+1 ). R = (λ a b. a =↑ e b) But Σ(R : Type i → Type i → Type i+1 ). R = (λ a b. a =↑ e b
) is a singleton type, which is always contractible. So we get an equivalence

[[Type i ]] u A B ≃ (A ≃ B)
and we conclude by univalence again. □

The Univalent Parametricity Translation

We now turn to the full definition of the univalent parametricity translation on the whole syntax of CC ω , including variables, application and lambda expressions, as a variation on the parametricity translation in the style of Bernardy et al. (recall Figure 2 of §2.1). Figure 4 shows how to extend the parametricity translation to force the relation defined between two types to correspond to a type equivalence with the coherence condition, as exposed in §5.1. Note that the translation does not target CC ω but rather CIC u , which is CIC augmented with the univalence axiom. We write Γ ⊢ u t : T to stipulate that the term is typeable in CIC u .

As explained in the previous section, the definition of the translation of a type A is more complex than that of Figure 2 that the relation is coherent with equality. This is why the translation of dependent products makes use of two additional terms Equiv Π and univ Π that will be explained during the proof of the Abstraction Theorem.

For the other terms, the translation does not change with respect to parametricity except that [[-]] u must be used accordingly when we are denoting the relation induced by the translation and not the translation itself.

1:20

Nicolas Tabareau, Éric Tanter, and Matthieu Sozeau

[Type i ] u ≜ (λ (A B : Type i ), Σ(R : A → B → Type i )(e : A ≃ B). Πab.(R a b) ≃ (a =↑ e b); id Type i ; univ Type i ) [Πa : A. B] u ≜ (λ (f : Πa : A.B) (д : Πa ′ : A ′ .B ′ ). Π(a : A)(a ′ : A ′ )(a ε : [[A]] u a a ′ ). [[B]] u (f a) (д a ′ ); Equiv Π A A ′ [A] u B B ′ [B] u ; univ Π A A ′ [A] u B B ′ [B] u ) [x] u ≜ x ε [λx : A.t] u ≜ λ(x : A)(x ′ : A ′ )(x ε : [[A]] u x x ′ ). [t] u [t u] u ≜ [t] u u u ′ [u] u [[A]] u ≜ [A] u .1 [[A]] eq u ≜ [A] u .2 [[A]] coh u ≜ [A] u .3 [[•]] u ≜ • [[Γ, x : A]] u ≜ [[Γ]] u , x : A, x ′ : A ′ , x ε : [[A]] u x x ′ Fig. 4. Univalent parametricity translation for CC ω Theorem 5.2 (Abstraction theorem). If Γ ⊢ t : A then [[Γ]] u ⊢ u [t] u : [[A]] u t t ′ .
Proof. The proof is a straightforward induction on the typing derivation. The only cases that differ from Theorem 2.1 are the typing rules for the universe and for the type of dependent functions. The case of the universe has already been addressed in § 5.1. For dependent products, we first need to provide a term that witnesses the fact that the dependent product is congruent with respect to equivalences in the following sense:

Equiv Π : Π (A B : Type i ) (UR AB : [[Type i ]] u A B). Π (P : A → Type i ) (Q : B → Type i ) (UR P Q : Π(a : A) (b : B). UR AB .1 a b → [[Type i ]] u (Pa) (Qb))). (Π(a : A). P a) ≃ (Π(b : B). Q b)
In particular, we have UR AB .2 : A ≃ B and λ a b r,

(UR P Q a b r ).2 : Π(a : A) (b : B). UR AB .1 a b → P a ≃ Q b.
Using the coherence condition UR AB .3 between UR AB .1 a b and a =↑b, this boils down to Π(a : A). P a ≃ Q (↑a).

At this point we can apply a standard result of HoTT, namely equiv_functor_∀ in the Coq HoTT library [START_REF] Bauer | The HoTT Library: A Formalization of Homotopy Type Theory in Coq[END_REF]]. This lemma requires functional extensionality in the proof that the two transport functions form an equivalence.11

The Marriage of Univalence and Parametricity 1:21

The second step is to provide a proof that the univalent (pointwise) relation on the dependent product is coherent with equality up to the equivalence above; i.e., we need to define a term univ Π :

Π (A B : Type i ) (UR AB : [[Type i ]] u A B). Π (P : A → Type i ) (Q : B → Type i ) (UR P Q : Π(a : A) (b : B). UR AB .1 a b → [[Type i ]] u (P a) (Q b))). Π f д.(Π(a : A)(b : B)(r : UR AB .1 a b). (UR P Q a b r ).1 (f a) (д a ′ )) ≃ (f = ↑д)
This part is quite involved. In essence, this is where we prove that transporting in many hardto-predict places is equivalent to transporting only at the top level. This is done by repeated use of commutativity lemmas of transport of equality over functions. We refer the reader to the Coq development for more details. □ 5.2.1 Prop. The definition of the univalent parametricity translation of Figure 4 does not deal with the universe Prop of proposition, but it can be treated in the same way as Type i because Prop : Type i is a universe that also enjoys the univalence axiom. The only specificity of Prop is its impredicativity, which does not play any role here.

It is also possible to state a stronger axiom on Prop called propositional extensionality, which uses logical equivalences instead of type equivalences in its statement:

(P = Q) ≃ (P ⇐⇒ Q).
This axiom cannot be deduced from univalence alone, one would need proof irrelevance for Prop as well. As we are looking for the minimal amount of axioms needed for establishing univalent parametricity, we do not make use of this stronger axiom. Note that exploiting the fact that Prop is proof irrelevant, [[Prop]] u P Q boils down to Σ(R : P → Q → Type). (P ⇐⇒ Q) * (Π(p : P) (q : Q). IsContr(R p q)).

where * is the product of types and IsContr A says that A is contractible, i.e., it has a unique inhabitant. This is because for all p and q, the type (p = ↑q) is contractible, and being equivalent to a contractible type is the same as being contractible. The definition we obtain in this case coincides with the definition of parametricity with uniformity of propositions developed by [START_REF] Anand | Revisiting Parametricity: Inductives and Uniformity of Propositions[END_REF] (more details in §10).

White Box and Black Box Fundamental Properties

The extension of the parametricity translation that takes a global context into account presented in order to handle heterogeneous instance ( §2.3) can also be applied to univalent parametricity. Recall that we consider a global context Ξ to be the following telescope Ξ n defined as:

Ξ 0 = • Ξ 1 = (c • 1 : A • 1 ; c • 1 : A • 1 ; c ⊗ 1 : [A 1 ] Ξ 0 u c • 1 c 1 • )
. . .

Ξ n = Ξ n-1 , (c • n : A • n ; c • n : A • n ; c ⊗ n : [A n ] Ξ n-1 u c • n c • n )
For simplicity, we reuse the notation of Section 2.3 to get a similar White Box FP for univalent parametricity. In particular, the definition of Figure 4 is likewise extended on constants as follows:

[c • ] Ξ u ≜ c ⊗ when (c • : _ ; c • : _ ; c ⊗ : _) ∈ Ξ Corollary 5.3 (White Box Fundamental Property). If |Ξ| • ⊢ a : A then |Ξ| • ⊢ [a] Ξ □ : [A] Ξ □ and |Ξ| ⊢ u [a] Ξ u : [[A]] Ξ u a [a] Ξ □ .
Proof. Similar to the proof of Corollary 2.2. □

As we have done for parametricity, we introduce the notation a ≈ b :

A ▷◁ B ≜ [[A]] Ξ u a b (when B = [A] Ξ □ )
which relates two terms a and b at two related-but potentially different-types A and B. This notation only makes sense when B = [A] Ξ □ in the current global context Ξ, and we implicitly assume it is the case when we use this notation.

The White Box FP is the usual result obtained using parametricity, just rephrased using a context of global constants. But in the case of univalent parametricity, we have an additional property coming from the use of equivalences, which is oblivious to the structure of the term, and is defined for any well-typed terms, even in an open context, and in particular in presence of axioms. Indeed, once we know that two types A and B are univalently related, there is a canonical term in B related to any term t of type A obtained from the following property: Proposition 5.4 (Black Box Fundamental Property). Let A and B be two types such that A ≈ B : Type ▷◁ Type, then for all t : A, there is a proof that t ≈↑t: A ▷◁ B.

Proof. By reflexivity of equality, ↑t= B ↑t, which gives the desired result by using the coherence condition between equality and the relation. □

Note that the Black Box FP is internal to the theory, as opposed to the White Box FP, which is external. In particular, this means that the Black Box FP is valid in any context on open terms, which is crucial to define automatic transport.

Univalent Parametricity for Transport à la Carte

The Black Box Fundamental Property (Proposition 5.4) is a key advantage of univalent parametricity over traditional parametricity, because knowing that two types A and B are univalently related is enough to get a transport function from A to B, whereas traditional parametricity requires the exact definition of the term a in A in order to compute its counterpart in B. Now, it remains to investigate how to determine that two types are univalently related.

The White Box FP (Corollary 5.3) allows us to enrich the univalent relation "outside the diagonal", i.e., to provide heterogeneous instances in the global context. For instance, we can relate unary naturals N and binary naturals Bin, i.e., N ≈ Bin : Type ▷◁ Type. By combining this basic relation with the fact that type constructors are univalently parametric, it is possible to automatically derive that:

N → N → N ≈ Bin → Bin → Bin : Type ▷◁ Type But more interestingly, not only univalent relation instances between types can be added, but also instances between any two terms, seen as new constants of the theory. For instance, consider the case of the definitions of the addition on unary and binary natural numbers plus : N → N → N and plus Bin : Bin → Bin → Bin. One can show that they are univalently related plus ≈ plus Bin : N → N → N ▷◁ Bin → Bin → Bin which, as illustrated in §4, allows automatic transport to be more computationally efficient, and proofs of results involving addition to be transported automatically. Indeed, there exists a context Ξ that relates Then, using the Black Box FP provides a direct transport plus Bin _comm of the proof of commutativity of addition plus_comm. Note that the computational content of plus_comm is not used to derive plus Bin _comm. Therefore, univalent parametricity naturally provides a framework to transport functions and proofs of theorems à la carte, depending on the univalent relation context that has been specified by the user, thanks to the interplay between white-box and black-box transports.

UNIVALENT PARAMETRICITY FOR INDUCTIVE TYPES

We now turn to the extension of univalent parametricity in theories that provide inductive types, such as the Calculus of Inductive Constructions (CIC) [Paulin-Mohring 2015]. We first give the general idea of the approach, and then proceed step-by-step, first considering dependent pairs ( §6.1), records ( §6.2), parameterized recursive inductive families ( §6.3), and finally indexed inductive types ( §6.4). An inductive type is defined as a new type constructor, together with associated constructors and an elimination principle.12 For instance, the inductive type of lists is 13Inductive list (A : Type) :

Type := nil : list A | cons : A → list A → list A
where nil and cons are the constructors of the inductive type. The associated eliminator is list_rect : ∀ (A : Type) (P : list A → Type), P nil → (∀ (a : A) (l : list A), P l → P (a :: l))

→ ∀ l : list A, P l.

Let us consider an inductive type I : T, with constructors I_c i : T c i and elimination principle I_rect : T rect . Using the global context presentation of Section 5.3, the introduction of this new inductive type in our framework amounts to the ability to extend the current global context Ξ with the following triple for the type constructor (I : T; I : T; I ⊗ : [[T]] Ξ u I I) and similar triples for each constructor and for the eliminator. We can then directly use the White Box FP (Corollary 5.3) extended with this inductive type. To sum up, the addition of the triples for the inductive type I amounts to giving the following terms14

      I ⊗ : I ≈ I : T ▷◁ T I_c i ⊗ : I_c i ≈ I_c i : T c i ▷◁ T c i I_rect ⊗ : I_rect ≈ I_rect : T rect ▷◁ T rect
When the above terms exist, we say that the inductive type, constructors and elimination principle are univalently parametric.

Dependent Pairs

In CIC, dependent pairs are defined as the inductive family:

Inductive sigT (A : Type) (B : A → Type) : Type := existT : ∀ x : A, B x → sigT A B.
Thus, the unique constructor of a dependent pair is existT and the elimination principle is given by sigT_rect : ∀ (A : Type) (P : A → Type) (P 0 : sigT A P → Type), (∀ (x : A) (p : P x), P 0 (x; p)) → ∀ s : sigT A P, P 0 s

As common, we use the notation Σa : A. B to denote sigT A (fun a ⇒ B), similarly to dependent type theories where pair types are part of the syntax [START_REF] Martin-Löf | An Intuitionistic Theory of Types: Predicative Part[END_REF]. Proposition 6.1. There exists a term

Σ ⊗ : Σ ≈ Σ : Π(A : Type i ). (A → Type i ) → Type i ▷◁ Π(A : Type i ). (A → Type i ) → Type i
Proof. The main steps of the construction are similar to those for the dependent product. Unfolding the definitions, giving a term Σ ⊗ amounts to giving an inhabitant of [[Type i ]] u given two terms UR AB : A ≈ B : Type i ▷◁ Type i and UR P Q : P ≈ Q : A → Type i ▷◁ B → Type i .

First, the univalent relation R Σ between Σa : A. P a and Σb : B. Q b is defined as R Σ ≜ λ(p : Σa : A. P a)(q : Σb : B. Q b). Σ(r pq : UR AB .1 p.1 q.1). (UR P Q p.1 q.1 r pq ).1 p.2 q.2.

It naturally requires the first and second elements of the pair to be related at the corresponding types.

Second, the proof that Σa : A. P a ≃ Σb : B. Q b also follows from a standard result of HoTT, namely equiv_functor_sigma in the Coq HoTT library. Contrarily to the dependent product, which requires functional extensionality, this lemma does not require any axiom.

Finally, the proof that the relation is coherent with equality is the novel part required by univalent parametricity. This means that we need to define a term:

univ Σ : Π (A B : Type i ) (UR AB : A ≈ B : Type i ▷◁ Type i ). Π (P : A → Type i ) (Q : B → Type i ) (UR P Q : P ≈ Q : A → Type i ▷◁ B → Type i ). Πx y.(x ≈ y : Σa : A. P a ▷◁ Σb : B. Q b) ≃ (x = ↑y)
Instead of building the equivalence explicitly with the transport functions and their associated section and retraction proofs, this equivalence can be conveniently proven by composition of equivalences. Specifically, we rely on a decomposition of equality for dependent sums:

(x ≈ y) ≡ (Σp : x .1 ≈ y.1. x .2 ≈ y.2) ≃ (Σp : x .1 =↑y.1 . x .2 =↑y.2) ≃ (x = ↑y)
Note that the last equivalence above is the counterpart of functional extensionality for dependent function types. The main difference is that this equivalence is effective as it can be proven by elimination of dependent pairs. □

With Σ ⊗ defined, we can extend the global context for the constructor and eliminator as well.

The Marriage of Univalence and Parametricity 1:25 Proposition 6.2. There is a term

existT ⊗ : existT ≈ existT : T ex ▷◁ T ex
where T ex ≜ Π(A : Type)(P : A → Type)(x : A). P x → Σ(x : A). P x and similarly for sigT_rect.

Proof. Direct by induction on the structure of a dependent pair type. □

Record Types

The treatment of dependent pairs above scales to dependent records, by considering their encoding as iterated dependent pairs. To illustrate, let us consider the example of a simple library record type Lib, which abstracts over an indexed container type constructor C, and packages functions head and map together with a property on their composition:

Record Lib (C : Type → N → Type) := { head : ∀ {A : Type} {n : N}, C A (S n) → A; map : ∀ {A B} (f :A → B) {n}, C A n → C B n; prop : ∀ n A B (f : A → B) (v : C A (S n)), head (map f v) = f (head v)}.
Like all record types, Lib can be formulated in terms of nested dependent pairs. This means that, for any C : Type → N → Type, Lib C is equivalent to

Lib' C := Σ (hd : ∀ A n. C A (S n) → A), Σ (map : ∀ A B (f:A → B) n, C A n → C B n), ∀ n A B (f : A → B) (v : C A (S n)), hd (map f v) = f (hd v).
The fact that Lib' is univalently parametric directly follows from the abstraction theorem of CC ω extended with dependent pairs. To conclude that Lib is univalently parametric, we use the fact that a type family equivalent to a univalently parametric type family is itself univalently parametric.

This approach to establish the univalent parametricity record type via its encoding with dependent pairs can be extended to any record type. We have automatized this principle in our Coq framework as a tactic, by reusing an idea used in the HoTT library that allows automated inference of type equivalence for records with their nested pair types formulation. This tactic can be used to automatically prove that a given record type is univalently parametric (provided its fields are).

Parameterized Recursive Inductive Families

To establish the univalent parametricity of a parameterless recursive inductive type, such as natural numbers with zero and successor, we can simply use the canonical structure over the identity equivalence, with equality as univalent relation and trivial coherence. However, whenever an inductive type has parameters, the situation is more complex. 15 Let us develop the case of lists and define the term

list ⊗ : list ≈ list : Type i → Type i ▷◁ Type i → Type i .
15 In this work the distinction between parameters and indices for inductive types is important. A parameter is merely indicative that the type behaves uniformly with respect to the supplied argument. For instance A in list A is a parameter. Thus the choice of A only affects the type of elements inside the list, not its shape. In particular, by knowing A for a given list, we cannot infer which constructor was used to construct the list. On the other hand, n in Vect A n is an index. By knowing the value of an index, one can infer which constructor(s) may or may not have been used to create the value. For instance, a value of type Vect A 0 is necessarily the empty vector. We address indexed inductive types in §6.4.

Unfolding the definitions, giving a term list ⊗ amounts to exhibiting an inhabitant of [[Type i ]] u given two types A and B related by UR AB : A ≈ B : Type i ▷◁ Type i . The univalent relation on lists is given directly by parametricity. Indeed, following the work of [START_REF] Bernardy | Proofs for free: Parametricity for dependent types[END_REF] on the inductive-style translation, the inductive type corresponding to the transport of a relation between A and B to a relation between list A and list B is given by:

Inductive UR_list A B (R : A → B → Type) : list A → list B → Type := UR_list_nil : UR_list R nil nil | UR_list_cons : ∀ a b l l', (R a b) → (UR_list R l l') → UR_list R (a::l) (b::l').
This definition captures the fact that two lists are related iff they are of the same length and pointwise-related. Then, the univalent relation is given by

R list ≜ λ(l : list A)(l ′ : list B). UR_list A B UR AB .1 l l ′
Then, we need to show that list A ≃ list B knowing that A ≃ B from UR AB . The two transport functions of the equivalence list A ≃ list B can be defined by induction on the structure of the list (i.e., using the eliminator list_rect). They both simply correspond to the usual map operation on lists. The proofs of the section and retraction are also direct by induction on the structure of the list, and transporting along the section and retraction of A ≃ B.

Similarly to dependent pairs, the proof that the relation is coherent with equality relies on the following decomposition of equality between lists:

Π A B (e : A ≃ B) l l ′ . (UR_list A B (λ a b.a = ↑b) l l ′ ) ≃ (l = ↑l ′ )
Indeed, using this lemma, the coherence of the univalent relation with equality is easy to infer:

(l ≈ l ′ ) ≡ (UR_list A B UR AB .1 l l ′ ) ≃ (UR_list A B (λ a b.a = ↑b) l l ′ ) ≃ (l = ↑l ′ )
Note that it is always valid to decompose equality on inductive types. This is because a value of an inductive type can only be observed by analyzing which constructor was used to build the value. This fact is explicitly captured by the elimination principle of an inductive type. On the contrary, for dependent products, the fact that functions can only be observed through application to a term is implicit in CIC, i.e., there is no corresponding elimination principle in the theory (hence functional extensionality is an axiom).

The proofs that the constructors nil and cons are univalently parametric are direct by definition of UR_List. Likewise, the proof that the eliminator list_rect is univalently parametric is direct by induction on UR_List.

Generalization. It is possible to generalize the above result, developed for lists, to any parameterized inductive family. As illustrated above, the univalent relation for parameterized inductive families is given by parametricity, and the proof that related inputs give rise to equivalent types proceeds by a direct induction on the structure of the type. The main difficulty is to generalize the proof of the coherence of the relation with equality. Indeed, this involves fairly technical reasoning on equality and injectivity of constructors.

Fortunately, in practice in our Coq framework, a general construction is not required to handle each new inductive type, because a witness of the fact that a given inductive is univalently

The Marriage of Univalence and Parametricity 1:27 parametric can be defined specifically as a typeclass instance. We also provide a tactic to automatically generate this proof on any parameterized datatype (up to a fixed number of constructors), depending on the univalent parametricity of its parameters.

Indexed Inductive Families

CIC supports the definition of inductive types that are not only parameterized, but also indexed, like length-indexed vectors Vector A n. Another mainstream example is Generalized Algebraic Data Types (GADTs) [START_REF] Simon | Simple unification-based type inference for GADTs[END_REF]] illustrated here with the typical application to modeling typed expressions:

Inductive Expr : Type → Type := | I : N → Expr N | B : B → Expr B | Ad : Expr N → Expr N → Expr N | Eq : Expr N → Expr N → Expr B.
Observe that the return types of constructors instantiate the inductive family at specific type indices, instead of uniform type parameters as is the case for e.g., the parameterized list inductive type. This specificity of constructors is exactly what makes GADTs interesting for certain applications; but this is precisely why their univalent parametricity is ineffective! Indeed, consider the equivalence between natural numbers N and binary natural numbers Bin. Univalent parametricity of the Expr GADT means that Expr N is equivalent to Expr Bin. However, there is no constructor for Expr that can produce a value of type Expr Bin. So the only way to obtain such a term is by using an equality between N and Bin, that is, using the univalence axiom. 16The challenge is that univalent parametricity for indexed inductive families relies on the coherence condition. To better understand this point, let us study the prototypical case of identity types.

Identity types. In Coq, the identity (or equality) type eq, with notation =, is defined as an indexed inductive family with a single constructor eq_refl: Inductive eq (A : Type) (x : A) : A → Type := eq_refl : x = x.

The elimination principle eq_rect, known as path induction in HoTT terminology, is: eq_rect : ∀ A (x : A) (P : ∀ a : A, x = a → Type), P x eq_refl → ∀ (y : A) (e : x = y), P y e Proposition 6.3. There is a term eq ⊗ : eq ≈ eq : Π (A : Type) (x : A). A → Type ▷◁ Π (A : Type) (x : A). A → Type. The univalent relation for identity types is defined using the inductive type obtained by applying parametricity to the identity type:

Inductive UR_eq (A 1 A 2 : Type) (A R : A 1 → A 2 → Type) (x 1 : A 1 ) (x 2 : A 2 ) (x R : A R x 1 x 2 ) : ∀ (y 1 : A 1 ) (y 2 : A 2 ), A R y 1 y 2 → x 1 = y 1 → x 2 = y 2 → Type := UR_eq_refl : UR_eq A 1 A 2 A R x 1 x 2 x R x 1 x 2 x R eq_refl eq_refl.
The univalent relation is just a specialization of UR_eq where A R is given by the relation induced by UR AB and with e and e ′ , so we set:

R eq ≜ λ(e 1 : a = A a ′ )(e 2 : b = B b ′ ). UR_eq A B UR AB .1 a b e a ′ b ′ e ′ e 1 e 2
To prove that (a = a ′ ) ≃ (b = b ′ ), it is necessary to use the coherence between the relation and the equivalence provided by UR AB . After rewriting, the equivalence to establish is

(a = A a ′ ) ≃ (↑a= B ↑a ′ )
This equivalence is again similar to a standard result of HoTT, namely equiv_functor_eq in the Coq HoTT library.

Finally, proving that the relation is coherent with equality amounts to show that

Π(e 1 e 2 : a = a ′ ). (e = e ′ ) ≃ UR_eq A B UR AB .1 a b e a ′ b ′ e ′ e 1 ↑e 2
This can be done by first showing the following equivalence17

UR_eq A B P x y H x ′ y ′ H ′ X Y ≃ (Y # (X # H ) = H ′ )
which means that the naturality square between H and H ′ commutes. □

The proofs that eq_refl and eq_rect are univalently parametric are direct by UR_eq_refl and elimination of UR_eq.

To deal with other indexed inductive types, one can follow a similar approach. Alternatively, it is possible to exploit the correspondence between an indexed inductive family and a subset of parameterized inductive family, established by [START_REF] Gambino | Wellfounded trees and dependent polynomial functors[END_REF], to prove the univalence of an indexed inductive family. In this correspondence, the property of the subset type is obtained from the identity type.

For instance, for vectors:

Vector A n ≃ Σ l : list A. length l = n
The length function computes the length of a list, as follows:

Definition length {A} (l: list A) : N := list_rect A (fun _ ⇒ N) O (fun _ l n ⇒ S n) l
where one can observe that the semantics of the index in the different constructors of vectors is captured in the use of the recursion principle list_rect. By the abstraction theorem, Σ l : list A. length l = n is univalently parametric, and thus so is Vect A n.

The Marriage of Univalence and Parametricity 1:29

UNIVALENT PARAMETRICITY IN COQ

The whole development of univalent parametricity exposed in this article has been formalized and implemented in the Coq proof assistant [Coq Development Team 2019], reusing several constructions from the HoTT library [START_REF] Bauer | The HoTT Library: A Formalization of Homotopy Type Theory in Coq[END_REF]]. We have formalized in Coq the univalent parametricity translation, in order to mechanically verify the content from §5-we do not discuss this effort here. Instead, we present the shallow embedding of the univalent relation in Coq, based on typeclass instances to define and automatically derive the univalent parametricity proofs of Coq constructions. This framework brings the benefits of univalent parametricity to standard Coq developments.

We first introduce the core classes of the framework ( §7.1), and then describe the instances for some type constructors ( §7.2). We explain how the use of typeclasses gives rise to a direct implementation of univalent transport à la carte ( §7.3). Finally, we discuss several refinements to the framework to circumvent the limitation of relying on the univalence axiom in Coq ( §7.4).

Coq Framework

The central notion at the heart of this work is that of type equivalences, which we formulate as a typeclass to allow automatic inference of equivalences: 18Class IsEquiv (A B : Type) (f :

A → B) := { e_inv : B → A; e_sect : ∀ x, e_inv (f x) = x; e_retr : ∀ y, f (e_inv y) = y; e_adj : ∀ x, e_retr (f x) = ap f (e_sect x) }.
The properties e_sect and e_retr express that e_inv is both the left and right inverse of f, respectively. The property e_adj is a compatibility condition between the proofs. It ensures that the equivalence is uniquely determined by the function f.

While IsEquiv characterizes a particular function f as being an equivalence, we say that two types A and B are equivalent, noted A ≃ B, iff there exists such a function f . Class Equiv A B := { e_fun :> A → B ; e_isequiv : IsEquiv e_fun }. Infix "≃" := Equiv.

Equiv is here defined as a typeclass to allow automatic inference of equivalences. This way, we can define automatic univalent transport as follows:

Definition univalent_transport {A B : Type} {e : A ≃ B} : A → B := e_fun e. Notation "↑ ■ " := univalent_transport.
where the equivalence is obtained through typeclass instance resolution, i.e., proof search. Note also that the source and target types of transport are implicitly resolved by default.

To formalize univalent relations, we define a hierarchy of classes, starting from UR for univalent relations (arbitrary heterogeneous relations), refined by UR_Coh, which additionally requires the proof of coherence between a univalent relation and equality.

Class UR A B := { ur : A → B → Type }. Infix "≈" := ur. Class UR_Coh A B (e : Equiv A B) (H : UR A B) := { ur_coh : ∀ (a a' : A), Equiv (a = a') (a ≈ ↑ ■ a') }.
The attentive reader will notice that the definition of the coherence condition above is dual to the one stated in Figure 4. Both definitions are in fact equivalent. 19 The reason for adopting this dual definition is that it eases the definition of new instances.

As presented in Figure 4, two types are related by the univalent parametricity relation if they are equivalent and there is a coherent univalent relation between them. This is captured by the typeclass UR_Type.

Class UR_Type A B := { Ur :> UR A B; equiv :> A ≃ B; Ur_Coh :> UR_Coh A B equiv Ur; Ur_Can A :> Canonical_eq A; Ur_Can B :> Canonical_eq B }. Infix "▷◁" := UR_Type.
The last two attributes are part of the Coq framework in order to better support extensibility and effectiveness, as will be described in §7.4.1.

Univalent Type Constructors

The core of the development is devoted to the proofs that standard type constructors are univalently parametric, notably Type and Π. In terms of the Coq framework, this means providing UR_Type instances relating each constructor to itself. These instance definitions follow directly the proofs discussed in §5.

For the universe Type i , we define:

Instance UR_Type_def@{i j} : UR@{j j j} Type@{i} Type@{i} := {| ur := UR_Type@{i i i} |}.

This is where our fixpoint construction appears: the relation at Type i is defined to be UR_Type itself. So, for a type to be in the relation means more than mere equivalence: we also get a relation between elements of that type that is coherent with equality. This UR_Type_def instance will be used implicitly everywhere we use the notation X ≈ Y, when X and Y are types themselves.

For dependent function types, we set:

Definition UR_Forall A A' (B : A → Type) (B' : A' → Type) (dom : UR A A') (codom: ∀ x y (H : x ≈ y), UR (B x) (B' y)) : UR (∀ x, B x) (∀ y, B' y) := {| ur := fun f g ⇒ ∀ x y (H: x ≈ y), f x ≈ g y |}.
The Marriage of Univalence and Parametricity 1:31

The univalent parametricity relation on dependent function types expects relations on the domain and codomain types, the latter being parameterized by the former through its argument (H : x ≈ y). The definition is the standard extensionality principle on dependent function types.

Then, we need to show that the universe is related to itself according to the relation on the universe at one level above. This corresponds to Proposition 5.1, and thanks to both universe polymorphism and implicit management of universe levels in Coq, there is no need to mention levels at all (note that Type ≈ Type in the definition actually computes to Type ▷◁ Type):20 Definition FP_Type : Type ≈ Type.

Regarding the dependent product, the Equiv instance that needs to be defined in order to show that it is univalently parametric has the following type:

Instance Equiv_∀ : ∀ (A A' : Type) (e A : A ≈ A') (B : A → Type) (B' : A' → Type) (e B : B ≈ B'), (∀ x : A, B x) ≃ (∀ x : A', B' x).
While the conclusion is an equivalence, the assumptions e A and e B are about univalent relations for A, A' and B and B'. The first one is implicitly resolved as the UR_Type_def defined above, and the second one as a combination of UR_Forall and UR_Type_def. With these stronger assumptions, and because ≈ is heterogeneous, we can prove the equivalence without introducing transports. This is key to make the typeclass instance proof search tractable: it is basically structurally recursive on the type indices. We can then show that the dependent function type seen as a binary type constructor is related to itself using the univalent relation and equivalence constructed above, and the coherence proof univ Π presented in the Abstraction Theorem (Th. 5.2):

Definition FP_∀ : (fun A B ⇒ (∀ x : A , B x)) ≈ (fun A' B' ⇒ (∀ x : A', B' x)).
To instrument the typeclass instance proof search, we add proof search Hints for each fundamental property.

We proceed similarly for other constructors: dependent pairs, the identity type, natural numbers and booleans with the canonical univalent relation, where we additionally prove the fundamental property for the eliminators. That is to say, we have many fundamental property lemmas such as:

Definition FP_Σ : @sigT ≈ @sigT.

Having spelled out the basics of the Coq framework for univalent parametricity, we can now turn to the practical issue of effective transport.

Univalent Transport à la Carte

Because the computation of the univalent parametricity relation is done using type class resolution, the framework is already set up to support extension with contexts of univalently-related constants, using typeclass instances. For example, to extend the context with the fact that two types A and B are univalently related, one needs to provide a proof that there is an equivalence between A and B, and declare it as a typeclass instance. Then, using for example the canonical relation fun (a : A) (b : B) ⇒ a = ↑ ■ b, one can construct an instance of A ▷◁ B. The user also needs to define an instance of B ▷◁ A using the symmetry of the relation, because typeclass resolution cannot be instrumented with a general rule for symmetry, otherwise proof search would never terminate. This way, typeclass resolution is able to automatically derive further instances of the relation based on this univalent relation instance.

Note that the relation between A and B does not have to be the canonical relation. For instance, coming back to the example of the equivalence between sized lists and vectors, the relation between sized lists and vectors can be based either on equality (plus transport using the equivalence), on the relation UR_list (plus transport using the equivalence), on a similar relation on vectors (plus transport using the equivalence) or even on a heterogeneous relation directly relating sized lists and vectors (without the use of transport). Of course, all these definitions are equivalent because of the coherence condition of univalent parametricity, but they can have different computational content and a user can favor one or the other, depending on the application in mind.

Going one step further, one can show that two functions defined on univalently-related types are in univalent relation. Let us say for example that f : A → A → A and g : B → B → B are in univalent relation, with witness univrel_fg. Then, to exploit this univalent relation to perform univalent transport à la carte, the user needs to add the following Hint to the proof search database:21 Hint Extern 0 (f _ _ ≈ g _ _) ⇒ eapply univrel_fg : typeclass_instances.

This declaration amounts to extending the global context of univalently-related constants with f and g.

In general, when adding new instances to univalent parametricity, the user needs to define corresponding Hints to enable automatic typeclass resolution. §8 explains in more details how the examples of §4 are realized, including such hints.

Effectiveness of Univalent Parametric Transport in Coq

The proofs of univalent parametricity we have developed in §5 are in a setting where univalence is realized as an axiom (CC ω and CIC). The axiomatic nature of the development manifests as follows:

(1) The univalence axiom proper is used to show the coherence condition of univalent parametricity for the universe ( §5.1). This is to be expected and unavoidable, as this condition for the universe exactly states that type equivalence coincides with equality. (2) Functional extensionality (an axiom in CIC, which follows from univalence) is used to show that the transport functions of the equivalence for the dependent product form an equivalence ( §5.2). Additionally, as shown in §6, the effectiveness of univalent transport for inductive types depends on the type of parameters and indices. In particular, proving univalent parametricity of indexed families requires using the coherence condition.

To see how this relates to practice, consider the case of functions. Functional extensionality is only used in the proof that the transport functions form an equivalence. In particular, this means that the transport functions themselves are effective. Therefore, when transporting a first-order function, the resulting function is effective.

For the axiom to interfere with effectiveness, we need to consider a higher-order function, i.e., that takes another function as argument. Consider for instance the conversion of a higher-order dependent function g operating on a function over natural numbers

g : ∀ (f : N → N), Vector N (f O)
The Marriage of Univalence and Parametricity 1:33

to one operating on a function over binary natural numbers

g' : ∀ (f : Bin → Bin), Vector Bin (f ↑ ■ O) := ↑ ■ g.
We transport g to g' along the equivalence between the two higher-order types above. Such a transport uses, in a computationally-relevant position, the fact that the function argument f can be transported along the equivalence between N → N and Bin → Bin. Consequently, the use of functional extensionality in the equivalence proof chimes in, and g' is not effective. (Specifically, g' pattern matches on an equality between natural numbers that contains the functional extensionality axiom.)

Fortunately, there are different ways to circumvent this problem, by exploiting the fact that univalent parametricity is specializable through specific typeclass instances. This section shows how we can further specialize proofs of univalent parametricity in situations where using axioms can be avoided. Sometimes we can ignore the fact that an equality proof might be axiomatic by automatically crafting a new one that is axiom-free ( §7.4.1), or we can avoid transporting type families with (potentially axiomatic) proofs of equality in some cases ( §7.4.2).

7.4.1 Canonical Equality for Types with Decidable Equality. Any proof of equality between two natural numbers can be turned into a canonical, axiom-free proof using decidability of equality on natural numbers. In general, decidable equality on a type A can be expressed in type theory as Definition DecEq (A : Type) := ∀ x y : A, (x = y) + ¬(x = y).

Hedberg's theorem [START_REF] Hedberg | A coherence theorem for Martin-Löf's type theory[END_REF]] implies that if A has decidable equality, then A satisfies Uniqueness of Identity Proofs (UIP): any two proofs of the same equality between elements of A are equal. Hedberg's theorem relies on the construction of a canonical equality to which every other is shown equal. Specifically, when A has a decidable equality, it is possible to define a function Definition Canonical_eq_decidable A (Hdec : DecEq A) : ∀ x y : A, x = y → x = y := fun x y e ⇒ match Hdec x y with | inl e0 ⇒ e0 | inr n ⇒ match (n e) with end end.

This function produces an equality between two terms x and y of type A by using the decision procedure Hdec, independently of the equality e. In the first branch, when x and y are equal, it returns the canonical proof produced by Hdec, instead of propagating the input (possibly-axiomatic) proof e. And in case the decision procedure returns an inequality proof (of type x=y → False), the function uses e to establish the contradiction. In summary, the function transforms any equality into a canonical equality by using the input equality only in cases that are not possible.

We can take advantage of this insight to ensure effective transport on indices of types with decidable equality. The general idea is to extend the relation on types A ▷◁ B to also include two functions ∀ x y : A , x = y → x = y and ∀ x y : B , x = y → x = y. For types with decidable equality, these functions can exploit the technique presented above, and for others, these are just the identity. However, care must be taken: we cannot add arbitrary new computational content to the relation; we have to require that these functions preserve reflexivity. This is specified in the following class:

Class Canonical_eq (A : Type) := { can_eq : ∀ (x y : A), x = y → x = y ; can_eq_refl : ∀ x, can_eq x x eq_refl = eq_refl }. which is used for the last two attributes of the UR_Type class given in §7.1.

There are two canonical instances of Canonical_eq, the one that is defined on types with decidable equality, and exploits the technique above, and the default one, which is given by the identity function (and proof by reflexivity).

Using this extra information, it is possible to improve the definition of univalent parametricity by always working with canonical equalities. This way, equivalences for inductive types whose indices are of types with decidable equality-like length-indexed vectors and many common examplesnever get stuck on rewriting of indices.

7.4.2 Canonically-Transportable Predicates. As mentioned in the introduction of this section, for some predicates, it is not necessary to pattern match on equality to implement transport.

The simplest example is when the predicate does not actually depend on the value, in which case P x ≃ P y can be implemented by the identity equivalence because P x is convertible to P y, independently of what x and y are. It is also the case when the predicate is defined on a type with a decidable equality, so we can instead pattern match on the canonical equality ( §7.4.1).

To take advantage of this situation whenever possible, we introduce the notion of transportable predicates.

Class Transportable {A} (P : A → Type) := { transportable :> ∀ x y, x = y → P x ≃ P y; transportable_refl : ∀ x, transportable x x eq_refl = Equiv_id (P x) }.

Note that as for Canonical_eq, we need to require that transportable behaves like the standard transport of equality by sending reflexivity to the identity equivalence.

For instance, the instance for constant type-valued functions is defined as the dependency in B instead of pattern matching on the equality between the dependencies. This is possible because from e B : B ≈ B', we know that B is transportable (thanks to the specialized definition URForall_Type).

Instance

UNIVALENT PARAMETRICITY IN ACTION: EXPLAINED

We now come back to the examples of §4, explaining the definitions and adjustments of the typeclass resolution mechanism necessary to achieve seamless transport à la carte.

Adding a univalent relation in the global context. To declare that unary and binary natural numbers are univalently related, one first needs to provide a proof IsEquiv_of_N that the transport function Bin.of_N from N to Bin is actually an equivalence, and declare it as a typeclass instance.

Instance Equiv NBin : N ≃ Bin := BuildEquiv N Bin Bin.of_N IsEquiv_of_N. Then, using for example the canonical relation fun (n:Bin) (m:N) ⇒ n = ↑ ■ m to define the univalent relation UR_N_Bin between N and Bin, the only remaining piece is the proof of the following coherence condition, which can easily be done using the section of the equivalence. Transport à la carte. However, the fact that N and Bin are in univalent relation alone only provides black-box transport on functions manipulating integers. To get more efficient transport, one can do an additional proof effort in order to also get some white-box transport, exploiting the relation between some particular functions. For instance, one can prove that the addition functions on unary and binary numbers are univalently related:

Definition coherence

Definition univrel_add : plus ≈ plus Bin . This amounts to show that for every n m : N, we have plus n m = ↑ ■ (plus Bin (↑ ■ n) (↑ ■ m)). The proof can be done by induction on n. The O case requires showing that plus Bin O Bin m = m for every m : Bin, which is true by computation. The S case requires showing that plus Bin (S Bin n) m = S Bin (plus Bin n m) for every n m: Bin. This property is more complex to prove because it must be done by induction on n and the definition of S Bin does not comply very well with the binary structure.

Next, to add this relation to the global context, we need to instrument typeclass resolution by defining the following hint, which will be used when looking for a function in relation with the plus function:

Hint Extern 0 (plus _ _ ≈ _) ⇒ eapply univrel_add : typeclass_instances.

With this hint, the system is able to automatically infer that the types ∀ n m : N, n + m = m + n and ∀ n m : Bin, n + m = m + n are in univalent relation using white-box transport. For instance:

Goal (∀ n m : N, n + m = m + n) ▷◁ (∀ n m : Bin, n + m = m + n). typeclasses eauto. Qed.
It is therefore possible to automatically transport the proof term of the commutativity of plus to a proof term of the commutativity of plus Bin using the black-box transport provided by this univalent relation.

Definition plus

Bin _comm : ∀ n m : Bin, n + m = m + n := ↑ ■ plus_comm.
Transporting goals. As explained in §4, univalent parametricity can also be used to prove properties by computation using an alternative representation that is more adequate computationally. For instance with the polynomial poly, the proof that poly 50 is bigger than 1000 can be done by moving to an equivalent property on binary natural numbers first, and then solving the goal by computation and basic inversion.

Goal poly 50 ≥ 1000.

replace_goal; now compute. Defined.

The tactic replace_goal proceeds by first asserting that there exists a property opt that is in univalent relation with the given goal (here poly 50 ≥ 1000), and inferring this equivalent property through typeclass resolution using white-box transport. Then the equivalence induced by the univalent relation is used to replace the original goal with the inferred property opt; this is black-box transport. The definition of the replace_goal tactic is simple in Ltac:

Ltac replace_goal := match goal with | ⊢ ?P ⇒ let X := fresh "X" in refine (let X := _ : { opt : Prop & P ≈ opt} in _);

[ eexists; typeclasses eauto | apply (e_inv (equiv X.2))] end.

It first introduces the definition of a property opt that is in univalent relation with P. This property opt is obtained automatically by triggering the typeclass resolution on P ≈ ?, finding a

The Marriage of Univalence and Parametricity 1:37 canonical instance. If it succeeds, this step gives at the same time the definition of opt and the proof that it is in univalent relation with P. In particular, this proof contains an equivalence between P and opt, which is used to replace the goal P by opt, using the inverse function of the equivalence.

Fixpoints. The proof technique above also scales to fixpoints, even though fixpoints must be dealt with in a non-generic way. Concretely, one needs to provide a univalent parametricity instance for each case of pattern matching performed inside the fixpoint. In the sequence example of §4.3, the required instance must be defined for fixpoint matching on 0, 1, and 2: Definition fix N3 :

(fun P X0 X1 X2 XS ⇒ fix f (n : N) {struct n} :

P := match n with | 0 ⇒ X0 | 1 ⇒ X1 | 2 ⇒ X2 | S n ⇒ XS n (f n) end) ≈ (fun P X0 X1 X2 XS ⇒ fix f (n : N) {struct n} : P := match n with | 0 ⇒ X0 | 1 ⇒ X1 | 2 ⇒ X2 | S n ⇒ XS n (f n) end).
The proof of this instance is systematic, and can be done automatically using induction and typeclasses eauto. However, because pattern matchings are not first-class objects in Coq, it is not possible to define a single generic univalent parametric instance for every fixpoint. Note that this (practical, rather than theoretical) issue does not manifest when using eliminators, because there is only one eliminator per inductive type.

Limitations of the current Coq implementation. The use of typeclasses and typeclass resolution to deal with the global context of univalently related constants is both a blessing and a curse. It is nice because it allows us to instrument univalent parametricity in Coq without modifying the source code, offering great flexibility and accessibility. But this approach does not scale very well to large developments because typeclass resolution is internally based on proof search, which quickly becomes intractable. In practice, in our current implementation, we observe that successful typeclasss resolution is fairly fast, but when the proof search fails because of some missing Hints, resolution can take a very long time or may even diverge.

This issue is a known limitation of using typeclasses to drive automatic program transformations, and can also be experienced in other frameworks like CoqEAL [START_REF] Cohen | Refinements for Free![END_REF]]. It could be addressed via a direct implementation of univalent parametricity, for instance using MetaCoq [Sozeau et al. 2020a,b]. With a MetaCoq plugin, it is possible to have complete access to the reification of a term of Coq in Coq. This would provide complete programmatic control over the univalent parametricity translation, thereby avoiding issues that follow from relying on proof search. Another possibility is to implement the translation directly as a Coq plugin in OCaml, as has recently been done for the white-box approach by [START_REF] Ringer | Ornaments for Proof Reuse in Coq[END_REF]. However, the direct definition of a plugin is very sensitive to changes in the implementation of the Coq proof assistant itself, so we believe that the MetaCoq approach would be better suited, as it provides an abstraction barrier between the theory of Coq and its actual implementation.

Definition lsl_add_distr

: ∀ x y n, (x + y) << n = (x << n) + (y << n) := ↑ ■ ZwB_lsl_add_distr.
In contrast, the proof of lsl_add_distr in the Coq standard library is done manually, and in fact does not even use the auxiliary lemma ZwB_lsl_add_distr. Instead, the proof is dealing with both the conversion to Z and the proof of the property on Z at the same time. We believe that systematically proving properties first on ZwB, and then automatically transporting them to int simplifies development, maintenance, and understanding.

RELATED WORK

Type theories. Homotopy Type Theory [Univalent Foundations Program 2013] treats equality of types as equivalence. For regular datatypes (also known as homotopy sets or hSets), equivalence boils down to isomorphism, hence the existence of transports between the types. However, as univalence is considered as an axiom, any meaningful use of the equality type to transport terms along equivalences results in the use of a non-computational construction. In contrast, in this work we carefully delimit the effective equivalence-preserving type constructors in our setting, pushing axioms as far as possible, and supporting specialized proofs to avoid them in certain scenarios.

Cubical Type Theory [START_REF] Cohen | Cubical Type Theory: a constructive interpretation of the univalence axiom[END_REF]] provides computational content to the univalence axiom, and hence functional and propositional extensionality as well. In this case, the invariance of constructions by type equivalence is built in the system and the equality type reflects it. Note that the recent work of [START_REF] Altenkirch | Towards a Cubical Type Theory without an Interval[END_REF] on a cubical type theory without an interval proposes to use a relation quite close to the one defined in univalent parametricity to encode equality in the theory. They are handling a different problem (albeit in a similar way), because they are trying to build a theory that supports univalence. In our framework, we relate the relation to equality and type equivalence, which allows us to stay within CIC, without relying on another more complex type theory, but the price we pay is to assume univalence as an axiom. Note that while we focus on CIC extended with the univalence axiom, univalent parametricity could be likewise developed in a cubical theory, such as Cubical Agda [START_REF] Vezzosi | Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types[END_REF]. The only change is that the definition of univalent relations for types and functions can make use of top-level equality directly instead of using explicit extensional definitions such as type equivalence and pointwise equality. In particular, terms such as Equiv Π or univ Π ( §5) can be largely simplified. But the interest of the general relational univalent parametric setting remains unchanged because it provides heterogeneous automatic transport, which is not readily available in cubical type theories.

Observational Type Theory (OTT) [START_REF] Altenkirch | Observational equality, now![END_REF]] uses a different notion of equality, coined John Major equality. It is a heterogeneous relation, where terms in potentially different types can be compared, usually with the assumption that the two types will eventually be structurally equal, not merely equivalent. This stronger notion of equality of types is baked in the type system, where type equality is defined by recursion on the structure of types, and value equality follows from it. It implies the K axiom, which is in general inconsistent with univalence, although certainly provable for all the non-polymorphic types definable in OTT. A system similar to ours could be defined on top of OTT to allow transporting by equivalences.

Parametric Type Theory and the line of work integrating parametricity theory to dependent type theory, either internally [START_REF] Bernardy | A Presheaf Model of Parametric Type Theory[END_REF] or externally, is linked to the current work in the sense that our univalent parametricity translation is a refinement of the usual parametricity translation. In its simple form, parametricity in type theory does not admit an identity extension lemma, which ensures that if we pass the identity type as relations for the arguments of type constructors, then the resulting relation for the type constructor is equivalent to the identity. This

The Marriage of Univalence and Parametricity 1:41 issue has been addressed, first on small types [START_REF] Atkey | A Relationally Parametric Model of Dependent Type Theory[END_REF]] by considering the reflexive graph model and then on an extension of type theory with a parametric function type [START_REF] Nuyts | Parametric Quantifiers for Dependent Type Theory[END_REF]].

In our work, we get a variant of the identity extension lemma very easily because all the relations we consider need to be related to equality through the coherence condition. However, we do not exactly get identity extension: for instance on the type of booleans B, it is also possible to provide the relation which says that true is related to false (and dually), together with the equivalence which flips booleans. This defines a univalent relation on B because it satisfies the coherence condition, but the relation does not coincide with equality on booleans-it only does up to flipping booleans.

Recently, [START_REF] Cavallo | Internal Parametricity for Cubical Type Theory[END_REF] proposed a theory mixing both cubical type theory and parametric type theory. However, they are not considering univalent parametricity, but rather a theory where proofs of parametricity can make use of univalent principles, such as functional extensionality or the univalence axiom.

For Extensional Type Theory, [START_REF] Neelakantan | Internalizing Relational Parametricity in the Extensional Calculus of Constructions[END_REF] develop an alternative view on parametricity, more in the style of Reynolds, by giving a parametric model of the theory using quasi-PERs and a realizability interpretation of the theory. From this model construction and proof of the fundamental lemma they can justify adding axioms to the theory that witness strong parametricity results, even on open terms. However they lose the computability and effectiveness enjoyed by both Bernardy's construction and ours, which are developed in intensional type theories.

The parametricity translation of [START_REF] Anand | Revisiting Parametricity: Inductives and Uniformity of Propositions[END_REF] extends the logical relation on propositions to force that related propositions are logically equivalent. It can be seen as a degenerate case of our approach that forces related types to be equivalent, considering that equivalence boils down to logical equivalence on propositions (see §5.2.1 for a more detailed explanation). However the translations differ in other aspects. While our translation requires the univalence axiom, theirs assumes proof irrelevance and the K axiom, and does not treat the type hierarchy. Our solution to the fixpoint arising from interpreting Type i : Type i+1 is original, along with the use of conditions to ensure coherence with equality. They study the translation of inductively-defined types and propositions in detail, giving specific translations in these two cases to accommodate the elimination restrictions on propositions, and are more fine-grained in the assumptions necessary on relations in parametricity theorems. In both cases, the constructions were analyzed to ensure that axioms were only used in the non-computational parts of the translation, hence they are effective.

Relational parametricity in type theory can be understood categorically in terms of inverse diagrams. Indeed, given a category with attributes (CwA) C, the category of inverse diagrams C Span (where Span is the "walking Span" category : 0 ← 01 → 1) is also a CwA where a type is now a triple of two types and a relation between them. This interpretation does not extend directly to univalent parametricity but the notion of homotopical inverse diagrams recently developed by [START_REF] Kapulkin | Homotopical inverse diagrams in categories with attributes[END_REF] seems to provide a categorical interpretation of univalent parametricity-namely, as inverse diagrams over the category • → • with two objects and one arrow between them which is "marked" as an equivalence. [START_REF] Kapulkin | Homotopical inverse diagrams in categories with attributes[END_REF] show that under the assumption that the CwA C satisfies functional extensionality, the category C •→• is also a CwA. However, they do not investigate the interpretation of universes and univalent universes as done for instance by [START_REF] Shulman | Univalence for inverse diagrams and homotopy canonicity[END_REF]. Our work suggests that the interpretation of universes for homotopical inverse diagrams can only be done for univalent universes, in the same way as dependent products can only be lifted in presence of functional extensionality.

Data refinement. Another part of the literature deals with the general data refinement problem, e.g. the ability to use different related data structures for different purposes: typically simplicity of proofs versus efficient computation. The frameworks provide means to systematically transport results from one type to the other. [START_REF] Magaud | Changing Data Structures in Type Theory: A Study of Natural Numbers[END_REF] and [START_REF] Magaud | Changing Data Representation within the Coq system[END_REF] first explored the idea of transporting proof terms from one data representation to another in Coq, assuming that the user provides a translation of the definitions from one datatype to the other. It is limited to isomorphism and implemented externally as a plugin. The technique is rather invasive in the sense that it supports the transport of proof terms that use the computational content of the first type (e.g., the reduction rules for plus on natural numbers) by making type conversions explicit, turning them into propositional rewrite rules. This approach breaks down in presence of type dependencies.

In CoqEAL [START_REF] Cohen | Refinements for Free![END_REF] refinement is allowed from proof-oriented data types to efficiencyoriented ones, relying on generic programming for the computational part and automating the transport of theorems and proofs. CoqEAL does not only deal with isomorphisms, but also quotients, and even partial quotients, which we cannot handle. The approach exploits parametricity for generating proofs, but it does not support general dependent types, only parametric polymorphism. Moreover, the advocated style prevents doing local transport and rather requires working with interfaces from the outset-which we coined the anticipation problem-and applying parametricity in a second step. We can avoid anticipating common interfaces thanks to our limitation to transport by equivalences.

In a categorical setting, [START_REF] Robinson | Parametricity as isomorphism[END_REF] uses parametricity for System F to show that when a function is defined on a type A using only the fact that it is isomorphic to a given type B, then the function can be transported to another type A ′ as long as it is also isomorphic to B. This approach to parametricity is similar to that of CoqEAL, which uses the fact that when working with an abstract interface-here an abstract copy of a type-the term does not depend on the implementation of the interface. This is different from the univalent parametricity approach we develop here, which works on two concrete types and functions defined on them, which can a posteriori be shown equivalent. [START_REF] Haftmann | Data Refinement in Isabelle/HOL[END_REF] explain how the Isabelle/HOL code generator uses data refinements to generate executable versions of abstract programs. The refinement relation used is similar to the partial quotients of CoqEAL. The Autoref tool for Isabelle [START_REF] Lammich | Automatic Data Refinement[END_REF]] also uses parametricity for refinement-based development. It is an external tool that synthesizes executable instances of generic algorithms and refinement proofs. [START_REF] Huffman | Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL[END_REF] address the problem of transferring propositions between different types, typically a representation type (e.g., integers) to an abstract type (e.g., natural numbers) in the context of Isabelle/HOL. Again this allows to relate a type and its quotient, like in CoqEAL, and is based on parametricity. Recently, [START_REF] Zimmermann | Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant[END_REF] present an algorithm and plugin to transport theorems along isomorphisms in Coq similar to that of [START_REF] Huffman | Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL[END_REF]. In addition to requiring the user to provide a surjective function f to relate two data types, their technique demands that the user explicitly provide transfer lemmas of the form ∀x 1 . . . x n , R(x 1 . . . x n ) =⇒ R ′ (f (x 1 ) . . . f (x n )), for each relation R that the user expects to transfer to a relation R ′ . The approach is not yet able to handle parameterized types, let alone dependent types and type-level computation.

Recently, [START_REF] Ringer | Ornaments for Proof Reuse in Coq[END_REF] developed a tool in Coq to automatically build equivalences between inductive types using the theory of ornaments [START_REF] Dagand | Transporting functions across ornaments[END_REF]. These equivalences are then instrumented to transport functions and proofs using a framework that is largely inspired by our previous conference article on univalent parametricity [START_REF] Tabareau | Equivalences for Free: Univalent Parametricity for Effective Transport[END_REF]]. However, the approach is implemented as a Coq plugin in OCaml. While this can be convenient to achieve full automation without relying on the somewhat brittle typeclass mechanism, it also presents major risks by being tied to a specific implementation of Coq. A direct implementation based on MetaCoq [Sozeau et al. 2020a,b] would seem preferable. Independently of the implementation The Marriage of Univalence and Parametricity 1:43 strategy, the tool developed by [START_REF] Ringer | Ornaments for Proof Reuse in Coq[END_REF] is essentially the white-box transport described in this article. Because they never perform black-box (univalent) transport, however, they also encountered the computation problem of parametricity described in § 2.3. We hope that the many clarifications provided in this extended and revised article will prove helpful for addressing these issues.

CONCLUSION

We have presented univalent parametricity, a fruitful marriage of parametricity and univalence that fully realizes programming and proving modulo equivalences in type-theoretic proof assistants. Univalent parametricity supports two complementary reasoning principles and forms of transport, resulting in transport à la carte: from a type equivalence, univalent transport operates in a black-box manner; additional proofs of equivalences between functions over related types allow heterogeneous parametricity to transport terms in a white-box manner up to these equivalences. We have shown how this makes it possible to conveniently switch between an easy-to-reason-about representation and a computationally-efficient representation. Our approach is realizable even in type theories where univalence is taken as an axiom, such as in Coq, and we have explored how to maximize the effectiveness of transport in this setting. Several examples and use cases in Coq attest to the practical impact of this work to provide easier-to-use proof assistants by supporting seamless programming and proving modulo equivalences.

Fig. 1 .

 1 Fig. 1. Definition of N and Bin in Coq

  is a monoid homomorphism *) 4. n + Bin m = m + Bin n (* by equivalence *)

Fig. 2 .

 2 Fig. 2. Parametricity translation for CC ω (from [Bernardy et al. 2012])

  and |Ξ| ε , the typing contexts obtained by projecting the respective components of each triple of Ξ, and |Ξ| the whole typing context |Ξ| • , |Ξ| • , |Ξ| ε .

Fig. 3 .

 3 Fig. 3. Transporting associativity from unary to binary naturals, in Cubical Agda (from [Vezzosi et al. 2019])

  2 n m to be passed to the eliminator of equality in order to define plus Bin _comm as Definition plus Bin _comm : ∀ (n m:Bin), plus Bin m n = plus Bin n m := eq_rect (Σ (A : Type), (A → A → A)) (N; plus) P_comm plus_comm (Bin; plus Bin ) e NBin

  intro n; rewrite plus_comm; reflexivity. Qed. can be transported automatically to the power function on binary natural numbers: Definition pow Bin _prop : ∀ n:Bin, 3 ^(n + 1) = 3 * 3 ^n := ↑ ■ pow_prop.

  because in addition to the relation [[A]] u , we need an equivalence [[A]] eq u and a witness [[A]] coh u

  |Ξ| • ≡ N:Type, plus:N → N → N, mult:N → N → N and |Ξ| • ≡ Bin:Type, plus Bin :Bin → Bin → Bin, mult Bin :Bin → Bin → Bin. The Marriage of Univalence and Parametricity 1:23 As discussed in Section 4.1, applying the White Box FP to the term square directly gives us the term square Bin□ together with a proof that it is related to square in the context Ξ. But the White Box FP also automatically gives us that the two following types are related ∀ (n m : N), plus n m = plus m n ≈ ∀ (n m : Bin), plus Bin n m = plus Bin m n : Type ▷◁ Type because ∀ (n m : Bin), plus Bin n m = plus Bin m n is the prime translation of ∀ (n m : N), plus n m = plus m n.

  Proof. Unfolding the definition, this amounts to defining an inhabitant of [[Type]] u given two types A, B related by UR AB : A ≈ B : Type ▷◁ Type, two terms a in A, b in B related by e : a ≈ b : A ▷◁ B and two terms a ′ in A ′ , b ′ in B related by e ′ : a ′ ≈ b ′ : A ▷◁ B.

  Transportable_cst A B : Transportable (fun _ : A ⇒ B) := {| transportable := fun (x y : A) _ ⇒ Equiv_id B; transportable_refl := fun x : A ⇒ eq_refl |}.To propagate the information that every predicate (a.k.a. type family) comes with its instance of Transportable, we specialize the definition of UR (A → Type) (A' → Type):Class URForall_Type_class A A' {dom : UR A A'} (P : A → Type) (Q : A' → Type) := { transport_ :> Transportable P; ur_type :> ∀ x y (H:x ≈ y), P x ▷◁ Q y }. Definition URForall_Type A A' {HA : UR A A'} : UR (A → Type) (A' → Type) := {| ur := fun P Q ⇒ URForall_Type_class A A' P Q |}.This definition says that two predicates are in relation whenever they are in relation pointwise, and when P is transportable.Using Transportable, we can instrument the definition of univalent relation on dependent products to improve effectiveness. More precisely, in the definition of the inverse function that defines the equivalence (∀ x : A, B x) ≃ (∀ x : A', B' x) we use the fact that B is transportable to changeThe Marriage of Univalence and Parametricity 1:35

  NBin : ∀ a a' : N, (a = a') ≃ (a = Bin.to_N (Bin.of_N a')).Then, one can define an instance of N ▷◁ Bin.Instance univrelNBin : N ▷◁ Bin := {| equiv := Equiv NBin ; Ur := UR_N_Bin; Ur_Coh := {| ur_coh := coherence NBin |}; |} This way, typeclass resolution is able to automatically derive further instances of the relation based on this basic univalent relation, emulating the White Box FP of Corollary 5.3. For instance, Coq can automatically infer the relation between N → N → N and Bin → Bin → Bin because it is equal to ↑ □ (N → N → N):Goal N → N → N ▷◁ Bin → Bin → Bin. typeclasses eauto. Qed.

  in the current global context Ξ, and we implicitly assume it is the case when we use this notation. The definition of the parametricity translation of Figure2for closed terms is the special homogeneous case, where there is no global context and where terms are related at the same type, i.e.,[[A]] p a 1 a 2 corresponds to a 1 ≈ p a 2 : A ▷◁ p A.The heterogeneous version of the parametricity translation makes it possible to relate terms of different types, such as O ≈ p O Bin : N ▷◁ p Bin, assuming that N ≈ p Bin : Type ▷◁ p Type appears in the global context. Hereafter, whenever a ≈ p b : A ▷◁ p B holds, we say that a and b are With the notation that makes the global context implicit, the parametricity relation on dependent functions can be expressed as: f ≈ p д : Πa : A.P a ▷◁ p Πb : B.Q b ≜ Π (a : A) (b : B). a ≈ p b : A ▷◁ p B → f a ≈ p д b : P a ▷◁ p Q b assuming A ≈ p B : Type ▷◁ p Type and P ≈ p Q : A → Type ▷◁ p B → Type.

	The Marriage of Univalence and Parametricity	1:9
	parametrically related.
	To avoid mentioning the global context explicitly, we introduce the notation
	a ≈ p b : A ▷◁ p B ≜ [[A]] Ξ p a b
	which relates two terms a and b at two related-but potentially different-types A and B. Of course,
	this notation only makes sense when B = [A] Ξ

□

J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

CC ω features a predicative hierarchy of universes Type i , and also an impredicative universe Prop. In this paper, we focus on the predicative hierarchy, because adding an impredicative universe has little impact. Section 5.2.1 explains the minor changes for integrating the impredicative universe Prop.

This function definition corresponds to the infix notation + N used in §1. J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

Note that this issue appears because we are working with an intensional type theory. It would not be present in an extensional type theory, but in this work we only consider theories with a decidable type checking algorithm. J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

This function definition corresponds to the infix notation + Bin used in §1. J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

In the following, arithmetic operations in expressions are denoted with the same infix symbols (such as + and * ); the actual operation is unambiguously determined by the type of its operands. J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

We thank Assia Mahboubi for suggesting this example, taken from an actual mechanized mathematics exercise.

Such an inhabitant is thus a dependent 3-tuple. We will later use syntactic sugar t = (a; b; c) with accessors t .1 t .2 and t .3 for nested pairs to ease reading.

From an equivalence e : A ≃ B we can extract functions ↑ B : A → B and ↑ A : B → A. We simply write ↑ e to refer to either one as required by the context; these correspond to univalent (aka. black-box) transport. Also, in the following, when e is clear from the context, we often omit it and simply write ↑, as in the Coq examples of §4.

The possibility to distinguish the translation of a type on the left and right-hand side of a judgment has already been noticedfor other translations that add extra information to types by[START_REF] Boulier | The next 700 syntactical models of type theory[END_REF]. For instance, to prove the independence of univalence with CIC, they use a translation that associates a Boolean to any type, e.g., [Type i ] = (Type i × B, true). Then a type on the left-hand side is translated as a 2-tuple and [[A]] = [A].1. This possibility to add additional information in the translation of a type comes from the fact that types in CIC can only be "observed" through inhabitance, that is, in a type position; therefore, the translation in term positions may collect additional information.J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

≡ denotes equality by conversion. J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

The definition of the inverse function requires using the retraction, and the proof that it forms a proper equivalence requires the adjunction condition ( §3.1). This means that the dependent function type would not be univalent if we replaced type equivalence with a simpler notion, such as the possibility to go from one type to another and back, or even by isomorphisms.J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

There is an equivalent presentation of inductive types with pattern matching instead of eliminators[START_REF] Goguen | Eliminating Dependent Pattern Matching[END_REF]].In Coq, eliminators are automatically inferred and defined using pattern matching.

In this section, to ease the reading, we navigate between the syntax of CIC and the one of Coq when appropriate.

Here, and in the following, we use the notation a ≈ b : A ▷◁ B extensively to avoid explicitly mentioning the global context. J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

It is however impossible to prove that no term of type Expr Bin can be constructed without univalence, because the univalence axiom is compatible with CIC. J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

The notation e # t , with e : x = y and t : P x when P is clear from the context, denotes the transport of the term e through the equality proof e (hence e # t : P y).J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

Adapted from: http://hott.github.io/HoTT/coqdoc-html/HoTT.Overture.html. J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

See lemma is_equiv_alt_ur_coh in the Coq development. J. ACM, Vol. 1, No. 1, Article 1. Publication date: January

Some universe annotations appear in the Coq source files in order to explicitly validate our assumptions about universes. J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

We use hint declarations to have precise control over the shape of goals a typeclass instance should solve and how. J. ACM, Vol. 1, No. 1, Article 1. Publication date: January 2020.

See https://github.com/coq/coq/blob/v8.10/theories/Numbers/Cyclic/Int63/Int63.v

ACKNOWLEDGMENTS

We thank the reviewers of the original ICFP 2018 publication, as well as the ICFP 2018 participants for asking several questions that forced us to better understand the limits of our initial proposal. This eventually led us to the enhanced presentation of this article. We are thankful as well to Assia Mahboubi for suggesting concrete applications for validating the use of our approach, which likewise pushed us to extend and enhance this work on univalent parametricity. Finally, we are extremely grateful to the anonymous JACM reviewers for their acute and eminently helpful comments and suggestions, which have resulted in considerable clarifications and more precise expositions of the concepts.

* This work is partially funded by CONICYT FONDECYT Regular Project 1190058, CONICYT REDES Project 170067, ERC Starting Grant CoqHoTT 637339 and Inria Équipe Associée GECO. , Gallinette Project-Team, Inria,

CASE STUDY: NATIVE INTEGERS

To further illustrate the applicability of univalent parametricity, we consider a case study based on a recent improvement to Coq: native 63-bits integers, available starting with Coq 8. 10. 22 This extension raises the question of how to interface a native datatype within Coq, supporting reasoning about (and with) such native values.

Native integers provide a basic datatype int together with native functions such as the left lshift operator a << b, which shifts each bit in a to the left by the number of positions indicated by b. These are defined as follows:

Register int : Set as int63_type. Primitive lsl := #int63_lsl. Infix "<<" := lsl (at level 30, no associativity) : int63_scope.

Because the operations are native, there is no direct way to reason about them in Coq. This is why the standard library of Coq relates int to binary numbers Z (these are similar to Bin, but include negative numbers), and states axioms to specify the behavior of native functions.

The statements of of_to Z and lsl_spec are very natural, but the first question it raises is about completeness: How can we be sure that these two axioms are enough to prove any property on lsl? For instance, do we also need to postulate that to Z forms a retraction?

Actually, it is possible to derive the other part of the correspondence between int and Z (note that this is not an axiom, it is proven by induction on z in Z):

Considering of_to Z and of Z _spec, it would seem that int and Z are indeed univalently related and that functions on int can likewise be univalently related to functions on Z. Actually, the careful reader might have noticed that of Z _spec does not exactly correspond to the statement of a retraction on to Z . This is because int is actually in relation with Z/2 63 Z. Therefore, we can define Z/2 63 Z as the type ZwB of integers between 0 and 2 63 , and adjust to Z and of Z accordingly.

Lemma to Z _bounded : ∀ x, 0 ≤ to Z x < wB. Definition to ZwB : int63 → ZwB := fun x ⇒ (to Z x; to Z _bounded x). Definition of ZwB (z:ZwB) : int63 := of Z z.1.

The Marriage of Univalence and Parametricity 1:39

The axioms of_to Z and lsl_spec are exactly what is required to show that int and ZwB are univalently related and that the native function lsl is univalent related to the corresponding function on ZwB. We have illustrated the correspondence between int and ZwB using the lsl function, but the very same can be done for all functions of the native integers interface.

Definition IsEquiv_to

Once this is done, it is possible to use univalent parametricity to go beyond what is currently provided in the Coq standard library, such as proving concrete properties on ZwB using an automatic transport to int. Consider the following polynomial, and two similar proofs by computation: the first directly on ZwB, and the second on int after transport. replace_goal. Time reflexivity. Defined.

Definition poly

While both executions of reflexivity terminate, the execution time when the goal is not shifted to int is two orders of magnitude slower than when it is (0.3s vs. 0.002s). The difference for this precise (artificial) example may not seem that significant in absolute terms, but we can expect it to be interesting in large-scale developments, which could justify the use of native integers.

The second-maybe more important-advantage of organizing all the axioms on the specification of the functions on native integers using univalent parametricity is that it guarantees completeness of the axiomatization. Indeed, by the White Box FP (Corollary 5.3), we are certain that any theorem on int and its native functions is univalently related to a theorem on ZwB. And by the Black Box FP (Proposition 5.4), such univalent relation allows us to easily transport the proof of this theorem on ZwB to a proof of the corresponding theorem on int. For instance, the distributivity of << over addition can be automatically transported from ZwB to int: Definition ZwB_lsl_add_distr x y n : (x + y) << n = (x << n) + (y << n). (* proof using properties of mod and automation on Z *)