Theorems · Theorem · category theory

CategoryTheory.Bicategory.inv_hom_whiskerRight_assoc

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

Defined in

Mathlib.CategoryTheory.Bicategory.Basic

Cited by

4 results in Mathlib

Foundations

Depth 6 from the axioms · uses Quot.sound

Assumes

CategoryTheory.Bicategory