B. Ahrens, C. Kapulkin, and M. Shulman, Univalent categories and the Rezk completion (2013), preprint

M. Barakat and M. Lange-hegermann, AN AXIOMATIC SETUP FOR ALGORITHMIC HOMOLOGICAL ALGEBRA AND AN ALTERNATIVE APPROACH TO LOCALIZATION, Journal of Algebra and Its Applications, vol.10, issue.02, pp.269-293, 2011.
DOI : 10.1142/S0219498811004562

M. Barakat and D. Robertz, homalg ??? A META-PACKAGE FOR HOMOLOGICAL ALGEBRA, Journal of Algebra and Its Applications, vol.07, issue.03, pp.299-317, 2008.
DOI : 10.1142/S0219498808002813

G. Barthe, V. Capretta, and O. Pons, Setoids in type theory, Journal of Functional Programming, vol.13, issue.02, pp.261-293, 2003.
DOI : 10.1017/S0956796802004501
URL : https://hal.archives-ouvertes.fr/hal-01124972

G. Cano and M. Dénès, MatricesàMatrices`Matricesà blocs et en forme canonique, JFLA -Journées francophones des langages applicatifs, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00779376

C. Cohen, Pragmatic Quotient Types in Coq, Interactive Theorem Proving, pp.213-228, 2013.
DOI : 10.1007/978-3-642-39634-2_17

T. Coquand, A. Mörtberg, and V. Siles, Coherent and Strongly Discrete Rings in Type Theory, pp.273-28812, 2012.
DOI : 10.1007/978-3-642-35308-6_21

T. Coquand and A. Spiwack, Towards Constructive Homological Algebra in Type Theory, pp.40-5407, 2007.
DOI : 10.1007/978-3-540-73086-6_4
URL : https://hal.archives-ouvertes.fr/inria-00432525

W. Decker and C. Lossen, Computing in Algebraic Geometry: A Quick Start using SINGULAR, 2006.

F. Garillot, G. Gonthier, A. Mahboubi, and L. Rideau, Packaging Mathematical Structures, TPHOLs'09, pp.327-342, 2009.
DOI : 10.1007/978-3-540-68103-8_11
URL : https://hal.archives-ouvertes.fr/inria-00368403

G. Gonthier and A. Mahboubi, A Small Scale Reflection Extension for the Coq system, Tech. rep., Microsoft Research INRIA, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00258384

G. Gonthier, Point-Free, Set-Free Concrete Linear Algebra, ITP'11, pp.103-118, 2011.
DOI : 10.1017/S0956796802004501
URL : https://hal.archives-ouvertes.fr/hal-00805966

G. M. Greuel and G. Pfister, A Singular Introduction to Commutative Algebra, 2007.
DOI : 10.1007/978-3-662-04963-1

A. Hatcher, Algebraic Topology, 2001.

M. Hedberg, A coherence theorem for Martin-L??f's type theory, Journal of Functional Programming, vol.8, issue.4, pp.413-436, 1998.
DOI : 10.1017/S0956796898003153

J. Heras, M. Dénès, G. Mata, A. Mörtberg, M. Poza et al., Towards a Certified Computation of Homology Groups for Digital Images, CTIC'12, pp.49-57, 2012.
DOI : 10.1007/978-3-642-30238-1_6
URL : https://hal.archives-ouvertes.fr/hal-00711385

J. Heras, T. Coquand, A. Mörtberg, and V. Siles, Computing persistent homology within Coq/SSReflect, ACM Transactions on Computational Logic, vol.14, issue.4, p.26, 2013.
DOI : 10.1145/2528929

I. Kaplansky, Elementary divisors and modules, Transactions of the American Mathematical Society, vol.66, issue.2, pp.464-491, 1949.
DOI : 10.1090/S0002-9947-1949-0031470-3

H. Lombardi and C. Quitté, Algèbre commutative, Méthodes constructives: Modules projectifs de type fini, Calvage et Mounet, 2011.

D. Lorenzini, Elementary Divisor domains and B??zout domains, Journal of Algebra, vol.371, issue.0, pp.609-619, 2012.
DOI : 10.1016/j.jalgebra.2012.08.020

R. Mines, F. Richman, and W. Ruitenburg, A Course in Constructive Algebra, 1988.
DOI : 10.1007/978-1-4419-8640-5

H. Poincaré, Analysis situs, Journal de l' ´ Ecole Polytechnique, vol.1, pp.1-123, 1895.

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