Theorems · Theorem · category theory

CategoryTheory.Bicategory.associator_eqToHom_hom_assoc

∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y z t : B} (e₁ : x = y) (e₂ : y = z) (e₃ : z = t) {Z : x ⟶ t}
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom e₁)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom e₂) (CategoryTheory.eqToHom e₃)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.eqToHom e₁) (CategoryTheory.eqToHom e₂)
          (CategoryTheory.eqToHom e₃)).hom
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.eqToHomTransIso e₁ e₂).inv
        (CategoryTheory.eqToHom e₃))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.eqToHomTransIso ⋯ e₃).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.eqToHomTransIso e₁ ⋯).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.eqToHom e₁)
              (CategoryTheory.Bicategory.eqToHomTransIso e₂ e₃).hom)
            h)))

Defined in

Mathlib.CategoryTheory.Bicategory.EqToHom

Cited by

0 results in Mathlib

Foundations

Depth 26 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.Bicategory