G. Barthe, V. Capretta, and O. Pons, Setoids in type theory, Special Issue on Logical Frameworks and Metalanguages, vol.13, issue.2, pp.261-293, 2003.
URL : https://hal.archives-ouvertes.fr/hal-01124972

M. Sozeau, A New Look at Generalized Rewriting in Type Theory, Journal of Formalized Reasoning, vol.2, issue.1, pp.41-62, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00628904

L. Chicli, L. Pottier, and C. Simpson, Mathematical quotients and quotient types in Coq, Types for Proofs and Programs. Number 2646, pp.95-107, 2003.
DOI : 10.1007/3-540-39185-1_6

G. Gonthier, A. Mahboubi, and E. Tassi, A small scale reflection extension for the Coq system, INRIA Technical report
URL : https://hal.archives-ouvertes.fr/inria-00258384

T. M. Project, SSReflect extension and libraries

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging Mathematical Structures, Theorem Proving in Higher Order Logics, vol.5674, pp.327-342, 2009.
DOI : 10.1007/978-3-642-03359-9_23
URL : https://hal.archives-ouvertes.fr/inria-00368403

C. Cohen, Formalized algebraic numbers: construction and first order theory, 2012.
URL : https://hal.archives-ouvertes.fr/pastel-00780446

A. Saibi, Typing algorithm in type theory with inheritance, Principles of Programming Languages, pp.292-301, 1997.

M. Hedberg, A coherence theorem for Martin-Löf's type theory, Journal of Functional Programming, pp.4-8, 1998.

I. Bartzia and P. Y. Strub, A formalization of elliptic curves, 2011.
URL : https://hal.archives-ouvertes.fr/tel-01563979

C. Cohen and T. Coquand, A constructive version of laplace's proof on the existence of complex roots, Journal of Algebra, vol.381, issue.0, pp.110-115, 2013.

C. Cohen, Reasoning about big enough numbers in Coq, 2012.

C. Cohen, Construction of real algebraic numbers in Coq, ITP-3rd International Conference on Interactive Theorem Proving2012, 2012.
DOI : 10.1007/978-3-642-32347-8_6
URL : https://hal.archives-ouvertes.fr/hal-00671809

M. Hofmann, Extensional concepts in intensional type theory, 1995.
DOI : 10.1007/978-1-4471-0963-1

P. Courtieu, Normalized types, Proceedings of CSL2001, vol.2142, 2001.
DOI : 10.1007/3-540-44802-0_39

G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, and L. Théry, A Modular Formalisation of Finite Group Theory, 2007.
URL : https://hal.archives-ouvertes.fr/inria-00139131