Theorems · Theorem · category theory

CategoryTheory.Bicategory.associator_eqToHom_inv

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

Defined in

Mathlib.CategoryTheory.Bicategory.EqToHom

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory