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.
- 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
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' := _}