Documentation

Mathlib.CategoryTheory.Bicategory.Basic

Bicategories #

In this file we define typeclass for bicategories.

A bicategory B consists of

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

A typeclass for bicategories extends CategoryTheory.CategoryStruct typeclass. This means that we have

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

The composition of 1-morphisms is in fact 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.

source
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.

Instances
    source
    def CategoryTheory.Bicategory.«term_◁_» :
    Lean.TrailingParserDescr
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def CategoryTheory.Bicategory.«term_▷_» :
      Lean.TrailingParserDescr
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def CategoryTheory.Bicategory.termα_ :
        Lean.ParserDescr
        Equations
        Instances For
          source
          def CategoryTheory.Bicategory.«termλ_» :
          Lean.ParserDescr
          Equations
          Instances For
            source
            def CategoryTheory.Bicategory.termρ_ :
            Lean.ParserDescr
            Equations
            Instances For

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

              source
              theorem CategoryTheory.Bicategory.id_whiskerLeft_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a b : B} {f 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))
              source
              theorem CategoryTheory.Bicategory.comp_whiskerLeft_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h 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✝))
              source
              theorem CategoryTheory.Bicategory.whisker_assoc_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g 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✝))
              source
              theorem CategoryTheory.Bicategory.whiskerRight_id_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a b : B} {f 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))
              source
              theorem CategoryTheory.Bicategory.whiskerRight_comp_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a b c d : B} {f 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✝))
              source
              theorem CategoryTheory.Bicategory.whisker_exchange_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} {h 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✝)
              source
              theorem CategoryTheory.Bicategory.comp_whiskerRight_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a b c : B} {f g 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✝)
              source
              theorem CategoryTheory.Bicategory.whiskerLeft_comp_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h 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✝)
              source
              @[simp]
              theorem CategoryTheory.Bicategory.pentagon_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a b c d 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✝)
              source
              @[simp]
              theorem CategoryTheory.Bicategory.triangle_assoc {B : Type u} [self : CategoryTheory.Bicategory B] {a 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
              source
              @[simp]
              theorem CategoryTheory.Bicategory.whiskerLeft_hom_inv {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g 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)
              source
              @[simp]
              theorem CategoryTheory.Bicategory.whiskerLeft_hom_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g 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✝
              source
              @[simp]
              theorem CategoryTheory.Bicategory.hom_inv_whiskerRight {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f 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)
              source
              @[simp]
              theorem CategoryTheory.Bicategory.hom_inv_whiskerRight_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f 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✝
              source
              @[simp]
              theorem CategoryTheory.Bicategory.whiskerLeft_inv_hom {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g 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)
              source
              @[simp]
              theorem CategoryTheory.Bicategory.whiskerLeft_inv_hom_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g 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✝
              source
              @[simp]
              theorem CategoryTheory.Bicategory.inv_hom_whiskerRight {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f 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)
              source
              @[simp]
              theorem CategoryTheory.Bicategory.inv_hom_whiskerRight_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f 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✝
              source
              def CategoryTheory.Bicategory.whiskerLeftIso {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g 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
              Instances For
                source
                @[simp]
                theorem CategoryTheory.Bicategory.whiskerLeftIso_inv {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
                (CategoryTheory.Bicategory.whiskerLeftIso f η).inv = CategoryTheory.Bicategory.whiskerLeft f η.inv
                source
                @[simp]
                theorem CategoryTheory.Bicategory.whiskerLeftIso_hom {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ≅ h) :
                (CategoryTheory.Bicategory.whiskerLeftIso f η).hom = CategoryTheory.Bicategory.whiskerLeft f η.hom
                source
                instance CategoryTheory.Bicategory.whiskerLeft_isIso {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) [CategoryTheory.IsIso η] :
                CategoryTheory.IsIso (CategoryTheory.Bicategory.whiskerLeft f η)
                source
                @[simp]
                theorem CategoryTheory.Bicategory.inv_whiskerLeft {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) {g h : b ⟶ c} (η : g ⟶ h) [CategoryTheory.IsIso η] :
                CategoryTheory.inv (CategoryTheory.Bicategory.whiskerLeft f η) = CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.inv η)
                source
                def CategoryTheory.Bicategory.whiskerRightIso {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f 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.
                Instances For
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.whiskerRightIso_hom {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) :
                  (CategoryTheory.Bicategory.whiskerRightIso η h).hom = CategoryTheory.Bicategory.whiskerRight η.hom h
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.whiskerRightIso_inv {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) :
                  (CategoryTheory.Bicategory.whiskerRightIso η h).inv = CategoryTheory.Bicategory.whiskerRight η.inv h
                  source
                  instance CategoryTheory.Bicategory.whiskerRight_isIso {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) [CategoryTheory.IsIso η] :
                  CategoryTheory.IsIso (CategoryTheory.Bicategory.whiskerRight η h)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.inv_whiskerRight {B : Type u} [CategoryTheory.Bicategory B] {a b c : B} {f g : a ⟶ b} (η : f ⟶ g) (h : b ⟶ c) [CategoryTheory.IsIso η] :
                  CategoryTheory.inv (CategoryTheory.Bicategory.whiskerRight η h) = CategoryTheory.Bicategory.whiskerRight (CategoryTheory.inv η) h
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_inv {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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✝)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_inv_inv_hom_hom_inv {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_inv_inv_hom_hom_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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✝)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_inv {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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✝)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_inv {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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✝)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_hom_hom_inv_hom_hom {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_hom_hom_inv_hom_hom_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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✝)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_hom {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_hom_inv_inv_inv_hom_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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✝)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_hom_hom_inv_inv_hom {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_hom_hom_inv_inv_hom_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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✝)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_hom {B : Type u} [CategoryTheory.Bicategory B] {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).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)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_inv_hom_hom_hom_hom_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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✝)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_inv_inv_hom_inv_inv {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.pentagon_inv_inv_hom_inv_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d 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✝)
                  source
                  theorem CategoryTheory.Bicategory.triangle_assoc_comp_left {B : Type u} [CategoryTheory.Bicategory B] {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
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.triangle_assoc_comp_right {B : Type u} [CategoryTheory.Bicategory B] {a 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
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.triangle_assoc_comp_right_assoc {B : Type u} [CategoryTheory.Bicategory B] {a 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
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.triangle_assoc_comp_right_inv {B : Type u} [CategoryTheory.Bicategory B] {a 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
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.triangle_assoc_comp_right_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a 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
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.triangle_assoc_comp_left_inv {B : Type u} [CategoryTheory.Bicategory B] {a 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
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.triangle_assoc_comp_left_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a 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
                  source
                  theorem CategoryTheory.Bicategory.associator_naturality_left {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} {f 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))
                  source
                  theorem CategoryTheory.Bicategory.associator_naturality_left_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} {f 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✝)
                  source
                  theorem CategoryTheory.Bicategory.associator_inv_naturality_left {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} {f 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)
                  source
                  theorem CategoryTheory.Bicategory.associator_inv_naturality_left_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} {f 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✝)
                  source
                  theorem CategoryTheory.Bicategory.whiskerRight_comp_symm {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} {f 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)
                  source
                  theorem CategoryTheory.Bicategory.whiskerRight_comp_symm_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} {f 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✝))
                  source
                  theorem CategoryTheory.Bicategory.associator_naturality_middle {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g 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))
                  source
                  theorem CategoryTheory.Bicategory.associator_naturality_middle_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g 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✝)
                  source
                  theorem CategoryTheory.Bicategory.associator_inv_naturality_middle {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g 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)
                  source
                  theorem CategoryTheory.Bicategory.associator_inv_naturality_middle_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g 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✝)
                  source
                  theorem CategoryTheory.Bicategory.whisker_assoc_symm {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g 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)
                  source
                  theorem CategoryTheory.Bicategory.whisker_assoc_symm_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) {g 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✝))
                  source
                  theorem CategoryTheory.Bicategory.associator_naturality_right {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h 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 η))
                  source
                  theorem CategoryTheory.Bicategory.associator_naturality_right_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h 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✝)
                  source
                  theorem CategoryTheory.Bicategory.associator_inv_naturality_right {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h 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) η)
                  source
                  theorem CategoryTheory.Bicategory.associator_inv_naturality_right_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h 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✝)
                  source
                  theorem CategoryTheory.Bicategory.comp_whiskerLeft_symm {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h 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)
                  source
                  theorem CategoryTheory.Bicategory.comp_whiskerLeft_symm_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) {h 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✝))
                  source
                  theorem CategoryTheory.Bicategory.leftUnitor_naturality {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f 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 η
                  source
                  theorem CategoryTheory.Bicategory.leftUnitor_naturality_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f 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)
                  source
                  theorem CategoryTheory.Bicategory.leftUnitor_inv_naturality {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f 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) η)
                  source
                  theorem CategoryTheory.Bicategory.leftUnitor_inv_naturality_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f 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)
                  source
                  theorem CategoryTheory.Bicategory.id_whiskerLeft_symm {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f 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)
                  source
                  theorem CategoryTheory.Bicategory.rightUnitor_naturality {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f 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 η
                  source
                  theorem CategoryTheory.Bicategory.rightUnitor_naturality_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f 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)
                  source
                  theorem CategoryTheory.Bicategory.rightUnitor_inv_naturality {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f 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))
                  source
                  theorem CategoryTheory.Bicategory.rightUnitor_inv_naturality_assoc {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f 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)
                  source
                  theorem CategoryTheory.Bicategory.whiskerRight_id_symm {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f 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)
                  source
                  theorem CategoryTheory.Bicategory.whiskerLeft_iff {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η θ : f ⟶ g) :
                  CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) η = CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.CategoryStruct.id a) θ ↔ η = θ
                  source
                  theorem CategoryTheory.Bicategory.whiskerRight_iff {B : Type u} [CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η θ : f ⟶ g) :
                  CategoryTheory.Bicategory.whiskerRight η (CategoryTheory.CategoryStruct.id b) = CategoryTheory.Bicategory.whiskerRight θ (CategoryTheory.CategoryStruct.id b) ↔ η = θ
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.leftUnitor_whiskerRight {B : Type u} [CategoryTheory.Bicategory B] {a 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).

                  source
                  theorem CategoryTheory.Bicategory.leftUnitor_whiskerRight_assoc {B : Type u} [CategoryTheory.Bicategory B] {a 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)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.leftUnitor_inv_whiskerRight {B : Type u} [CategoryTheory.Bicategory B] {a 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
                  source
                  theorem CategoryTheory.Bicategory.leftUnitor_inv_whiskerRight_assoc {B : Type u} [CategoryTheory.Bicategory B] {a 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)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.whiskerLeft_rightUnitor {B : Type u} [CategoryTheory.Bicategory B] {a 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
                  source
                  theorem CategoryTheory.Bicategory.whiskerLeft_rightUnitor_assoc {B : Type u} [CategoryTheory.Bicategory B] {a 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)
                  source
                  @[simp]
                  theorem CategoryTheory.Bicategory.whiskerLeft_rightUnitor_inv {B : Type u} [CategoryTheory.Bicategory B] {a 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
                  source
                  theorem CategoryTheory.Bicategory.whiskerLeft_rightUnitor_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a 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)
                  source
                  theorem CategoryTheory.Bicategory.leftUnitor_comp {B : Type u} [CategoryTheory.Bicategory B] {a 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)
                  source
                  theorem CategoryTheory.Bicategory.leftUnitor_comp_assoc {B : Type u} [CategoryTheory.Bicategory B] {a 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)
                  source
                  theorem CategoryTheory.Bicategory.leftUnitor_comp_inv {B : Type u} [CategoryTheory.Bicategory B] {a 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
                  source
                  theorem CategoryTheory.Bicategory.leftUnitor_comp_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a 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)
                  source
                  theorem CategoryTheory.Bicategory.rightUnitor_comp {B : Type u} [CategoryTheory.Bicategory B] {a 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)
                  source
                  theorem CategoryTheory.Bicategory.rightUnitor_comp_assoc {B : Type u} [CategoryTheory.Bicategory B] {a 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)
                  source
                  theorem CategoryTheory.Bicategory.rightUnitor_comp_inv {B : Type u} [CategoryTheory.Bicategory B] {a 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
                  source
                  theorem CategoryTheory.Bicategory.rightUnitor_comp_inv_assoc {B : Type u} [CategoryTheory.Bicategory B] {a 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)
                  source
                  @[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
                  source
                  @[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
                  source
                  def CategoryTheory.Bicategory.precomp {B : Type u} [CategoryTheory.Bicategory B] {a 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.
                  Instances For
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.precomp_map {B : Type u} [CategoryTheory.Bicategory B] {a 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✝
                    source
                    @[simp]
                    theorem CategoryTheory.Bicategory.precomp_obj {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (c : B) (f : a ⟶ b) (x✝ : b ⟶ c) :
                    (CategoryTheory.Bicategory.precomp c f).obj x✝ = CategoryTheory.CategoryStruct.comp f x✝
                    source
                    def CategoryTheory.Bicategory.precomposing {B : Type u} [CategoryTheory.Bicategory B] (a 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.
                    Instances For
                      source
                      @[simp]
                      theorem CategoryTheory.Bicategory.precomposing_obj {B : Type u} [CategoryTheory.Bicategory B] (a b c : B) (f : a ⟶ b) :
                      (CategoryTheory.Bicategory.precomposing a b c).obj f = CategoryTheory.Bicategory.precomp c f
                      source
                      @[simp]
                      theorem CategoryTheory.Bicategory.precomposing_map_app {B : Type u} [CategoryTheory.Bicategory B] (a 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✝
                      source
                      def CategoryTheory.Bicategory.postcomp {B : Type u} [CategoryTheory.Bicategory 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.
                      Instances For
                        source
                        @[simp]
                        theorem CategoryTheory.Bicategory.postcomp_obj {B : Type u} [CategoryTheory.Bicategory B] {b c : B} (a : B) (f : b ⟶ c) (x✝ : a ⟶ b) :
                        (CategoryTheory.Bicategory.postcomp a f).obj x✝ = CategoryTheory.CategoryStruct.comp x✝ f
                        source
                        @[simp]
                        theorem CategoryTheory.Bicategory.postcomp_map {B : Type u} [CategoryTheory.Bicategory 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
                        source
                        def CategoryTheory.Bicategory.postcomposing {B : Type u} [CategoryTheory.Bicategory B] (a 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.
                        Instances For
                          source
                          @[simp]
                          theorem CategoryTheory.Bicategory.postcomposing_map_app {B : Type u} [CategoryTheory.Bicategory B] (a 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✝ η
                          source
                          @[simp]
                          theorem CategoryTheory.Bicategory.postcomposing_obj {B : Type u} [CategoryTheory.Bicategory B] (a b c : B) (f : b ⟶ c) :
                          (CategoryTheory.Bicategory.postcomposing a b c).obj f = CategoryTheory.Bicategory.postcomp a f
                          source
                          def CategoryTheory.Bicategory.associatorNatIsoLeft {B : Type u} [CategoryTheory.Bicategory B] {b c 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
                          Instances For
                            source
                            @[simp]
                            theorem CategoryTheory.Bicategory.associatorNatIsoLeft_inv_app {B : Type u} [CategoryTheory.Bicategory B] {b c 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
                            source
                            @[simp]
                            theorem CategoryTheory.Bicategory.associatorNatIsoLeft_hom_app {B : Type u} [CategoryTheory.Bicategory B] {b c 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
                            source
                            def CategoryTheory.Bicategory.associatorNatIsoMiddle {B : Type u} [CategoryTheory.Bicategory B] {a b c 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
                            Instances For
                              source
                              @[simp]
                              theorem CategoryTheory.Bicategory.associatorNatIsoMiddle_hom_app {B : Type u} [CategoryTheory.Bicategory B] {a b c 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
                              source
                              @[simp]
                              theorem CategoryTheory.Bicategory.associatorNatIsoMiddle_inv_app {B : Type u} [CategoryTheory.Bicategory B] {a b c 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
                              source
                              def CategoryTheory.Bicategory.associatorNatIsoRight {B : Type u} [CategoryTheory.Bicategory B] {a 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
                              Instances For
                                source
                                @[simp]
                                theorem CategoryTheory.Bicategory.associatorNatIsoRight_hom_app {B : Type u} [CategoryTheory.Bicategory B] {a 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
                                source
                                @[simp]
                                theorem CategoryTheory.Bicategory.associatorNatIsoRight_inv_app {B : Type u} [CategoryTheory.Bicategory B] {a 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
                                source
                                def CategoryTheory.Bicategory.leftUnitorNatIso {B : Type u} [CategoryTheory.Bicategory B] (a 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
                                Instances For
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Bicategory.leftUnitorNatIso_inv_app {B : Type u} [CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b) :
                                  (CategoryTheory.Bicategory.leftUnitorNatIso a b).inv.app X = (CategoryTheory.Bicategory.leftUnitor X).inv
                                  source
                                  @[simp]
                                  theorem CategoryTheory.Bicategory.leftUnitorNatIso_hom_app {B : Type u} [CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b) :
                                  (CategoryTheory.Bicategory.leftUnitorNatIso a b).hom.app X = (CategoryTheory.Bicategory.leftUnitor X).hom
                                  source
                                  def CategoryTheory.Bicategory.rightUnitorNatIso {B : Type u} [CategoryTheory.Bicategory B] (a 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
                                  Instances For
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Bicategory.rightUnitorNatIso_hom_app {B : Type u} [CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b) :
                                    (CategoryTheory.Bicategory.rightUnitorNatIso a b).hom.app X = (CategoryTheory.Bicategory.rightUnitor X).hom
                                    source
                                    @[simp]
                                    theorem CategoryTheory.Bicategory.rightUnitorNatIso_inv_app {B : Type u} [CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b) :
                                    (CategoryTheory.Bicategory.rightUnitorNatIso a b).inv.app X = (CategoryTheory.Bicategory.rightUnitor X).inv