mathlib

ef89e9af - feat(data/qpf): compositional data type framework for inductive / coinductive types (#3317)

feat(data/qpf): compositional data type framework for inductive / coinductive types (#3317) First milestone of the QPF project. Includes multivariate quotients of polynomial functors and compiler for coinductive types. Not included in this PR * nested inductive / coinductive data types * universe polymorphism with more than one variable * inductive / coinductive families * equation compiler * efficient byte code implementation Those are coming in future PRs