科研之友
微信
新浪微博
Facebook
分享链接
摘要
<jats:p>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<jats:italic>et al.</jats:italic>2012).</jats:p>
- 出版日期2015-6
