Theorems · Theorem · category theory

CategoryTheory.StrictPseudofunctor.toFunctor_obj

∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : CategoryTheory.Bicategory.Strict B] [inst_3 : CategoryTheory.Bicategory.Strict C]
  (F : CategoryTheory.StrictPseudofunctor B C) (a : B), F.toFunctor.obj a = F.obj a

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor

Cited by

0 results in Mathlib

Foundations

Depth 12 from the axioms · uses no axioms

Assumes

CategoryTheory.BicategoryCategoryTheory.BicategoryCategoryTheory.Bicategory.StrictCategoryTheory.Bicategory.Strict