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

• 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),

The associators are given by equalities

Instances
theorem CategoryTheory.Bicategory.Strict.id_comp {B : Type u} [self : ] {a : B} {b : B} (f : a b) :

Identity morphisms are left identities for composition.

theorem CategoryTheory.Bicategory.Strict.comp_id {B : Type u} [self : ] {a : B} {b : B} (f : a b) :

Identity morphisms are right identities for composition.

theorem CategoryTheory.Bicategory.Strict.assoc {B : Type u} [self : ] {a : B} {b : B} {c : B} {d : B} (f : a b) (g : b c) (h : c d) :

Composition in a bicategory is associative.

@[simp]
theorem CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso {B : Type u} [self : ] {a : B} {b : B} (f : a b) :

The left unitors are given by equalities

@[simp]
theorem CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso {B : Type u} [self : ] {a : B} {b : B} (f : a b) :

The right unitors are given by equalities

@[simp]
theorem CategoryTheory.Bicategory.Strict.associator_eqToIso {B : Type u} [self : ] {a : B} {b : B} {c : B} {d : B} (f : a b) (g : b c) (h : c d) :

The associators are given by equalities

@[instance 100]

Category structure on a strict bicategory

Equations
@[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) :