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.
Functor composition on polynomial functors
Constructor for functor composition
Destructor for functor composition