homMk

Mathlib.CategoryTheory.Monoidal.Free.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.FreeMonoidalCategory.homMk

Lean4

/-- The abbreviation for `⟦f⟧`. -/
/- This is useful since the notation `⟦f⟧` often behaves like an element of the quotient set,
but not like a morphism. This is why we need weird `@CategoryStruct.comp (F C) ...` in the
statement in `mk_comp` above. -/

abbrev homMk {X Y : F C} (f : X ⟶ᵐ Y) : X ⟶ Y :=
  ⟦f⟧

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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