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 between 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 CategoryTheory.CategoryStruct typeclass. This means that we have

• a composition f ≫ g : a ⟶ c for each 1-morphisms f : a ⟶ b and g : b ⟶ c, and
• an 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 an 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 whiskerLeft 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 whiskerRight η h : f ≫ h ⟶ g ≫ h. These satisfy the exchange law whiskerLeft f θ ≫ whiskerRight η i = whiskerRight η h ≫ whiskerLeft g θ, which is required as an axiom in the definition here.

class CategoryTheory.Bicategory (B : Type u) extends CategoryTheory.CategoryStruct , Quiver : Type (max (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.

See https://ncatlab.org/nlab/show/bicategory.

• Hom : B → B → Type v
• id : (X : B) → X ⟶ X
• comp : {X Y Z : B} → (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z)
• homCategory : (a b : B) → CategoryTheory.Category.{w, v} (a ⟶ b)
• whiskerLeft : {a b c : B} → (f : a ⟶ b) → {g h : b ⟶ c} → (g ⟶ h) → (CategoryTheory.CategoryStruct.comp f g ⟶ CategoryTheory.CategoryStruct.comp f h)
• whiskerRight : {a b c : B} → {f g : a ⟶ b} → (f ⟶ g) → (h : b ⟶ c) → CategoryTheory.CategoryStruct.comp f h ⟶ CategoryTheory.CategoryStruct.comp g h
• associator : {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)
• leftUnitor : {a b : B} → (f : a ⟶ b) → CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f ≅ f
• rightUnitor : {a b : B} → (f : a ⟶ b) → CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b) ≅ f
• whiskerLeft_id : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.CategoryStruct.id g) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
• whiskerLeft_comp : ∀ {a b c : B} (f : a ⟶ b) {g h i : b ⟶ c} (η : g ⟶ h) (θ : h ⟶ i), CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η) (CategoryTheory.Bicategory.whiskerLeft f θ)
• id_whiskerLeft : ∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.leftUnitor g).inv)
• comp_whiskerLeft : ∀ {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h h' : c ⟶ d} (η : h ⟶ h'), CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η)) (CategoryTheory.Bicategory.associator f g h').inv)
• id_whiskerRight : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.id f) g = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)
• comp_whiskerRight : ∀ {a b c : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) (i : b ⟶ c), CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.comp η θ) i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η i) (CategoryTheory.Bicategory.whiskerRight θ i)
• whiskerRight_id : ∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g), CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.rightUnitor g).inv)
• whiskerRight_comp : ∀ {a b c d : B} {f f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d), CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h) (CategoryTheory.Bicategory.associator f' g h).hom)
• whisker_assoc : ∀ {a b c d : B} (f : a ⟶ b) {g g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d), CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h)) (CategoryTheory.Bicategory.associator f g' h).inv)
• whisker_exchange : ∀ {a b c : B} {f g : a ⟶ b} {h i : b ⟶ c} (η : f ⟶ g) (θ : h ⟶ i), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f θ) (CategoryTheory.Bicategory.whiskerRight η i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η h) (CategoryTheory.Bicategory.whiskerLeft g θ)
• pentagon : ∀ {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom
• triangle : ∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom) = CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g

@[simp]

theorem CategoryTheory.Bicategory.whiskerLeft_id {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.CategoryStruct.id g) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.Bicategory.whiskerLeft_comp {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) {g : b ⟶ c} {h : b ⟶ c} {i : b ⟶ c} (η : g ⟶ h) (θ : h ⟶ i) : CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.CategoryStruct.comp η θ) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η) (CategoryTheory.Bicategory.whiskerLeft f θ)

@[simp]

theorem CategoryTheory.Bicategory.id_whiskerLeft {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) : CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.leftUnitor g).inv)

@[simp]

theorem CategoryTheory.Bicategory.comp_whiskerLeft {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) {h : c ⟶ d} {h' : c ⟶ d} (η : h ⟶ h') : CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η)) (CategoryTheory.Bicategory.associator f g h').inv)

@[simp]

theorem CategoryTheory.Bicategory.id_whiskerRight {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.id f) g = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.Bicategory.comp_whiskerRight {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h) (i : b ⟶ c) : CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.comp η θ) i = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η i) (CategoryTheory.Bicategory.whiskerRight θ i)

@[simp]

theorem CategoryTheory.Bicategory.whiskerRight_id {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) : CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom (CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.rightUnitor g).inv)

@[simp]

theorem CategoryTheory.Bicategory.whiskerRight_comp {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {f : a ⟶ b} {f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) : CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h) (CategoryTheory.Bicategory.associator f' g h).hom)

@[simp]

theorem CategoryTheory.Bicategory.whisker_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) {g : b ⟶ c} {g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) : CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h)) (CategoryTheory.Bicategory.associator f g' h).inv)

theorem CategoryTheory.Bicategory.whisker_exchange {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ b} {h : b ⟶ c} {i : b ⟶ c} (η : f ⟶ g) (θ : h ⟶ i) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f θ) (CategoryTheory.Bicategory.whiskerRight η i) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η h) (CategoryTheory.Bicategory.whiskerLeft g θ)

@[simp]

theorem CategoryTheory.Bicategory.pentagon {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom

@[simp]

theorem CategoryTheory.Bicategory.triangle {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom) = CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g

def CategoryTheory.Bicategory.«term_◁_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Bicategory.«term_▷_» : Lean.TrailingParserDescr

Equations

• One or more equations did not get rendered due to their size.

def CategoryTheory.Bicategory.termα_ : Lean.ParserDescr

Equations

• CategoryTheory.Bicategory.termα_ = Lean.ParserDescr.node `CategoryTheory.Bicategory.termα_ 1024 (Lean.ParserDescr.symbol "α_")

def CategoryTheory.Bicategory.«termλ_» : Lean.ParserDescr

Equations

• CategoryTheory.Bicategory.«termλ_» = Lean.ParserDescr.node `CategoryTheory.Bicategory.«termλ_» 1024 (Lean.ParserDescr.symbol "λ_")

def CategoryTheory.Bicategory.termρ_ : Lean.ParserDescr

Equations

• CategoryTheory.Bicategory.termρ_ = Lean.ParserDescr.node `CategoryTheory.Bicategory.termρ_ 1024 (Lean.ParserDescr.symbol "ρ_")

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 CategoryTheory.Bicategory.id_whiskerLeft_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) {Z : a ⟶ b} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom (CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor g).inv h))

theorem CategoryTheory.Bicategory.comp_whiskerLeft_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) {h : c ⟶ d} {h' : c ⟶ d} (η : h✝ ⟶ h') {Z : a ⟶ d} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h✝).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h').inv h))

theorem CategoryTheory.Bicategory.whisker_assoc_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) {g : b ⟶ c} {g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) {Z : a ⟶ d} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g') h✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h✝) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h✝).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g' h✝).inv h))

theorem CategoryTheory.Bicategory.whiskerRight_id_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) {Z : a ⟶ b} (h : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom (CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).inv h))

theorem CategoryTheory.Bicategory.whiskerRight_comp_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {f : a ⟶ b} {f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) {Z : a ⟶ d} (h : CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g h✝) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h✝)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h✝).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f' g h✝).hom h))

theorem CategoryTheory.Bicategory.whisker_exchange_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ b} {h : b ⟶ c} {i : b ⟶ c} (η : f ⟶ g) (θ : h✝ ⟶ i) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp g i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f θ) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η i) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft g θ) h)

theorem CategoryTheory.Bicategory.comp_whiskerRight_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ b} {h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h✝) (i : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp h✝ i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.CategoryStruct.comp η θ) i) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight θ i) h)

theorem CategoryTheory.Bicategory.whiskerLeft_comp_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) {g : b ⟶ c} {h : b ⟶ c} {i : b ⟶ c} (η : g ⟶ h✝) (θ : h✝ ⟶ i) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.CategoryStruct.comp η θ)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f θ) h)

@[simp]

theorem CategoryTheory.Bicategory.pentagon_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) {Z : a ⟶ e} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h✝ i)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h✝).hom i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h✝) i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h✝ i).hom) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h✝ i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h✝ i)).hom h)

@[simp]

theorem CategoryTheory.Bicategory.triangle_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g) h

@[simp]

theorem CategoryTheory.Bicategory.whiskerLeft_hom_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) {g : b ⟶ c} {h : b ⟶ c} (η : g ≅ h) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.hom) (CategoryTheory.Bicategory.whiskerLeft f η.inv) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f g)

@[simp]

theorem CategoryTheory.Bicategory.whiskerLeft_hom_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) {g : b ⟶ c} {h : b ⟶ c} (η : g ≅ h✝) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.inv) h) = h

@[simp]

theorem CategoryTheory.Bicategory.hom_inv_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.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.hom h) (CategoryTheory.Bicategory.whiskerRight η.inv h) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.Bicategory.hom_inv_whiskerRight_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f h✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.hom h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.inv h✝) h) = h

@[simp]

theorem CategoryTheory.Bicategory.whiskerLeft_inv_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) {g : b ⟶ c} {h : b ⟶ c} (η : g ≅ h) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.inv) (CategoryTheory.Bicategory.whiskerLeft f η.hom) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.Bicategory.whiskerLeft_inv_hom_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) {g : b ⟶ c} {h : b ⟶ c} (η : g ≅ h✝) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f h✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f η.hom) h) = h

@[simp]

theorem CategoryTheory.Bicategory.inv_hom_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.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.inv h) (CategoryTheory.Bicategory.whiskerRight η.hom h) = CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.comp g h)

@[simp]

theorem CategoryTheory.Bicategory.inv_hom_whiskerRight_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp g h✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.inv h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η.hom h✝) h) = h

def CategoryTheory.Bicategory.whiskerLeftIso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) {g : b ⟶ c} {h : b ⟶ c} (η : g ≅ h) : CategoryTheory.CategoryStruct.comp f g ≅ CategoryTheory.CategoryStruct.comp f h

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

Equations

• CategoryTheory.Bicategory.whiskerLeftIso f η = { hom := CategoryTheory.Bicategory.whiskerLeft f η.hom, inv := CategoryTheory.Bicategory.whiskerLeft f η.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.Bicategory.whiskerLeftIso_inv {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.whiskerLeftIso f η).inv = CategoryTheory.Bicategory.whiskerLeft f η.inv

@[simp]

theorem CategoryTheory.Bicategory.whiskerLeftIso_hom {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.whiskerLeftIso f η).hom = CategoryTheory.Bicategory.whiskerLeft f η.hom

instance CategoryTheory.Bicategory.whiskerLeft_isIso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) {g : b ⟶ c} {h : b ⟶ c} (η : g ⟶ h) [CategoryTheory.IsIso η] : CategoryTheory.IsIso (CategoryTheory.Bicategory.whiskerLeft f η)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Bicategory.inv_whiskerLeft {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) {g : b ⟶ c} {h : b ⟶ c} (η : g ⟶ h) [CategoryTheory.IsIso η] : CategoryTheory.inv (CategoryTheory.Bicategory.whiskerLeft f η) = CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.inv η)

def CategoryTheory.Bicategory.whiskerRightIso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) : CategoryTheory.CategoryStruct.comp f h ≅ CategoryTheory.CategoryStruct.comp g h

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

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Bicategory.whiskerRightIso_hom {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.whiskerRightIso η h).hom = CategoryTheory.Bicategory.whiskerRight η.hom h

@[simp]

theorem CategoryTheory.Bicategory.whiskerRightIso_inv {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.whiskerRightIso η h).inv = CategoryTheory.Bicategory.whiskerRight η.inv h

instance CategoryTheory.Bicategory.whiskerRight_isIso {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) [CategoryTheory.IsIso η] : CategoryTheory.IsIso (CategoryTheory.Bicategory.whiskerRight η h)

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Bicategory.inv_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.IsIso η] : CategoryTheory.inv (CategoryTheory.Bicategory.whiskerRight η h) = CategoryTheory.Bicategory.whiskerRight (CategoryTheory.inv η) h

@[simp]

theorem CategoryTheory.Bicategory.pentagon_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv

@[simp]

theorem CategoryTheory.Bicategory.pentagon_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) {Z : a ⟶ e} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h✝) i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h✝ i).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h✝) i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h✝).inv i) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h✝ i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h✝ i).inv h)

@[simp]

theorem CategoryTheory.Bicategory.pentagon_inv_inv_hom_hom_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i) (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom) (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv

@[simp]

theorem CategoryTheory.Bicategory.pentagon_inv_inv_hom_hom_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) {Z : a ⟶ e} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp h✝ i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h✝) i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h✝).inv i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h✝ i).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h✝ i).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h✝ i)).inv h)

@[simp]

theorem CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i) (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv)

@[simp]

theorem CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) {Z : a ⟶ e} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g h✝) i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h✝ i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h✝).hom i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h✝) i).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h✝ i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h✝ i).inv) h)

@[simp]

theorem CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i)

@[simp]

theorem CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) {Z : a ⟶ e} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h✝) i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h✝ i).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h✝ i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h✝ i).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h✝) i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h✝).inv i) h)

@[simp]

theorem CategoryTheory.Bicategory.pentagon_hom_hom_inv_hom_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i) (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom

@[simp]

theorem CategoryTheory.Bicategory.pentagon_hom_hom_inv_hom_hom_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) {Z : a ⟶ e} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp g h✝) i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h✝ i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h✝ i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h✝ i).inv) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h✝).hom i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h✝) i).hom h)

@[simp]

theorem CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv) (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i)

@[simp]

theorem CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_hom_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) {Z : a ⟶ e} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h✝)) i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h✝ i)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h✝ i).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h✝) i).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h✝ i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h✝).hom i) h)

@[simp]

theorem CategoryTheory.Bicategory.pentagon_hom_hom_inv_inv_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom) (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i) (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom

@[simp]

theorem CategoryTheory.Bicategory.pentagon_hom_hom_inv_inv_hom_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) {Z : a ⟶ e} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp h✝ i) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h✝) i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h✝ i).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h✝ i)).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h✝).inv i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h✝ i).hom h)

@[simp]

theorem CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_hom {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).hom (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).hom)

@[simp]

theorem CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_hom_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) {Z : a ⟶ e} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp h✝ i)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h✝).inv i) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h✝ i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h✝ i)).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h✝) i).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h✝ i).hom) h)

@[simp]

theorem CategoryTheory.Bicategory.pentagon_inv_inv_hom_inv_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).hom i)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv) (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv

@[simp]

theorem CategoryTheory.Bicategory.pentagon_inv_inv_hom_inv_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e) {Z : a ⟶ e} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h✝)) i ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h✝ i)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h✝ i).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h✝).hom i) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h✝ i).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h✝) i).inv h)

theorem CategoryTheory.Bicategory.triangle_assoc_comp_left {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom) = CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g

@[simp]

theorem CategoryTheory.Bicategory.triangle_assoc_comp_right {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g) = CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom

@[simp]

theorem CategoryTheory.Bicategory.triangle_assoc_comp_right_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).hom g) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).hom) h

@[simp]

theorem CategoryTheory.Bicategory.triangle_assoc_comp_right_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).inv g) (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom = CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).inv

@[simp]

theorem CategoryTheory.Bicategory.triangle_assoc_comp_right_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id b) g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).inv g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).inv) h

@[simp]

theorem CategoryTheory.Bicategory.triangle_assoc_comp_left_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).inv) (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).inv = CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).inv g

@[simp]

theorem CategoryTheory.Bicategory.triangle_assoc_comp_left_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id b)) g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor g).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.id b) g).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.rightUnitor f).inv g) h

theorem CategoryTheory.Bicategory.associator_naturality_left {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {f : a ⟶ b} {f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h) (CategoryTheory.Bicategory.associator f' g h).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h))

theorem CategoryTheory.Bicategory.associator_naturality_left_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {f : a ⟶ b} {f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) {Z : a ⟶ d} (h : CategoryTheory.CategoryStruct.comp f' (CategoryTheory.CategoryStruct.comp g h✝) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f' g h✝).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h✝).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h✝)) h)

theorem CategoryTheory.Bicategory.associator_inv_naturality_left {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {f : a ⟶ b} {f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.associator f' g h).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h)

theorem CategoryTheory.Bicategory.associator_inv_naturality_left_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {f : a ⟶ b} {f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) {Z : a ⟶ d} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f' g) h✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f' g h✝).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h✝).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h✝) h)

theorem CategoryTheory.Bicategory.whiskerRight_comp_symm {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {f : a ⟶ b} {f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) : CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h)) (CategoryTheory.Bicategory.associator f' g h).inv)

theorem CategoryTheory.Bicategory.whiskerRight_comp_symm_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} {f : a ⟶ b} {f' : a ⟶ b} (η : f ⟶ f') (g : b ⟶ c) (h : c ⟶ d) {Z : a ⟶ d} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f' g) h✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η g) h✝) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h✝).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.comp g h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f' g h✝).inv h))

theorem CategoryTheory.Bicategory.associator_naturality_middle {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) {g : b ⟶ c} {g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h) (CategoryTheory.Bicategory.associator f g' h).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h))

theorem CategoryTheory.Bicategory.associator_naturality_middle_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) {g : b ⟶ c} {g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) {Z : a ⟶ d} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g' h✝) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g' h✝).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h✝).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h✝)) h)

theorem CategoryTheory.Bicategory.associator_inv_naturality_middle {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) {g : b ⟶ c} {g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h)) (CategoryTheory.Bicategory.associator f g' h).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h)

theorem CategoryTheory.Bicategory.associator_inv_naturality_middle_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) {g : b ⟶ c} {g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) {Z : a ⟶ d} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g') h✝ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h✝)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g' h✝).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h✝).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h✝) h)

theorem CategoryTheory.Bicategory.whisker_assoc_symm {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) {g : b ⟶ c} {g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) : CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h) (CategoryTheory.Bicategory.associator f g' h).hom)

theorem CategoryTheory.Bicategory.whisker_assoc_symm_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) {g : b ⟶ c} {g' : b ⟶ c} (η : g ⟶ g') (h : c ⟶ d) {Z : a ⟶ d} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g' h✝) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight η h✝)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h✝).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerLeft f η) h✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g' h✝).hom h))

theorem CategoryTheory.Bicategory.associator_naturality_right {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) {h : c ⟶ d} {h' : c ⟶ d} (η : h ⟶ h') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η) (CategoryTheory.Bicategory.associator f g h').hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η))

theorem CategoryTheory.Bicategory.associator_naturality_right_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) {h : c ⟶ d} {h' : c ⟶ d} (η : h✝ ⟶ h') {Z : a ⟶ d} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h').hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h✝).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η)) h)

theorem CategoryTheory.Bicategory.associator_inv_naturality_right {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) {h : c ⟶ d} {h' : c ⟶ d} (η : h ⟶ h') : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η)) (CategoryTheory.Bicategory.associator f g h').inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η)

theorem CategoryTheory.Bicategory.associator_inv_naturality_right_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) {h : c ⟶ d} {h' : c ⟶ d} (η : h✝ ⟶ h') {Z : a ⟶ d} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h').inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h✝).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η) h)

theorem CategoryTheory.Bicategory.comp_whiskerLeft_symm {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) {h : c ⟶ d} {h' : c ⟶ d} (η : h ⟶ h') : CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η) (CategoryTheory.Bicategory.associator f g h').hom)

theorem CategoryTheory.Bicategory.comp_whiskerLeft_symm_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (g : b ⟶ c) {h : c ⟶ d} {h' : c ⟶ d} (η : h✝ ⟶ h') {Z : a ⟶ d} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g h') ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft g η)) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h✝).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.comp f g) η) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g h').hom h))

theorem CategoryTheory.Bicategory.leftUnitor_naturality {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η) (CategoryTheory.Bicategory.leftUnitor g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom η

theorem CategoryTheory.Bicategory.leftUnitor_naturality_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) {Z : a ⟶ b} (h : g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor g).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom (CategoryTheory.CategoryStruct.comp η h)

theorem CategoryTheory.Bicategory.leftUnitor_inv_naturality {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) : CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.leftUnitor g).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).inv (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η)

theorem CategoryTheory.Bicategory.leftUnitor_inv_naturality_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) {Z : a ⟶ b} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) g ⟶ Z) : CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor g).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η) h)

theorem CategoryTheory.Bicategory.id_whiskerLeft_symm {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) : η = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η) (CategoryTheory.Bicategory.leftUnitor g).hom)

theorem CategoryTheory.Bicategory.rightUnitor_naturality {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.Bicategory.rightUnitor g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom η

theorem CategoryTheory.Bicategory.rightUnitor_naturality_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) {Z : a ⟶ b} (h : g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).hom (CategoryTheory.CategoryStruct.comp η h)

theorem CategoryTheory.Bicategory.rightUnitor_inv_naturality {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) : CategoryTheory.CategoryStruct.comp η (CategoryTheory.Bicategory.rightUnitor g).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).inv (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b))

theorem CategoryTheory.Bicategory.rightUnitor_inv_naturality_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) {Z : a ⟶ b} (h : CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id b) ⟶ Z) : CategoryTheory.CategoryStruct.comp η (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor g).inv h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b)) h)

theorem CategoryTheory.Bicategory.whiskerRight_id_symm {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) : η = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor f).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b)) (CategoryTheory.Bicategory.rightUnitor g).hom)

theorem CategoryTheory.Bicategory.whiskerLeft_iff {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) (θ : f ⟶ g) : CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η = CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) θ ↔ η = θ

theorem CategoryTheory.Bicategory.whiskerRight_iff {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {f : a ⟶ b} {g : a ⟶ b} (η : f ⟶ g) (θ : f ⟶ g) : CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b) = CategoryTheory.Bicategory.whiskerRight θ (CategoryTheory.CategoryStruct.id b) ↔ η = θ

@[simp]

theorem CategoryTheory.Bicategory.leftUnitor_whiskerRight {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).hom g = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).hom (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).hom

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

theorem CategoryTheory.Bicategory.leftUnitor_whiskerRight_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).hom g) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).hom h)

@[simp]

theorem CategoryTheory.Bicategory.leftUnitor_inv_whiskerRight {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).inv g = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).inv (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).inv

theorem CategoryTheory.Bicategory.leftUnitor_inv_whiskerRight_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) f) g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).inv g) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).inv h)

@[simp]

theorem CategoryTheory.Bicategory.whiskerLeft_rightUnitor {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).inv (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).hom

theorem CategoryTheory.Bicategory.whiskerLeft_rightUnitor_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).hom h)

@[simp]

theorem CategoryTheory.Bicategory.whiskerLeft_rightUnitor_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).inv (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).hom

theorem CategoryTheory.Bicategory.whiskerLeft_rightUnitor_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.id c)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).inv) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).hom h)

theorem CategoryTheory.Bicategory.leftUnitor_comp {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).inv (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).hom g)

theorem CategoryTheory.Bicategory.leftUnitor_comp_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).hom g) h)

theorem CategoryTheory.Bicategory.leftUnitor_comp_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).inv g) (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).hom

theorem CategoryTheory.Bicategory.leftUnitor_comp_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id a) (CategoryTheory.CategoryStruct.comp f g) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.comp f g)).inv h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.leftUnitor f).inv g) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.id a) f g).hom h)

theorem CategoryTheory.Bicategory.rightUnitor_comp {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).hom (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).hom)

theorem CategoryTheory.Bicategory.rightUnitor_comp_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp f g ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).hom) h)

theorem CategoryTheory.Bicategory.rightUnitor_comp_inv {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) : (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).inv) (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).inv

theorem CategoryTheory.Bicategory.rightUnitor_comp_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c} (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.id c) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.comp f g)).inv h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor g).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.id c)).inv h)

@[simp]

theorem CategoryTheory.Bicategory.unitors_equal {B : Type u} [CategoryTheory.Bicategory B] {a : B} : (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.id a)).hom = (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id a)).hom

@[simp]

theorem CategoryTheory.Bicategory.unitors_inv_equal {B : Type u} [CategoryTheory.Bicategory B] {a : B} : (CategoryTheory.Bicategory.leftUnitor (CategoryTheory.CategoryStruct.id a)).inv = (CategoryTheory.Bicategory.rightUnitor (CategoryTheory.CategoryStruct.id a)).inv

def CategoryTheory.Bicategory.precomp {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (c : B) (f : a ⟶ b) : CategoryTheory.Functor (b ⟶ c) (a ⟶ c)

Precomposition of a 1-morphism as a functor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Bicategory.precomp_map {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (c : B) (f : a ⟶ b) : ∀ {X Y : b ⟶ c} (x : X ⟶ Y), (CategoryTheory.Bicategory.precomp c f).map x = CategoryTheory.Bicategory.whiskerLeft f x

@[simp]

theorem CategoryTheory.Bicategory.precomp_obj {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} (c : B) (f : a ⟶ b) : ∀ (x : b ⟶ c), (CategoryTheory.Bicategory.precomp c f).obj x = CategoryTheory.CategoryStruct.comp f x

def CategoryTheory.Bicategory.precomposing {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) (c : B) : CategoryTheory.Functor (a ⟶ b) (CategoryTheory.Functor (b ⟶ c) (a ⟶ c))

Precomposition of a 1-morphism as a functor from the category of 1-morphisms a ⟶ b into the category of functors (b ⟶ c) ⥤ (a ⟶ c).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Bicategory.precomposing_obj {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) (c : B) (f : a ⟶ b) : (CategoryTheory.Bicategory.precomposing a b c).obj f = CategoryTheory.Bicategory.precomp c f

@[simp]

theorem CategoryTheory.Bicategory.precomposing_map_app {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) (c : B) : ∀ {X Y : a ⟶ b} (η : X ⟶ Y) (x : b ⟶ c), ((CategoryTheory.Bicategory.precomposing a b c).map η).app x = CategoryTheory.Bicategory.whiskerRight η x

def CategoryTheory.Bicategory.postcomp {B : Type u} [CategoryTheory.Bicategory B] {b : B} {c : B} (a : B) (f : b ⟶ c) : CategoryTheory.Functor (a ⟶ b) (a ⟶ c)

Postcomposition of a 1-morphism as a functor.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Bicategory.postcomp_obj {B : Type u} [CategoryTheory.Bicategory B] {b : B} {c : B} (a : B) (f : b ⟶ c) : ∀ (x : a ⟶ b), (CategoryTheory.Bicategory.postcomp a f).obj x = CategoryTheory.CategoryStruct.comp x f

@[simp]

theorem CategoryTheory.Bicategory.postcomp_map {B : Type u} [CategoryTheory.Bicategory B] {b : B} {c : B} (a : B) (f : b ⟶ c) : ∀ {X Y : a ⟶ b} (x : X ⟶ Y), (CategoryTheory.Bicategory.postcomp a f).map x = CategoryTheory.Bicategory.whiskerRight x f

def CategoryTheory.Bicategory.postcomposing {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) (c : B) : CategoryTheory.Functor (b ⟶ c) (CategoryTheory.Functor (a ⟶ b) (a ⟶ c))

Postcomposition of a 1-morphism as a functor from the category of 1-morphisms b ⟶ c into the category of functors (a ⟶ b) ⥤ (a ⟶ c).

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem CategoryTheory.Bicategory.postcomposing_map_app {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) (c : B) : ∀ {X Y : b ⟶ c} (η : X ⟶ Y) (x : a ⟶ b), ((CategoryTheory.Bicategory.postcomposing a b c).map η).app x = CategoryTheory.Bicategory.whiskerLeft x η

@[simp]

theorem CategoryTheory.Bicategory.postcomposing_obj {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) (c : B) (f : b ⟶ c) : (CategoryTheory.Bicategory.postcomposing a b c).obj f = CategoryTheory.Bicategory.postcomp a f

def CategoryTheory.Bicategory.associatorNatIsoLeft {B : Type u} [CategoryTheory.Bicategory B] {b : B} {c : B} {d : B} (a : B) (g : b ⟶ c) (h : c ⟶ d) : ((CategoryTheory.Bicategory.postcomposing a b c).obj g).comp ((CategoryTheory.Bicategory.postcomposing a c d).obj h) ≅ (CategoryTheory.Bicategory.postcomposing a b d).obj (CategoryTheory.CategoryStruct.comp g h)

Left component of the associator as a natural isomorphism.

Equations

• CategoryTheory.Bicategory.associatorNatIsoLeft a g h = CategoryTheory.NatIso.ofComponents (fun (x : a ⟶ b) => CategoryTheory.Bicategory.associator x g h) ⋯

@[simp]

theorem CategoryTheory.Bicategory.associatorNatIsoLeft_inv_app {B : Type u} [CategoryTheory.Bicategory B] {b : B} {c : B} {d : B} (a : B) (g : b ⟶ c) (h : c ⟶ d) (X : a ⟶ b) : (CategoryTheory.Bicategory.associatorNatIsoLeft a g h).inv.app X = (CategoryTheory.Bicategory.associator X g h).inv

@[simp]

theorem CategoryTheory.Bicategory.associatorNatIsoLeft_hom_app {B : Type u} [CategoryTheory.Bicategory B] {b : B} {c : B} {d : B} (a : B) (g : b ⟶ c) (h : c ⟶ d) (X : a ⟶ b) : (CategoryTheory.Bicategory.associatorNatIsoLeft a g h).hom.app X = (CategoryTheory.Bicategory.associator X g h).hom

def CategoryTheory.Bicategory.associatorNatIsoMiddle {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (h : c ⟶ d) : ((CategoryTheory.Bicategory.precomposing a b c).obj f).comp ((CategoryTheory.Bicategory.postcomposing a c d).obj h) ≅ ((CategoryTheory.Bicategory.postcomposing b c d).obj h).comp ((CategoryTheory.Bicategory.precomposing a b d).obj f)

Middle component of the associator as a natural isomorphism.

Equations

• CategoryTheory.Bicategory.associatorNatIsoMiddle f h = CategoryTheory.NatIso.ofComponents (fun (x : b ⟶ c) => CategoryTheory.Bicategory.associator f x h) ⋯

@[simp]

theorem CategoryTheory.Bicategory.associatorNatIsoMiddle_hom_app {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (h : c ⟶ d) (X : b ⟶ c) : (CategoryTheory.Bicategory.associatorNatIsoMiddle f h).hom.app X = (CategoryTheory.Bicategory.associator f X h).hom

@[simp]

theorem CategoryTheory.Bicategory.associatorNatIsoMiddle_inv_app {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} {d : B} (f : a ⟶ b) (h : c ⟶ d) (X : b ⟶ c) : (CategoryTheory.Bicategory.associatorNatIsoMiddle f h).inv.app X = (CategoryTheory.Bicategory.associator f X h).inv

def CategoryTheory.Bicategory.associatorNatIsoRight {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) : (CategoryTheory.Bicategory.precomposing a c d).obj (CategoryTheory.CategoryStruct.comp f g) ≅ ((CategoryTheory.Bicategory.precomposing b c d).obj g).comp ((CategoryTheory.Bicategory.precomposing a b d).obj f)

Right component of the associator as a natural isomorphism.

Equations

• CategoryTheory.Bicategory.associatorNatIsoRight f g d = CategoryTheory.NatIso.ofComponents (fun (x : c ⟶ d) => CategoryTheory.Bicategory.associator f g x) ⋯

@[simp]

theorem CategoryTheory.Bicategory.associatorNatIsoRight_hom_app {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) (X : c ⟶ d) : (CategoryTheory.Bicategory.associatorNatIsoRight f g d).hom.app X = (CategoryTheory.Bicategory.associator f g X).hom

@[simp]

theorem CategoryTheory.Bicategory.associatorNatIsoRight_inv_app {B : Type u} [CategoryTheory.Bicategory B] {a : B} {b : B} {c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) (X : c ⟶ d) : (CategoryTheory.Bicategory.associatorNatIsoRight f g d).inv.app X = (CategoryTheory.Bicategory.associator f g X).inv

def CategoryTheory.Bicategory.leftUnitorNatIso {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) : (CategoryTheory.Bicategory.precomposing a a b).obj (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.Functor.id (a ⟶ b)

Left unitor as a natural isomorphism.

Equations

• CategoryTheory.Bicategory.leftUnitorNatIso a b = CategoryTheory.NatIso.ofComponents (fun (x : a ⟶ b) => CategoryTheory.Bicategory.leftUnitor x) ⋯

@[simp]

theorem CategoryTheory.Bicategory.leftUnitorNatIso_inv_app {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) (X : a ⟶ b) : (CategoryTheory.Bicategory.leftUnitorNatIso a b).inv.app X = (CategoryTheory.Bicategory.leftUnitor X).inv

@[simp]

theorem CategoryTheory.Bicategory.leftUnitorNatIso_hom_app {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) (X : a ⟶ b) : (CategoryTheory.Bicategory.leftUnitorNatIso a b).hom.app X = (CategoryTheory.Bicategory.leftUnitor X).hom

def CategoryTheory.Bicategory.rightUnitorNatIso {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) : (CategoryTheory.Bicategory.postcomposing a b b).obj (CategoryTheory.CategoryStruct.id b) ≅ CategoryTheory.Functor.id (a ⟶ b)

Right unitor as a natural isomorphism.

Equations

• CategoryTheory.Bicategory.rightUnitorNatIso a b = CategoryTheory.NatIso.ofComponents (fun (x : a ⟶ b) => CategoryTheory.Bicategory.rightUnitor x) ⋯

@[simp]

theorem CategoryTheory.Bicategory.rightUnitorNatIso_hom_app {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) (X : a ⟶ b) : (CategoryTheory.Bicategory.rightUnitorNatIso a b).hom.app X = (CategoryTheory.Bicategory.rightUnitor X).hom

@[simp]

theorem CategoryTheory.Bicategory.rightUnitorNatIso_inv_app {B : Type u} [CategoryTheory.Bicategory B] (a : B) (b : B) (X : a ⟶ b) : (CategoryTheory.Bicategory.rightUnitorNatIso a b).inv.app X = (CategoryTheory.Bicategory.rightUnitor X).inv