Univalent Foundations (UF) were designed by Voevodsky as a foundation of mathematics that is "invariant under equivalence", meaning that constructions and proofs transfer across equivalence of mathematical structures. UF is particularly well-suited to the formalization of the theory of (higher) categories; the so-called "univalent" categories (and higher analogs) are particularly well-behaved: universal objects therein are actually unique, and constructions on univalent categories transfer along equivalence. The work is largely contained in showing that a category is univalent.
UniMath is a library of computer-checked mathematics in the univalent style, based on the computer proof assistant Coq. It aims to accommodate all of mathematics, but has seen most growth in the area of category theory and bicategory theory. In this talk, I will give an overview of the part of the UniMath library concerned with (higher) categories, including the mathematical tools developed to facilitate proofs of univalence of complicated (bi)categories.
Copyright. All Rights Reserved.