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

    Identity morphisms are left identities for composition.

    Identity morphisms are right identities for composition.

    The associators are given by equalities

    @[simp]