ofCocone

Mathlib.CategoryTheory.Limits.Shapes.Equalizers

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Limits.Cofork.ofCocone

Lean4

/-- Given `F : WalkingParallelPair ⥤ C`, which is really the same as
`parallelPair (F.map left) (F.map right)` and a cocone on `F`, we get a cofork on
`F.map left` and `F.map right`. -/
def ofCocone {F : WalkingParallelPair ⥤ C} (t : Cocone F) : Cofork (F.map left) (F.map right)
    where
  pt := t.pt
  ι :=
    { app := fun X => eqToHom (by simp) ≫ t.ι.app X
      naturality := by rintro _ _ (_ | _ | _) <;> simp }

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

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

Разделы

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

Аффилиация

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