HepLean Documentation

Mathlib.CategoryTheory.Bicategory.Strict

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.

source
class CategoryTheory.Bicategory.Strict (B : Type u) [CategoryTheory.Bicategory B] :
Prop

A bicategory is called Strict if the left unitors, the right unitors, and the associators are isomorphisms given by equalities.

Instances
    source
    theorem CategoryTheory.Bicategory.Strict.id_comp {B : Type u} :
    ∀ {inst : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f = f

    Identity morphisms are left identities for composition.

    source
    theorem CategoryTheory.Bicategory.Strict.comp_id {B : Type u} :
    ∀ {inst : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b : B} (f : a ⟶ b), CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b) = f

    Identity morphisms are right identities for composition.

    source
    theorem CategoryTheory.Bicategory.Strict.assoc {B : Type u} :
    ∀ {inst : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h)

    Composition in a bicategory is associative.

    source
    theorem CategoryTheory.Bicategory.Strict.leftUnitor_eqToIso {B : Type u} :
    ∀ {inst : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b : B} (f : a ⟶ b), CategoryTheory.Bicategory.leftUnitor f = CategoryTheory.eqToIso ⋯

    The left unitors are given by equalities

    source
    theorem CategoryTheory.Bicategory.Strict.rightUnitor_eqToIso {B : Type u} :
    ∀ {inst : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b : B} (f : a ⟶ b), CategoryTheory.Bicategory.rightUnitor f = CategoryTheory.eqToIso ⋯

    The right unitors are given by equalities

    source
    theorem CategoryTheory.Bicategory.Strict.associator_eqToIso {B : Type u} :
    ∀ {inst : CategoryTheory.Bicategory B} [self : CategoryTheory.Bicategory.Strict B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d), CategoryTheory.Bicategory.associator f g h = CategoryTheory.eqToIso ⋯

    The associators are given by equalities

    source
    @[instance 100]
    instance CategoryTheory.StrictBicategory.category (B : Type u) [CategoryTheory.Bicategory B] [CategoryTheory.Bicategory.Strict B] :
    CategoryTheory.Category.{v, u} B

    Category structure on a strict bicategory

    Equations
    source
    @[simp]
    theorem CategoryTheory.Bicategory.whiskerLeft_eqToHom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) {g : b ⟶ c} {h : b ⟶ c} (η : g = h) :
    CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.eqToHom η) = CategoryTheory.eqToHom ⋯
    source
    @[simp]
    theorem CategoryTheory.Bicategory.eqToHom_whiskerRight {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ b} (η : f = g) (h : b ⟶ c) :
    CategoryTheory.Bicategory.whiskerRight (CategoryTheory.eqToHom η) h = CategoryTheory.eqToHom ⋯