An experimental library of formalized Mathematics based on the univalent foundations

摘要

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