This coq library aims to formalize a substantial body of mathematics using the univalent point of view.

View the Project on GitHub UniMath/UniMath


The contribution in this directory is illustrated and discussed in

Bicategories in Univalent Foundations
Benedikt Ahrens, Dan Frumin, Marco Maggesi, Niccolò Veltri, Niels van der Weide
Formal Structures for Computation and Deduction (FSCD) 2019, LIPIcs Vol. 131, pp. 5:1-5:17
DOI: 10.4230/LIPIcs.FSCD.2019.5

A revised and extended version of the same article will appear on Mathematical Structures in Computer Science.

Preprint versions: arXiv:1903.01152