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.
Applying P
to an object of Type
Instances For
Applying P
to a morphism of Type
Instances For
Constant functor where the input object does not affect the output
Instances For
Constructor for the constant functor
Instances For
Destructor for the constant functor
Instances For
Functor composition on polynomial functors
Instances For
Constructor for functor composition
Instances For
Destructor for functor composition
Instances For
Split polynomial functor, get an n-ary functor
from an n+1
-ary functor
Instances For
Split polynomial functor, get a univariate functor
from an n+1
-ary functor
Instances For
append arrows of a polynomial functor application