This coq library aims to formalize a substantial body of mathematics using the univalent point of view.
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