Comp — Mathlib

English

For given n, m, a family of functors F and G, the composition Comp F G is the functor acting on m-ary vectors v by applying F to the family of m-ary functors G i applied to v; i.e., (Comp F G)(v) = F( i ↦ G i v ).

Русский

Для данных n, m и семейства функторов F и G композиция Comp F G является функтором по отношению к вектору типа m; он действует на вектора типа m так: (Comp F G)(v) = F( i ↦ G i v ).

LaTeX

$$$\mathrm{Comp}(v) = F\bigl(i \mapsto G(i)(v)\bigr).$$$

Lean4

/-- Composition of an `n`-ary functor with `n` `m`-ary
functors gives us one `m`-ary functor -/
def Comp (v : TypeVec.{u} m) : Type _ :=
  F fun i : Fin2 n ↦ G i v

Похожие утверждения