mathlib documentation

category_theory.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 eq_to_iso, which gives isomorphisms from equalities, instead of identities.

@[class]

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

Instances of this typeclass
@[simp]
theorem category_theory.bicategory.strict.assoc {B : Type u} [category_theory.bicategory B] [self : category_theory.bicategory.strict B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) :
(f ≫ g) ≫ h = f ≫ g ≫ h