Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.mapComp_id_left_hom_app_assoc

∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {a b : B}
  (f : a ⟶ b) (X : ↑(F.obj a)) {Z : ↑(F.obj b)}
  (h : (F.map f).toFunctor.obj ((F.map (CategoryTheory.CategoryStruct.id a)).toFunctor.obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((F.mapComp (CategoryTheory.CategoryStruct.id a) f).hom.toNatTrans.app X) h =
    CategoryTheory.CategoryStruct.comp ((F.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom).toNatTrans.app X)
      (CategoryTheory.CategoryStruct.comp ((F.map f).toFunctor.map ((F.mapId a).inv.toNatTrans.app X)) h)

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory