English
Given a cone c over F and a point x in its cone point, define a section s of F by s(j) = c.π.app j x, and the naturality condition holds automatically by the cone’s naturality.
Русский
Пусть дан конус c над F и элемент x в вершине конуса. Определим секцию s по формуле s(j) = c.π.app j x; естественность следует из натурализованности конуса.
LaTeX
$$$\\text{Given } c: \\mathrm{Cone}(F) \\text{ and } x \\in c.pt,\\; s: J \\to \\bigcup_j F.obj j \\text{ defined by } s(j) = c.\\pi_{j}(x),\\text{ with } F.map(f)(s(i)) = s(j) \\text{ for all } f:i\\to j.$$$
Lean4
/-- Given a cone over a functor F into `Type*` and an element in the cone point,
construct a section of F. -/
def sectionOfCone (c : Cone F) (x : c.pt) : F.sections :=
⟨fun j ↦ c.π.app j x, fun f ↦ congr_fun (c.π.naturality f).symm x⟩
