  Reasoning modulo equivalences is natural for everyone, including
mathematicians. Unfortunately, in proof assistants based on type theory,
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 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 in isolation, and then devises
a fruitful marriage between both. The resulting concept, univalent
parametricity, is an heterogeneous extension of parametricity strengthened with
univalence that fully realizes programming and proving modulo equivalences. In
addition to the theory of univalent parametricity, we present a lightweight
framework implemented in Coq 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 \`a 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 lift 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.
