English
Let F : J ⥤ Type be a diagram and let s be a section of F (i.e., a family s(j) ∈ F.obj j compatible with the functor). Then there exists a cone over F with cone point PUnit whose projection to each j is s(j).
Русский
Пусть F : J ⥤ Type задан диаграммой и s — секция F (множество значений s(j) ∈ F.obj j, совместимая с отображениями). Тогда существует конус над F с вершиной в PUnit и проекциями π_j, удовлетворяющими π_j = s(j).
LaTeX
$$$\\text{Let } F : J \\to \\mathbf{Type} \\text{ be a diagram and } s \\in F.\\text{sections}.\\text{ Then there exists a cone } \\mathcal{C} \\text{ over } F \\text{ with } \\mathrm{pt}(\\mathcal{C}) = PUnit \\text{ and } \\pi_j = s(j).$$$
Lean4
/-- Given a section of a functor F into `Type*`,
construct a cone over F with `PUnit` as the cone point. -/
def coneOfSection {s} (hs : s ∈ F.sections) : Cone F
where
pt := PUnit
π := { app := fun j _ ↦ s j, naturality := fun i j f ↦ by ext; exact (hs f).symm }
