English
For a functor F: J ⥤ Type, the sections are the families u_j ∈ F.obj j for each object j of J, such that for every morphism f: j ⟶ j', F.map f (u_j) = u_{j'}. These sections form a set.
Русский
Для функторa F: J ⥤ Type секции — это семейство элементов u_j ∈ F.obj j для каждого объекта j, такое что для каждого морфизма f: j ⟶ j' выполняется F.map f (u_j) = u_{j'}. Эти секции образуют множество.
LaTeX
$$$$ \mathrm{sections}(F) = \{ u:\prod_{j\in \mathrm{Obj}(J)} F(j) \mid \forall f:\; j \to j',\ F(f)(u_j)=u_{j'} \}. $$$$
Lean4
/-- The sections of a functor `F : J ⥤ Type` are
the choices of a point `u j : F.obj j` for each `j`,
such that `F.map f (u j) = u j'` for every morphism `f : j ⟶ j'`.
We later use these to define limits in `Type` and in many concrete categories.
-/
def sections (F : J ⥤ Type w) : Set (∀ j, F.obj j) :=
{u | ∀ {j j'} (f : j ⟶ j'), F.map f (u j) = u j'}
