Theorems · Theorem · category theory

CategoryTheory.Bicategory.associatorNatIsoLeftCat_hom_toNatTrans_app

∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a : B) {b c d : B} (g : b ⟶ c) (h : c ⟶ d)
  (X : ↑(CategoryTheory.Cat.of (a ⟶ b))),
  (CategoryTheory.Bicategory.associatorNatIsoLeftCat a g h).hom.toNatTrans.app X =
    (CategoryTheory.Bicategory.associator X g h).hom

Defined in

Mathlib.CategoryTheory.Bicategory.Yoneda

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory