English
Dually, given a diagram of cocones and a cocone over the uncurry of a two-variable functor, yields a cocone over the diagram of cocone points.
Русский
Аналогично, дано диаграмма коконусов и кокон над uncurryobj F, получаем коконие над диаграммой коконeв.
LaTeX
$$$\\text{coconeOfCoconeUncurry}(D,Q,c) : \\text{Cocone } D.\\mathrm{coconePoints}$$$
Lean4
/-- Given a diagram `D` of limit cones over the `curry.obj G j`, and a cone over `G`,
we can construct a cone over the diagram consisting of the cone points from `D`.
-/
@[simps]
def coneOfConeCurry {D : DiagramOfCones (curry.obj G)} (Q : ∀ j, IsLimit (D.obj j)) (c : Cone G) : Cone D.conePoints
where
pt := c.pt
π :=
{ app
j :=
(Q j).lift
{ pt := c.pt
π := { app k := c.π.app (j, k) } }
naturality {_ j'} _ := (Q j').hom_ext (by simp) }
