Lecture: UniMath

Vladimir Voevodsky

Abstract:

UniMath is the name of the library of formalized mathematics and related formalization tools that Benedikt Ahrens, Daniel Grayson, Michael Warren and myself started to build a little over a year ago based in the earlier code created in 2009-2014.

The library is written entirely in the univalent formalization style and it is implemented using a very small subset of the Coq proof assistant. I will tell about some of the features of this library and about some of the projects that use this library as a starting point.

---