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.
@[class]
- 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
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[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) :
@[protected, instance]
def
category_theory.strict_bicategory.category
(B : Type u)
[category_theory.bicategory B]
[category_theory.bicategory.strict 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' := _}
@[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) :
@[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) :