English
The composition of functors is itself a functor: there is a map on Comp F G that corresponds to applying map to the inner G i components and then reassembling with mk.
Русский
Композиция функторов сама является функтором: существует отображение для Comp F G, соответствующее применению отображения ко внутренним компонентам G_i и повторной сборке через mk.
LaTeX
$$$\mathrm{Comp}.\mathrm{map}(f): \operatorname{Comp} F G \alpha \to \operatorname{Comp} F G \beta\;\text{defined by}\; \mathrm{mk} \bigl( (\mathrm{G}_i) \mathrm{map} f (x) \bigr)_{i}.$$$
Lean4
/-- The composition of functors is itself functorial -/
protected def map : (Comp F G) α → (Comp F G) β :=
(map fun _i ↦ map f : (F fun i ↦ G i α) → F fun i ↦ G i β)
