# mathlib3documentation

category_theory.bicategory.strict

# Strict bicategories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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]
structure category_theory.bicategory.strict (B : Type u)  :
Prop
• id_comp' : ( {a b : B} (f : a b), 𝟙 a f = f) . "obviously"
• comp_id' : ( {a b : B} (f : a b), f 𝟙 b = f) . "obviously"
• assoc' : ( {a b c d : B} (f : a b) (g : b c) (h : c d), (f g) h = f g h) . "obviously"
• left_unitor_eq_to_iso' : ( {a b : B} (f : a b), . "obviously"
• right_unitor_eq_to_iso' : ( {a b : B} (f : a b), . "obviously"
• associator_eq_to_iso' : ( {a b c d : B} (f : a b) (g : b c) (h : c d), . "obviously"

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.id_comp {B : Type u} [self : category_theory.bicategory.strict B] {a b : B} (f : a b) :
𝟙 a f = f
@[simp]
theorem category_theory.bicategory.strict.comp_id {B : Type u} [self : category_theory.bicategory.strict B] {a b : B} (f : a b) :
f 𝟙 b = f
@[simp]
theorem category_theory.bicategory.strict.assoc {B : Type u} [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
@[simp]
theorem category_theory.bicategory.strict.associator_eq_to_iso {B : Type u} [self : category_theory.bicategory.strict B] {a b c d : B} (f : a b) (g : b c) (h : c d) :
@[protected, instance]

Category structure on a strict bicategory

Equations
@[simp]
theorem category_theory.bicategory.whisker_left_eq_to_hom {B : Type u} {a b c : B} (f : a b) {g h : b c} (η : g = h) :
@[simp]
theorem category_theory.bicategory.eq_to_hom_whisker_right {B : Type u} {a b c : B} {f g : a b} (η : f = g) (h : b c) :