# 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.

• id_comp : ∀ {a b : B} (f : a b),

Identity morphisms are left identities for composition.

• comp_id : ∀ {a b : B} (f : a b),

Identity morphisms are right identities for composition.

• assoc : ∀ {a b c d : B} (f : a b) (g : b c) (h : c d),

Composition in a bicategory is associative.

• leftUnitor_eqToIso : ∀ {a b : B} (f : a b),

The left unitors are given by equalities

• rightUnitor_eqToIso : ∀ {a b : B} (f : a b),

The right unitors are given by equalities

• associator_eqToIso : ∀ {a b c d : B} (f : a b) (g : b c) (h : c d), = CategoryTheory.eqToIso (_ : )

The associators are given by equalities

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

Instances

Category structure on a strict bicategory

@[simp]
theorem CategoryTheory.Bicategory.whiskerLeft_eqToHom {B : Type u} {a : B} {b : B} {c : B} (f : a b) {g : b c} {h : b c} (η : g = h) :
@[simp]
theorem CategoryTheory.Bicategory.eqToHom_whiskerRight {B : Type u} {a : B} {b : B} {c : B} {f : a b} {g : a b} (η : f = g) (h : b c) :