Documentation

Mathlib.CategoryTheory.Bicategory.Strict

Strict bicategories #

A bicategory is called Strict if the left unitors, the right unitors, and the associators are isomorphisms given by equalities.

Implementation notes #

In the literature of category theory, a strict bicategory (usually called a strict 2-category) is often defined as a bicategory whose left unitors, right unitors, and associators are identities. We cannot use this definition directly here since the types of 2-morphisms depend on 1-morphisms. For this reason, we use eqToIso, which gives isomorphisms from equalities, instead of identities.

A bicategory is called Strict if the left unitors, the right unitors, and the associators are isomorphisms given by equalities.

Instances