toCocone

Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.BinaryBicone.toCocone

Lean4

/-- Extract the cocone from a binary bicone. -/
def toCocone (c : BinaryBicone P Q) : Cocone (pair P Q) :=
  BinaryCofan.mk c.inl c.inr

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

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

Разделы

Аффилиация

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