T. Altenkirch and A. Kaposi, Towards a cubical type theory without an interval, Leibniz International Proceedings in Informatics, 2017.

T. Altenkirch, C. Mcbride, and W. Swierstra, Observational equality, now!, Proceedings of the 2007 workshop on Programming languages meets program verification , PLPV '07, pp.57-68, 2007.
DOI : 10.1145/1292597.1292608

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

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

A. Bauer, J. Gross, P. Lefanu-lumsdaine, M. Shulman, M. 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, CPP 2017, pp.164-172, 2017.
DOI : 10.1017/S0960129514000577
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.
DOI : 10.1016/j.entcs.2015.12.006

J. Bernardy, P. Jansson, and R. Paterson, Proofs for free, Journal of Functional Programming, vol.83, issue.02, pp.107-152, 2012.
DOI : 10.1007/BFb0037116

S. Boulier, P. Pédrot, and N. Tabareau, The next 700 syntactical models of type theory, Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2017, pp.182-194, 2017.
DOI : 10.1109/LICS.1989.39193
URL : https://hal.archives-ouvertes.fr/hal-01445835

, Proc. ACM Program. Lang. Equivalences for Free!, vol.2, issue.26, p.29, 2018.

C. Cohen, T. Coquand, S. Huber, and A. Mörtberg, Cubical Type Theory: a constructive interpretation of the univalence axiom, 2016.
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), pp.147-162, 2013.
DOI : 10.1007/978-3-319-03545-1_10
URL : https://hal.archives-ouvertes.fr/hal-01113453

, The Coq Development Team. 2016. The Coq proof assistant reference manual

N. Gambino and M. Hyland, Wellfounded Trees and Dependent Polynomial Functors, Proceedings of Types for Proofs and Programs (TYPES 2003), pp.210-225, 2004.
DOI : 10.1007/978-3-540-24849-1_14

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), pp.100-115, 2013.
DOI : 10.1007/978-3-642-39634-2_10

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.
DOI : 10.1007/978-3-319-03545-1_9

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

P. Lammich, Automatic Data Refinement, Proceedings of the 4th International Conference on Interactive Theorem Proving, pp.84-99, 2013.
DOI : 10.1007/978-3-642-39634-2_9

N. Magaud, Changing Data Representation within the Coq System, International Conference on Theorem Proving in Higher Order Logics, 2003.
DOI : 10.1007/10930755_6

N. Magaud and Y. Bertot, Changing Data Structures in Type Theory: A Study of Natural Numbers, International Workshop on Types for Proofs and Programs, pp.181-196, 2000.
DOI : 10.1007/3-540-45842-5_12

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

C. Paulin-mohring, Introduction to the Calculus of Inductive Constructions In All about Proofs, Proofs for All, Studies in Logic (Mathematical logic and foundations), 2015.

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.

C. John and . 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.
DOI : 10.1007/11542384_8
URL : https://hal.archives-ouvertes.fr/inria-00628864

, The Univalent Foundations Program Homotopy Type Theory: Univalent Foundations of Mathematics, 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