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, displayed bicategories and some applications, including Categories with Families (CwF).

Started by Benedikt Ahrens, Marco Maggesi in February 2018. Extended by Dan Frumin and Niels van der Weide from November 2018 on.

Directory WkCatEnrichment contains an alternative definition of bicategory in the style of enrichment in 1-categories contributed by Mitchell Riley (see https://github.com/UniMath/UniMath/pull/409).


Basics about bicategories

Equivalence with with the presentation based on weakly enriched 1-categories

Displayed bicategories and other constructions

Application: Categories with Families (CwF)