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

source
class CategoryTheory.Bicategory.Strict (B : Type u) [Bicategory B] :
Prop

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

- id_comp {a b : B} (f : a ⟶ b) : CategoryStruct.comp (CategoryStruct.id a) f = f

  Identity morphisms are left identities for composition.

- comp_id {a b : B} (f : a ⟶ b) : CategoryStruct.comp f (CategoryStruct.id b) = f

  Identity morphisms are right identities for composition.

- assoc {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : CategoryStruct.comp (CategoryStruct.comp f g) h = CategoryStruct.comp f (CategoryStruct.comp g h)

  Composition in a bicategory is associative.

- leftUnitor_eqToIso {a b : B} (f : a ⟶ b) : leftUnitor f = eqToIso ⋯

  The left unitors are given by equalities

- rightUnitor_eqToIso {a b : B} (f : a ⟶ b) : rightUnitor f = eqToIso ⋯

  The right unitors are given by equalities

- associator_eqToIso {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) : associator f g h = eqToIso ⋯

  The associators are given by equalities

Instances

source
@[instance 100]
instance CategoryTheory.StrictBicategory.category (B : Type u) [Bicategory B] [Bicategory.Strict B] :
Category.{v, u} B

Category structure on a strict bicategory

Equations

- CategoryTheory.StrictBicategory.category B = { toCategoryStruct := inst✝¹.toCategoryStruct, id_comp := ⋯, comp_id := ⋯, assoc := ⋯ }

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