homMk

Mathlib.CategoryTheory.Bicategory.Extension

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

Lean4

/-- To construct a morphism between right lifts, we need a 2-morphism between the lifts,
and to check that it is compatible with the counits. -/
abbrev homMk {s t : RightLift f g} (η : s.lift ⟶ t.lift) (w : η ▷ f ≫ t.counit = s.counit) : s ⟶ t :=
  CostructuredArrow.homMk η w

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

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

Разделы

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

Аффилиация

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