UniMath

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

View the Project on GitHub UniMath/UniMath

Bicategories

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