id_eq

Mathlib.CategoryTheory.Bicategory.CatEnriched

URI: https://scilib.ai/kg/mathlib#CategoryTheory.CatEnrichedOrdinary.Hom.id_eq

English

The identity 2-cell on f equals Hom.mk (id (homEquiv f)).

Русский

Идентичная 2-ячейка на f равна Hom.mk(идентичность(homEquiv f)).

LaTeX

$$$ \\mathbf{1}_f = Hom.mk(\\mathbf{1}_{\\mathrm{homEquiv} f}) $$$

Lean4

theorem id_eq {X Y : CatEnrichedOrdinary C} (f : X ⟶ Y) : 𝟙 f = Hom.mk (𝟙 (homEquiv f)) :=
  rfl

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru