# mathlibdocumentation

category_theory.bicategory.basic

# Bicategories #

In this file we define typeclass for bicategories.

A bicategory `B` consists of

• objects `a : B`,
• 1-morphisms `f : a ⟶ b` between objects `a b : B`, and
• 2-morphisms `η : f ⟶ g` beween 1-morphisms `f g : a ⟶ b` between objects `a b : B`.

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

• a composition `f ≫ g : a ⟶ c` for each 1-morphisms `f : a ⟶ b` and `g : b ⟶ c`, and
• a identity `𝟙 a : a ⟶ a` for each object `a : B`.

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))
• to_category_struct :
• hom_category : (Π (a b : B), category_theory.category (a b)) . "apply_instance"
• whisker_left : Π {a b c : B} (f : a b) {g h : b c}, (g h)(f g f h)
• whisker_right : Π {a b c : B} {f g : a b}, (f g)Π (h : b c), f h g h
• associator : Π {a b c d : B} (f : a b) (g : b c) (h : c d), (f g) h f g h
• left_unitor : Π {a b : B} (f : a b), 𝟙 a f f
• right_unitor : Π {a b : B} (f : a b), f 𝟙 b f
• whisker_left_id' : (∀ {a b c : B} (f : a b) (g : b c), = 𝟙 (f g)) . "obviously"
• whisker_left_comp' : (∀ {a b c : B} (f : a b) {g h i : b c} (η : g h) (θ : h i), . "obviously"
• id_whisker_left' : (∀ {a b : B} {f g : a b} (η : f g), . "obviously"
• comp_whisker_left' : (∀ {a b c d : B} (f : a b) (g : b c) {h h' : c d} (η : h h'), . "obviously"
• id_whisker_right' : (∀ {a b c : B} (f : a b) (g : b c), = 𝟙 (f g)) . "obviously"
• comp_whisker_right' : (∀ {a b c : B} {f g h : a b} (η : f g) (θ : g h) (i : b c), . "obviously"
• whisker_right_id' : (∀ {a b : B} {f g : a b} (η : f g), . "obviously"
• whisker_right_comp' : (∀ {a b c d : B} {f f' : a b} (η : f f') (g : b c) (h : c d), . "obviously"
• whisker_assoc' : (∀ {a b c d : B} (f : a b) {g g' : b c} (η : g g') (h : c d), . "obviously"
• whisker_exchange' : (∀ {a b c : B} {f g : a b} {h i : b c} (η : f g) (θ : h i), . "obviously"
• pentagon' : (∀ {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e), = i).hom (h i)).hom) . "obviously"
• triangle' : (∀ {a b c : B} (f : a b) (g : b c), . "obviously"

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₅)))`.

@[simp]
theorem category_theory.bicategory.whisker_left_id {B : Type u} [self : category_theory.bicategory B] {a b c : B} (f : a b) (g : b c) :
= 𝟙 (f g)
@[simp]
theorem category_theory.bicategory.whisker_left_comp {B : Type u} [self : category_theory.bicategory B] {a b c : B} (f : a b) {g h i : b c} (η : g h) (θ : h i) :
@[simp]
theorem category_theory.bicategory.id_whisker_left {B : Type u} [self : category_theory.bicategory B] {a b : B} {f g : a b} (η : f g) :
@[simp]
theorem category_theory.bicategory.comp_whisker_left {B : Type u} [self : category_theory.bicategory B] {a b c d : B} (f : a b) (g : b c) {h h' : c d} (η : h h') :
@[simp]
theorem category_theory.bicategory.id_whisker_right {B : Type u} [self : category_theory.bicategory B] {a b c : B} (f : a b) (g : b c) :
= 𝟙 (f g)
@[simp]
theorem category_theory.bicategory.comp_whisker_right {B : Type u} [self : category_theory.bicategory B] {a b c : B} {f g h : a b} (η : f g) (θ : g h) (i : b c) :
@[simp]
theorem category_theory.bicategory.whisker_right_id {B : Type u} [self : category_theory.bicategory B] {a b : B} {f g : a b} (η : f g) :
@[simp]
theorem category_theory.bicategory.whisker_right_comp {B : Type u} [self : category_theory.bicategory B] {a b c d : B} {f f' : a b} (η : f f') (g : b c) (h : c d) :
@[simp]
theorem category_theory.bicategory.whisker_assoc {B : Type u} [self : category_theory.bicategory B] {a b c d : B} (f : a b) {g g' : b c} (η : g g') (h : c d) :
theorem category_theory.bicategory.whisker_exchange {B : Type u} [self : category_theory.bicategory B] {a b c : B} {f g : a b} {h i : b c} (η : f g) (θ : h i) :
@[simp]
theorem category_theory.bicategory.pentagon {B : Type u} [self : category_theory.bicategory B] {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) :
= i).hom (h i)).hom
@[simp]
theorem category_theory.bicategory.triangle {B : Type u} [self : category_theory.bicategory B] {a b c : B} (f : a b) (g : b c) :
@[simp]
theorem category_theory.bicategory.pentagon_assoc {B : Type u} [self : category_theory.bicategory B] {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) {X' : a e} (f' : f g h i X') :
= i).hom (h i)).hom f'
theorem category_theory.bicategory.id_whisker_left_assoc {B : Type u} [self : category_theory.bicategory B] {a b : B} {f g : a b} (η : f g) {X' : a b} (f' : 𝟙 a g X') :
theorem category_theory.bicategory.comp_whisker_left_assoc {B : Type u} [self : category_theory.bicategory B] {a b c d : B} (f : a b) (g : b c) {h h' : c d} (η : h h') {X' : a d} (f' : (f g) h' X') :
theorem category_theory.bicategory.comp_whisker_right_assoc {B : Type u} [self : category_theory.bicategory B] {a b c : B} {f g h : a b} (η : f g) (θ : g h) (i : b c) {X' : a c} (f' : h i X') :
theorem category_theory.bicategory.whisker_right_id_assoc {B : Type u} [self : category_theory.bicategory B] {a b : B} {f g : a b} (η : f g) {X' : a b} (f' : g 𝟙 b X') :
theorem category_theory.bicategory.whisker_right_comp_assoc {B : Type u} [self : category_theory.bicategory B] {a b c d : B} {f f' : a b} (η : f f') (g : b c) (h : c d) {X' : a d} (f'_1 : f' g h X') :
f'_1 =
theorem category_theory.bicategory.whisker_exchange_assoc {B : Type u} [self : category_theory.bicategory B] {a b c : B} {f g : a b} {h i : b c} (η : f g) (θ : h i) {X' : a c} (f' : g i X') :
@[simp]
theorem category_theory.bicategory.triangle_assoc {B : Type u} [self : category_theory.bicategory B] {a b c : B} (f : a b) (g : b c) {X' : a c} (f' : f g X') :
theorem category_theory.bicategory.whisker_assoc_assoc {B : Type u} [self : category_theory.bicategory B] {a b c d : B} (f : a b) {g g' : b c} (η : g g') (h : c d) {X' : a d} (f' : (f g') h X') :
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') :
@[simp]
theorem category_theory.bicategory.hom_inv_whisker_left_assoc {B : Type u} {a b c : B} (f : a b) {g h : b c} (η : g h) {X' : a c} (f' : f g X') :
@[simp]
theorem category_theory.bicategory.hom_inv_whisker_left {B : Type u} {a b c : B} (f : a b) {g h : b c} (η : g h) :
@[simp]
theorem category_theory.bicategory.hom_inv_whisker_right {B : Type u} {a b c : B} {f g : a b} (η : f g) (h : b c) :
@[simp]
theorem category_theory.bicategory.hom_inv_whisker_right_assoc {B : Type u} {a b c : B} {f g : a b} (η : f g) (h : b c) {X' : a c} (f' : f h X') :
@[simp]
theorem category_theory.bicategory.inv_hom_whisker_left_assoc {B : Type u} {a b c : B} (f : a b) {g h : b c} (η : g h) {X' : a c} (f' : f h X') :
@[simp]
theorem category_theory.bicategory.inv_hom_whisker_left {B : Type u} {a b c : B} (f : a b) {g h : b c} (η : g h) :
@[simp]
theorem category_theory.bicategory.inv_hom_whisker_right_assoc {B : Type u} {a b c : B} {f g : a b} (η : f g) (h : b c) {X' : a c} (f' : g h X') :
@[simp]
theorem category_theory.bicategory.inv_hom_whisker_right {B : Type u} {a b c : B} {f g : a b} (η : f g) (h : b c) :
@[simp]
theorem category_theory.bicategory.whisker_left_iso_inv {B : Type u} {a b c : B} (f : a b) {g h : b c} (η : g h) :
@[simp]
theorem category_theory.bicategory.whisker_left_iso_hom {B : Type u} {a b c : B} (f : a b) {g h : b c} (η : g h) :
def category_theory.bicategory.whisker_left_iso {B : Type u} {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.

Equations
@[protected, instance]
def category_theory.bicategory.whisker_left_is_iso {B : Type u} {a b c : B} (f : a b) {g h : b c} (η : g h)  :
@[simp]
theorem category_theory.bicategory.inv_whisker_left {B : Type u} {a b c : B} (f : a b) {g h : b c} (η : g h)  :
def category_theory.bicategory.whisker_right_iso {B : Type u} {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.

Equations
@[simp]
theorem category_theory.bicategory.whisker_right_iso_hom {B : Type u} {a b c : B} {f g : a b} (η : f g) (h : b c) :
@[simp]
theorem category_theory.bicategory.whisker_right_iso_inv {B : Type u} {a b c : B} {f g : a b} (η : f g) (h : b c) :
@[protected, instance]
def category_theory.bicategory.whisker_right_is_iso {B : Type u} {a b c : B} {f g : a b} (η : f g) (h : b c)  :
@[simp]
theorem category_theory.bicategory.inv_whisker_right {B : Type u} {a b c : B} {f g : a b} (η : f g) (h : b c)  :
@[simp]
theorem category_theory.bicategory.pentagon_inv_assoc {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) {X' : a e} (f' : ((f g) h) i X') :
= (h i)).inv i).inv f'
@[simp]
theorem category_theory.bicategory.pentagon_inv {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) :
= (h i)).inv i).inv
@[simp]
theorem category_theory.bicategory.pentagon_inv_inv_hom_hom_inv {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) :
i).inv =
@[simp]
theorem category_theory.bicategory.pentagon_inv_inv_hom_hom_inv_assoc {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) {X' : a e} (f' : (f g) h i X') :
i).inv =
@[simp]
theorem category_theory.bicategory.pentagon_inv_hom_hom_hom_inv_assoc {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) {X' : a e} (f' : f (g h) i X') :
i).inv =
@[simp]
theorem category_theory.bicategory.pentagon_inv_hom_hom_hom_inv {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) :
i).inv =
@[simp]
theorem category_theory.bicategory.pentagon_hom_inv_inv_inv_inv_assoc {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) {X' : a e} (f' : ((f g) h) i X') :
(h i)).inv i).inv f' =
@[simp]
theorem category_theory.bicategory.pentagon_hom_inv_inv_inv_inv {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) :
(h i)).inv i).inv =
@[simp]
theorem category_theory.bicategory.pentagon_hom_hom_inv_hom_hom {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) :
i).hom =
@[simp]
theorem category_theory.bicategory.pentagon_hom_hom_inv_hom_hom_assoc {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) {X' : a e} (f' : f (g h) i X') :
i).hom =
@[simp]
theorem category_theory.bicategory.pentagon_hom_inv_inv_inv_hom_assoc {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) {X' : a e} (f' : (f g h) i X') :
(h i)).hom =
@[simp]
theorem category_theory.bicategory.pentagon_hom_inv_inv_inv_hom {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) :
(h i)).hom =
@[simp]
theorem category_theory.bicategory.pentagon_hom_hom_inv_inv_hom {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) :
i).hom =
@[simp]
theorem category_theory.bicategory.pentagon_hom_hom_inv_inv_hom_assoc {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) {X' : a e} (f' : (f g) h i X') :
i).hom =
@[simp]
theorem category_theory.bicategory.pentagon_inv_hom_hom_hom_hom_assoc {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) {X' : a e} (f' : f g h i X') :
i).hom (h i)).hom f' =
@[simp]
theorem category_theory.bicategory.pentagon_inv_hom_hom_hom_hom {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) :
i).hom (h i)).hom =
@[simp]
theorem category_theory.bicategory.pentagon_inv_inv_hom_inv_inv {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) :
(h i)).inv =
@[simp]
theorem category_theory.bicategory.pentagon_inv_inv_hom_inv_inv_assoc {B : Type u} {a b c d e : B} (f : a b) (g : b c) (h : c d) (i : d e) {X' : a e} (f' : (f g h) i X') :
(h i)).inv =
theorem category_theory.bicategory.triangle_assoc_comp_left {B : Type u} {a b c : B} (f : a b) (g : b c) :
@[simp]
theorem category_theory.bicategory.triangle_assoc_comp_right_assoc {B : Type u} {a b c : B} (f : a b) (g : b c) {X' : a c} (f' : f g X') :
@[simp]
theorem category_theory.bicategory.triangle_assoc_comp_right {B : Type u} {a b c : B} (f : a b) (g : b c) :
@[simp]
theorem category_theory.bicategory.triangle_assoc_comp_right_inv_assoc {B : Type u} {a b c : B} (f : a b) (g : b c) {X' : a c} (f' : f 𝟙 b g X') :
@[simp]
theorem category_theory.bicategory.triangle_assoc_comp_right_inv {B : Type u} {a b c : B} (f : a b) (g : b c) :
@[simp]
theorem category_theory.bicategory.triangle_assoc_comp_left_inv {B : Type u} {a b c : B} (f : a b) (g : b c) :
@[simp]
theorem category_theory.bicategory.triangle_assoc_comp_left_inv_assoc {B : Type u} {a b c : B} (f : a b) (g : b c) {X' : a c} (f' : (f 𝟙 b) g X') :
theorem category_theory.bicategory.associator_naturality_left_assoc {B : Type u} {a b c d : B} {f f' : a b} (η : f f') (g : b c) (h : c d) {X' : a d} (f'_1 : f' g h X') :
= f'_1
theorem category_theory.bicategory.associator_naturality_left {B : Type u} {a b c d : B} {f f' : a b} (η : f f') (g : b c) (h : c d) :
theorem category_theory.bicategory.associator_inv_naturality_left {B : Type u} {a b c d : B} {f f' : a b} (η : f f') (g : b c) (h : c d) :
theorem category_theory.bicategory.associator_inv_naturality_left_assoc {B : Type u} {a b c d : B} {f f' : a b} (η : f f') (g : b c) (h : c d) {X' : a d} (f'_1 : (f' g) h X') :
.inv f'_1 =
theorem category_theory.bicategory.whisker_right_comp_symm {B : Type u} {a b c d : B} {f f' : a b} (η : f f') (g : b c) (h : c d) :
theorem category_theory.bicategory.whisker_right_comp_symm_assoc {B : Type u} {a b c d : B} {f f' : a b} (η : f f') (g : b c) (h : c d) {X' : a d} (f'_1 : (f' g) h X') :
= .inv f'_1
theorem category_theory.bicategory.associator_naturality_middle {B : Type u} {a b c d : B} (f : a b) {g g' : b c} (η : g g') (h : c d) :
theorem category_theory.bicategory.associator_naturality_middle_assoc {B : Type u} {a b c d : B} (f : a b) {g g' : b c} (η : g g') (h : c d) {X' : a d} (f' : f g' h X') :
theorem category_theory.bicategory.associator_inv_naturality_middle_assoc {B : Type u} {a b c d : B} (f : a b) {g g' : b c} (η : g g') (h : c d) {X' : a d} (f' : (f g') h X') :
theorem category_theory.bicategory.associator_inv_naturality_middle {B : Type u} {a b c d : B} (f : a b) {g g' : b c} (η : g g') (h : c d) :
theorem category_theory.bicategory.whisker_assoc_symm {B : Type u} {a b c d : B} (f : a b) {g g' : b c} (η : g g') (h : c d) :
theorem category_theory.bicategory.whisker_assoc_symm_assoc {B : Type u} {a b c d : B} (f : a b) {g g' : b c} (η : g g') (h : c d) {X' : a d} (f' : f g' h X') :
theorem category_theory.bicategory.associator_naturality_right {B : Type u} {a b c d : B} (f : a b) (g : b c) {h h' : c d} (η : h h') :
theorem category_theory.bicategory.associator_naturality_right_assoc {B : Type u} {a b c d : B} (f : a b) (g : b c) {h h' : c d} (η : h h') {X' : a d} (f' : f g h' X') :
theorem category_theory.bicategory.associator_inv_naturality_right {B : Type u} {a b c d : B} (f : a b) (g : b c) {h h' : c d} (η : h h') :
theorem category_theory.bicategory.associator_inv_naturality_right_assoc {B : Type u} {a b c d : B} (f : a b) (g : b c) {h h' : c d} (η : h h') {X' : a d} (f' : (f g) h' X') :
theorem category_theory.bicategory.comp_whisker_left_symm_assoc {B : Type u} {a b c d : B} (f : a b) (g : b c) {h h' : c d} (η : h h') {X' : a d} (f' : f g h' X') :
theorem category_theory.bicategory.comp_whisker_left_symm {B : Type u} {a b c d : B} (f : a b) (g : b c) {h h' : c d} (η : h h') :
theorem category_theory.bicategory.left_unitor_naturality_assoc {B : Type u} {a b : B} {f g : a b} (η : f g) {X' : a b} (f' : g X') :
theorem category_theory.bicategory.left_unitor_naturality {B : Type u} {a b : B} {f g : a b} (η : f g) :
theorem category_theory.bicategory.left_unitor_inv_naturality_assoc {B : Type u} {a b : B} {f g : a b} (η : f g) {X' : a b} (f' : 𝟙 a g X') :
theorem category_theory.bicategory.left_unitor_inv_naturality {B : Type u} {a b : B} {f g : a b} (η : f g) :
theorem category_theory.bicategory.id_whisker_left_symm {B : Type u} {a b : B} {f g : a b} (η : f g) :
theorem category_theory.bicategory.right_unitor_naturality_assoc {B : Type u} {a b : B} {f g : a b} (η : f g) {X' : a b} (f' : g X') :
theorem category_theory.bicategory.right_unitor_naturality {B : Type u} {a b : B} {f g : a b} (η : f g) :
theorem category_theory.bicategory.right_unitor_inv_naturality {B : Type u} {a b : B} {f g : a b} (η : f g) :
theorem category_theory.bicategory.right_unitor_inv_naturality_assoc {B : Type u} {a b : B} {f g : a b} (η : f g) {X' : a b} (f' : g 𝟙 b X') :
theorem category_theory.bicategory.whisker_right_id_symm {B : Type u} {a b : B} {f g : a b} (η : f g) :
theorem category_theory.bicategory.whisker_left_iff {B : Type u} {a b : B} {f g : a b} (η θ : f g) :
theorem category_theory.bicategory.whisker_right_iff {B : Type u} {a b : B} {f g : a b} (η θ : f g) :
theorem category_theory.bicategory.left_unitor_whisker_right_assoc {B : Type u} {a b c : B} (f : a b) (g : b c) {X' : a c} (f' : f g X') :
@[simp]
theorem category_theory.bicategory.left_unitor_whisker_right {B : Type u} {a b c : B} (f : a b) (g : b c) :

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

theorem category_theory.bicategory.left_unitor_inv_whisker_right_assoc {B : Type u} {a b c : B} (f : a b) (g : b c) {X' : a c} (f' : (𝟙 a f) g X') :
@[simp]
theorem category_theory.bicategory.left_unitor_inv_whisker_right {B : Type u} {a b c : B} (f : a b) (g : b c) :
theorem category_theory.bicategory.whisker_left_right_unitor_assoc {B : Type u} {a b c : B} (f : a b) (g : b c) {X' : a c} (f' : f g X') :
@[simp]
theorem category_theory.bicategory.whisker_left_right_unitor {B : Type u} {a b c : B} (f : a b) (g : b c) :
@[simp]
theorem category_theory.bicategory.whisker_left_right_unitor_inv {B : Type u} {a b c : B} (f : a b) (g : b c) :
theorem category_theory.bicategory.whisker_left_right_unitor_inv_assoc {B : Type u} {a b c : B} (f : a b) (g : b c) {X' : a c} (f' : f g 𝟙 c X') :
theorem category_theory.bicategory.left_unitor_comp_assoc {B : Type u} {a b c : B} (f : a b) (g : b c) {X' : a c} (f' : f g X') :
theorem category_theory.bicategory.left_unitor_comp {B : Type u} {a b c : B} (f : a b) (g : b c) :
theorem category_theory.bicategory.left_unitor_comp_inv_assoc {B : Type u} {a b c : B} (f : a b) (g : b c) {X' : a c} (f' : 𝟙 a f g X') :
theorem category_theory.bicategory.left_unitor_comp_inv {B : Type u} {a b c : B} (f : a b) (g : b c) :
theorem category_theory.bicategory.right_unitor_comp_assoc {B : Type u} {a b c : B} (f : a b) (g : b c) {X' : a c} (f' : f g X') :
theorem category_theory.bicategory.right_unitor_comp {B : Type u} {a b c : B} (f : a b) (g : b c) :
theorem category_theory.bicategory.right_unitor_comp_inv_assoc {B : Type u} {a b c : B} (f : a b) (g : b c) {X' : a c} (f' : (f g) 𝟙 c X') :
theorem category_theory.bicategory.right_unitor_comp_inv {B : Type u} {a b c : B} (f : a b) (g : b c) :
@[simp]
theorem category_theory.bicategory.unitors_equal {B : Type u} {a : B} :
@[simp]
theorem category_theory.bicategory.unitors_inv_equal {B : Type u} {a : B} :