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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

def CategoryTheory.Bicategory.whiskerLeftIso {B : Type u} [Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) : CategoryStruct.comp f g ≅ 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_hom {B : Type u} [Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) : (whiskerLeftIso f η).hom = whiskerLeft f η.hom

@[simp]

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

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

@[simp]

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

def CategoryTheory.Bicategory.whiskerRightIso {B : Type u} [Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) : CategoryStruct.comp f h ≅ 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_inv {B : Type u} [Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) : (whiskerRightIso η h).inv = whiskerRight η.inv h

@[simp]

theorem CategoryTheory.Bicategory.whiskerRightIso_hom {B : Type u} [Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) : (whiskerRightIso η h).hom = whiskerRight η.hom h

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

theorem CategoryTheory.Bicategory.leftUnitor_whiskerRight {B : Type u} [Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) : whiskerRight (leftUnitor f).hom g = CategoryStruct.comp (associator (CategoryStruct.id a) f g).hom (leftUnitor (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} [Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) {Z : a ⟶ c} (h : CategoryStruct.comp f g ⟶ Z) : CategoryStruct.comp (whiskerRight (leftUnitor f).hom g) h = CategoryStruct.comp (associator (CategoryStruct.id a) f g).hom (CategoryStruct.comp (leftUnitor (CategoryStruct.comp f g)).hom h)

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

def CategoryTheory.Bicategory.precomp {B : Type u} [Bicategory B] {a b : B} (c : B) (f : a ⟶ b) : 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_obj {B : Type u} [Bicategory B] {a b : B} (c : B) (f : a ⟶ b) (x✝ : b ⟶ c) : (precomp c f).obj x✝ = CategoryStruct.comp f x✝

@[simp]

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

def CategoryTheory.Bicategory.precomposing {B : Type u} [Bicategory B] (a b c : B) : Functor (a ⟶ b) (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} [Bicategory B] (a b c : B) (f : a ⟶ b) : (precomposing a b c).obj f = precomp c f

@[simp]

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

def CategoryTheory.Bicategory.postcomp {B : Type u} [Bicategory B] {b c : B} (a : B) (f : b ⟶ c) : 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} [Bicategory B] {b c : B} (a : B) (f : b ⟶ c) (x✝ : a ⟶ b) : (postcomp a f).obj x✝ = CategoryStruct.comp x✝ f

@[simp]

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

def CategoryTheory.Bicategory.postcomposing {B : Type u} [Bicategory B] (a b c : B) : Functor (b ⟶ c) (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} [Bicategory B] (a b c : B) {X✝ Y✝ : b ⟶ c} (η : X✝ ⟶ Y✝) (x✝ : a ⟶ b) : ((postcomposing a b c).map η).app x✝ = whiskerLeft x✝ η

@[simp]

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

def CategoryTheory.Bicategory.associatorNatIsoLeft {B : Type u} [Bicategory B] {b c d : B} (a : B) (g : b ⟶ c) (h : c ⟶ d) : ((postcomposing a b c).obj g).comp ((postcomposing a c d).obj h) ≅ (postcomposing a b d).obj (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_hom_app {B : Type u} [Bicategory B] {b c d : B} (a : B) (g : b ⟶ c) (h : c ⟶ d) (X : a ⟶ b) : (associatorNatIsoLeft a g h).hom.app X = (associator X g h).hom

@[simp]

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

def CategoryTheory.Bicategory.associatorNatIsoMiddle {B : Type u} [Bicategory B] {a b c d : B} (f : a ⟶ b) (h : c ⟶ d) : ((precomposing a b c).obj f).comp ((postcomposing a c d).obj h) ≅ ((postcomposing b c d).obj h).comp ((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_inv_app {B : Type u} [Bicategory B] {a b c d : B} (f : a ⟶ b) (h : c ⟶ d) (X : b ⟶ c) : (associatorNatIsoMiddle f h).inv.app X = (associator f X h).inv

@[simp]

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

def CategoryTheory.Bicategory.associatorNatIsoRight {B : Type u} [Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) : (precomposing a c d).obj (CategoryStruct.comp f g) ≅ ((precomposing b c d).obj g).comp ((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_inv_app {B : Type u} [Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (d : B) (X : c ⟶ d) : (associatorNatIsoRight f g d).inv.app X = (associator f g X).inv

@[simp]

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

def CategoryTheory.Bicategory.leftUnitorNatIso {B : Type u} [Bicategory B] (a b : B) : (precomposing a a b).obj (CategoryStruct.id a) ≅ 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_hom_app {B : Type u} [Bicategory B] (a b : B) (X : a ⟶ b) : (leftUnitorNatIso a b).hom.app X = (leftUnitor X).hom

@[simp]

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

def CategoryTheory.Bicategory.rightUnitorNatIso {B : Type u} [Bicategory B] (a b : B) : (postcomposing a b b).obj (CategoryStruct.id b) ≅ 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} [Bicategory B] (a b : B) (X : a ⟶ b) : (rightUnitorNatIso a b).hom.app X = (rightUnitor X).hom

@[simp]

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