Theorems · Theorem · category theory

CategoryTheory.StrictlyUnitaryLaxFunctor.map_id

∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryLaxFunctor B C) (X : B),
  self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)

Defined in

Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary

Cited by

2 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

CategoryTheory.BicategoryCategoryTheory.Bicategory