mathlib3 documentation


Bicategories #

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

In this file we define typeclass for bicategories.

A bicategory B consists of

We use u, v, and w as the universe variables for objects, 1-morphisms, and 2-morphisms, respectively.

A typeclass for bicategories extends category_theory.category_struct typeclass. This means that we have

For each object a b : B, the collection of 1-morphisms a ⟶ b has a category structure. The 2-morphisms in the bicategory are implemented as the morphisms in this family of categories.

The composition of 1-morphisms is in fact a object part of a functor (a ⟶ b) ⥤ (b ⟶ c) ⥤ (a ⟶ c). The definition of bicategories in this file does not require this functor directly. Instead, it requires the whiskering functions. For a 1-morphism f : a ⟶ b and a 2-morphism η : g ⟶ h between 1-morphisms g h : b ⟶ c, there is a 2-morphism whisker_left f η : f ≫ g ⟶ f ≫ h. Similarly, for a 2-morphism η : f ⟶ g between 1-morphisms f g : a ⟶ b and a 1-morphism f : b ⟶ c, there is a 2-morphism whisker_right η h : f ≫ h ⟶ g ≫ h. These satisfy the exchange law whisker_left f θ ≫ whisker_right η i = whisker_right η h ≫ whisker_left g θ, which is required as an axiom in the definition here.

@[nolint, class]
structure category_theory.bicategory (B : Type u) :
Type (max u (v+1) (w+1))

In a bicategory, we can compose the 1-morphisms f : a ⟶ b and g : b ⟶ c to obtain a 1-morphism f ≫ g : a ⟶ c. This composition does not need to be strictly associative, but there is a specified associator, α_ f g h : (f ≫ g) ≫ h ≅ f ≫ (g ≫ h). There is an identity 1-morphism 𝟙 a : a ⟶ a, with specified left and right unitor isomorphisms λ_ f : 𝟙 a ≫ f ≅ f and ρ_ f : f ≫ 𝟙 a ≅ f. These associators and unitors satisfy the pentagon and triangle equations.


Instances of this typeclass
Instances of other typeclasses for category_theory.bicategory
  • category_theory.bicategory.has_sizeof_inst

Simp-normal form for 2-morphisms #

Rewriting involving associators and unitors could be very complicated. We try to ease this complexity by putting carefully chosen simp lemmas that rewrite any 2-morphisms into simp-normal form defined below. Rewriting into simp-normal form is also useful when applying (forthcoming) coherence tactic.

The simp-normal form of 2-morphisms is defined to be an expression that has the minimal number of parentheses. More precisely,

  1. it is a composition of 2-morphisms like η₁ ≫ η₂ ≫ η₃ ≫ η₄ ≫ η₅ such that each ηᵢ is either a structural 2-morphisms (2-morphisms made up only of identities, associators, unitors) or non-structural 2-morphisms, and
  2. each non-structural 2-morphism in the composition is of the form f₁ ◁ f₂ ◁ f₃ ◁ η ▷ f₄ ▷ f₅, where each fᵢ is a 1-morphism that is not the identity or a composite and η is a non-structural 2-morphisms that is also not the identity or a composite.

Note that f₁ ◁ f₂ ◁ f₃ ◁ η ▷ f₄ ▷ f₅ is actually f₁ ◁ (f₂ ◁ (f₃ ◁ ((η ▷ f₄) ▷ f₅))).

theorem category_theory.bicategory.whisker_left_comp_assoc {B : Type u} [self : category_theory.bicategory B] {a b c : B} (f : a b) {g h i : b c} (η : g h) (θ : h i) {X' : a c} (f' : f i X') :
def category_theory.bicategory.whisker_left_iso {B : Type u} [category_theory.bicategory B] {a b c : B} (f : a b) {g h : b c} (η : g h) :
f g f h

The left whiskering of a 2-isomorphism is a 2-isomorphism.

def category_theory.bicategory.whisker_right_iso {B : Type u} [category_theory.bicategory B] {a b c : B} {f g : a b} (η : f g) (h : b c) :
f h g h

The right whiskering of a 2-isomorphism is a 2-isomorphism.


We state it as a simp lemma, which is regarded as an involved version of id_whisker_right f g : 𝟙 f ▷ g = 𝟙 (f ≫ g).