Hostname: page-component-74656f9884-c52kr Total loading time: 0 Render date: 2026-11-08T08:42:49.344Z Has data issue: false hasContentIssue false
  • English
  • Français

An experimental library of formalized Mathematics based on the univalent foundations

Published online by Cambridge University Press:  20 January 2015

VLADIMIR VOEVODSKY
VLADIMIR VOEVODSKY*
Affiliation:
School of Mathematics, Institute for Advanced Study, Princeton, New Jersey, U.S.A. Email: vladimir@ias.edu
Rights & Permissions [Opens in a new window]

Extract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the 'Save PDF' action button.

This is a short overview of an experimental library of Mathematics formalized in the Coq proof assistant using the univalent interpretation of the underlying type theory of Coq. I started to work on this library in February 2010 in order to gain experience with formalization of Mathematics in a constructive type theory based on the intuition gained from the univalent models (see Kapulkin et al. 2012).

References

Ahrens, B., Kapulkin, C. and Shulman, M. (2014) Univalent categories and the Rezk completion. Mathematical Structures in Computer Science http://dx.doi.org/10.1017/S0960129514000486.Google Scholar
Coquand, T. and Huet, G. (1988) The calculus of constructions. Information and Computation 76 (2–3) 95–120.Google Scholar
Grothendieck, A. (1997) Esquisse d'un programme. In: Geometric Galois Actions, 1, London Mathematical Society Lecture Note Series volume 242, Cambridge University Press, Cambridge 5–48. (With an English translation on pp. 243–283.)Google Scholar
Kapulkin, C., LeFanu Lumsdaine, P. and Voevodsky, V. (2012) The simplicial model of univalent foundations. Preprint, arXiv:1211.2851.Google Scholar
Luo, Z. (1994) Computation and Reasoning. A Type Theory for Computer Science, International Series of Monographs on Computer Science volume 11, The Clarendon Press. Oxford University Press, New York.Google Scholar
Makkai, M. (1995) First order logic with dependent sorts, with applications to category theory. Preprint, Available at: http://www.math.mcgill.ca/makkai/folds/foldsinpdf/FOLDS.pdf.Google Scholar
Paulin-Mohring, C. (1993) Inductive definitions in the system Coq: Rules and properties. In: Typed Lambda Calculi and Applications (Utrecht, 1993), Springer Lecture Notes in Computer Science volume 664 Berlin 328–345.Google Scholar
Pelayo, A., Voevodsky, V. and Warren, M. A. (2014) A preliminary univalent formalization of the p-adic numbers. Mathematical Structures in Computer Science http://dx.doi.org/10.1017/S0960129514000541.Google Scholar
Univalent Foundations Project (2013) Homotopy type theory: Univalent foundations for mathematics. Available at: http://homotopytypetheory.org/book.Google Scholar
Voevodsky, V. (2011) Resizing rules, slides from a talk at TYPES2011. Available at: https://github.com/vladimirias/2011_Bergen.Google Scholar
Supplementary material: File

Voevodsky supplementary material

Supplementary material

Download Voevodsky supplementary material(File)
File 878.6 KB