Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.mapComp_id_right_hom_app

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

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor

Cited by

1 results in Mathlib

Foundations

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

Assumes

CategoryTheory.Bicategory