Lecture: UniMath

Vladimir Voevodsky

Abstract:

UniMath is a library of formalized mathematics that is based on the Univalent Foundations and written in what we call the UniMath language which is a small subset of the language of the Coq proof assistant. I wrote the core of the library under the name Foundations in 2010-11 to try out whether the Univalent Foundations can be used with Coq to formalize some real mathematics. After discovering that it can we, Benedikt Ahrens, Dan Grayson and myself, formed a GitHub organization called UniMath. Today UniMath has 12 authors, about 7 of them, including all three of the founders, are active in expanding and improving the library.

---