An experimental library of formalized Mathematics based on the univalent foundations
Vladimir Voevodsky · Mathematical Structures in Computer Science · 2015
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 Kapulkinet al.2012).