Multivariate polynomial functors. #
Multivariate polynomial functors are used for defining M-types and W-types.
They map a type vector
α to the type
Σ a : A, B a ⟹ α, with
A : Type and
B : A → TypeVec n. They interact well with Lean's inductive definitions because
they guarantee that occurrences of
α are positive.
append arrows of a polynomial functor application