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.

source

@[class]

structure category_theory.bicategory.strict (B : Type u) [category_theory.bicategory B] :

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), category_theory.bicategory.left_unitor f = category_theory.eq_to_iso _) . "obviously"
right_unitor_eq_to_iso' : (∀ {a b : B} (f : a ⟶ b), category_theory.bicategory.right_unitor f = category_theory.eq_to_iso _) . "obviously"
associator_eq_to_iso' : (∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), category_theory.bicategory.associator f g h = category_theory.eq_to_iso _) . "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

source

@[simp]

theorem category_theory.bicategory.strict.id_comp {B : Type u} [category_theory.bicategory B] [self : category_theory.bicategory.strict B] {a b : B} (f : a ⟶ b) :

𝟙 a ≫ f = f

source

@[simp]

theorem category_theory.bicategory.strict.comp_id {B : Type u} [category_theory.bicategory B] [self : category_theory.bicategory.strict B] {a b : B} (f : a ⟶ b) :

f ≫ 𝟙 b = f

source

@[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

source

@[simp]

theorem category_theory.bicategory.strict.left_unitor_eq_to_iso {B : Type u} [category_theory.bicategory B] [self : category_theory.bicategory.strict B] {a b : B} (f : a ⟶ b) :

category_theory.bicategory.left_unitor f = category_theory.eq_to_iso _

source

@[simp]

theorem category_theory.bicategory.strict.right_unitor_eq_to_iso {B : Type u} [category_theory.bicategory B] [self : category_theory.bicategory.strict B] {a b : B} (f : a ⟶ b) :

category_theory.bicategory.right_unitor f = category_theory.eq_to_iso _

source

@[simp]

theorem category_theory.bicategory.strict.associator_eq_to_iso {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) :

category_theory.bicategory.associator f g h = category_theory.eq_to_iso _

source

@[protected, instance]

def category_theory.strict_bicategory.category (B : Type u) [category_theory.bicategory B] [category_theory.bicategory.strict B] :

category_theory.category B

Category structure on a strict bicategory

Equations

category_theory.strict_bicategory.category B = {to_category_struct := category_theory.bicategory.to_category_struct _inst_1, id_comp' := _, comp_id' := _, assoc' := _}

source

@[simp]

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

category_theory.bicategory.whisker_left f (category_theory.eq_to_hom η) = category_theory.eq_to_hom _

source

@[simp]

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

category_theory.bicategory.whisker_right (category_theory.eq_to_hom η) h = category_theory.eq_to_hom _