T. Altenkirch, C. Mcbride, and W. Swierstra, Observational equality, now!, Proceedings of the Workshop on Programming Languages meets Program Verification, pp.57-68, 2007.

A. Anand and G. Morrisett, Revisiting Parametricity: Inductives and Uniformity of Propositions, 2017.

J. Bacon, The Untenability of Genera, Logique et Analyse, vol.17, pp.197-208, 1974.

A. Bauer, J. Gross, M. Peter-lefanu-lumsdaine, M. Shulman, B. Sozeau et al., The HoTT Library: A Formalization of Homotopy Type Theory in Coq, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, pp.164-172, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01421212

J. Bernardy, T. Coquand, and G. Moulin, A Presheaf Model of Parametric Type Theory, Electronic Notes in Theoretical Computer Science, vol.319, pp.67-82, 2015.

J. Bernardy, P. Jansson, and R. Paterson, Proofs for free: Parametricity for dependent types, Journal of Functional Programming, vol.22, issue.2, pp.107-152, 2012.

S. Boulier, P. Pédrot, and N. Tabareau, The next 700 syntactical models of type theory, Certified Programs and Proofs, pp.182-194, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01445835

C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical Type Theory: a constructive interpretation of the univalence axiom, vol.262, p.29, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01378906

C. Cohen, M. Dénès, and A. Mörtberg, Refinements for Free!, Proceedings of the International Conference on Certified Programming and Proofs (CPP 2013) (Lecture Notes in Computer Science, vol.8307, pp.147-162, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01113453

, The Coq proof assistant reference manual, 2019.

N. Gambino and M. Hyland, Wellfounded trees and dependent polynomial functors, Proceedings of Types for Proofs and Programs (TYPES 2003), vol.3085, pp.210-225, 2004.

F. Haftmann, A. Krauss, O. Kun?ar, and T. Nipkow, Data Refinement in Isabelle/HOL, Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP 2013) (Lecture Notes in Computer Science), vol.7998, pp.100-115, 2013.

B. Huffman and O. Kun?ar, Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL, Proceedings of the 3rd International Conference on Certified Programs and Proofs, pp.131-146, 2013.

R. Neelakantan, D. Krishnaswami, and . Dreyer, Internalizing Relational Parametricity in the Extensional Calculus of Constructions, Proceedings of the Conference for Computer Science Logic (CSL 2013, pp.432-451, 2013.

P. Lammich, Automatic Data Refinement, Proceedings of the 4th International Conference on Interactive Theorem Proving (ITP 2013) (Lecture Notes in Computer Science), vol.7998, pp.84-99, 2013.

N. Magaud, Changing Data Representation within the Coq system, International Conference on Theorem Proving in Higher Order Logics, vol.2758, 2003.

N. Magaud, Y. Bertot, ;. , P. Callaghan, and Z. Luo, Changing Data Structures in Type Theory: A Study of Natural Numbers, International Workshop on Types for Proofs and Programs (TYPES 2000) (Lecture Notes in Computer Science), vol.2277, pp.181-196, 2000.

P. Martin-löf, An Intuitionistic Theory of Types, 1971.

C. Paulin-mohring, Introduction to the Calculus of Inductive Constructions, Studies in Logic (Mathematical logic and foundations), vol.55, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01094195

D. Simon-peyton-jones, S. Vytiniotis, G. Weirich, and . Washburn, Simple unification-based type inference for GADTs, Proceedings of the 11th ACM SIGPLAN Conference on Functional Programming, pp.50-61, 2006.

J. C. Reynolds, Types, Abstraction and Parametric Polymorphism, IFIP Congress, pp.513-523, 1983.

M. Sozeau and N. Oury, First-Class Type Classes, Proceedings of the 21st International Conference on Theorem Proving in Higher-Order Logics, pp.278-293, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00628864

, The Univalent Foundations Program, Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013.

P. Wadler, Theorems for Free!. In Functional Programming Languages and Computer Architecture, pp.347-359, 1989.

T. Zimmermann and H. Herbelin, Automatic and Transparent Transfer of Theorems along Isomorphisms in the Coq Proof Assistant, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01152588