Equivalences for Free!: Univalent Parametricity for Effective Transport

Nicolas Tabareau 1, 2 Éric Tanter 3 Matthieu Sozeau 4, 5
Inria Rennes – Bretagne Atlantique , LS2N - Laboratoire des Sciences du Numérique de Nantes
4 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, Inria de Paris
Abstract : Homotopy Type Theory promises a unification of the concepts of equality and equivalence in Type Theory, through the introduction of the univalence principle. However, existing proof assistants based on type theory treat this principle as an axiom, and it is not yet entirely clear how to extend them to handle univalence internally. In this paper, we propose a construction grounded on a univalent version of parametricity to bring the benefits of univalence to the programmer and prover, that can be used on top of existing type theories. In particular, univalent parametricity strengthens parametricity to ensure preservation of type equivalences. 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. We study and strive to maximize the effectiveness of these transports in terms of computational behavior, relying on the univalence axiom as little as possible. Our approach handles both type and term dependency.
Type de document :
Pré-publication, Document de travail
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

Contributeur : Nicolas Tabareau <>
Soumis le : mardi 25 juillet 2017 - 14:45:14
Dernière modification le : mardi 16 janvier 2018 - 14:40:49


Fichiers produits par l'(les) auteur(s)


  • HAL Id : hal-01559073, version 2



Nicolas Tabareau, Éric Tanter, Matthieu Sozeau. Equivalences for Free!: Univalent Parametricity for Effective Transport. 2017. 〈hal-01559073v2〉



Consultations de la notice


Téléchargements de fichiers