Theorems · Theorem · category theory

CategoryTheory.Pseudofunctor.ObjectProperty.mapId_inv_app

∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (P : F.ObjectProperty) [inst_1 : P.IsClosedUnderMapObj] {X : B} (M : P.Obj X),
  (P.mapId X).inv.app M = CategoryTheory.ObjectProperty.homMk ((F.mapId X).inv.toNatTrans.app M.obj)

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.Cat.ObjectProperty

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.BicategoryCategoryTheory.Pseudofunctor.ObjectProperty.IsClosedUnderMapObj