English
Let C be a category. Suppose X, Y, Z are objects of C equipped with maps to a fixed object S (i.e. they are objects over S). If f: X → Y and g: Y → Z are morphisms over S, and X, Y, Z are over S in the appropriate sense, then the composite g ∘ f: X → Z is also over S. Equivalently, HomIsOver(g ∘ f, S) holds whenever HomIsOver(f, S) and HomIsOver(g, S) hold (together with the relevant OverClass hypotheses).
Русский
Пусть C — категория. Пусть X, Y, Z — объекты C, оснащённые отображениями в фиксированный объект S (то есть они являются объектами над S). Если f: X → Y и g: Y → Z над S, и X, Y, Z над S в соответствующем смысле, тогда композиция g ∘ f: X → Z тоже над S. Эквивалентно: если HomIsOver(f, S) и HomIsOver(g, S), то HomIsOver(g ∘ f, S).
LaTeX
$$$\forall {\mathcal C} \ [\text{Category}(\mathcal C)], \ X,Y,Z \in \mathcal C, \ S \in \mathcal C, \\ X \xrightarrow{f} Y \xrightarrow{g} Z, \[OverClass\ X\ S], [OverClass\ Y\ S], [OverClass\ Z\ S], [HomIsOver\ f\ S], [HomIsOver\ g\ S] \implies \ HomIsOver\ (g \circ f)\ S$$$
Lean4
instance [OverClass X S] [OverClass Y S] [OverClass Z S] (f : X ⟶ Y) (g : Y ⟶ Z) [HomIsOver f S] [HomIsOver g S] :
HomIsOver (f ≫ g) S where
