vId

Mathlib.CategoryTheory.Functor.TwoSquare

URI: https://scilib.ai/kg/mathlib#CategoryTheory.TwoSquare.vId

Lean4

/-- The vertical identity 2-square. -/
@[simps!]
def vId (T : C₁ ⥤ C₂) : TwoSquare T (𝟭 _) (𝟭 _) T :=
  𝟙 _

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

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

Разделы

Аффилиация

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