-
for_mathlib.lean: general infrastructure -
pfunctor/: polynomial functors, including M and W types -
qpf.lean: quotients of unary polynomial functors, initial algebras, final coalgebras, and closure under quotients and composition. This is subsumed by the multivariate versions, which do not depend on the unary versions, though the latter are instructive. -
mvfunctor/: multivariate functors -
mvpfunctor/: multivariate polynomial functors, including multivariate M and W -
mvqpf/: multivariate qpfs -
data/: a Lean front end for specifying data types based on these constructions. This is still work in progress.