Combinatorics of Trees via Derivatives of Polynomial Functors in Homotopy Type Theory

Source abstract

Polynomial functors are, essentially, polynomials whose variables take values in sets, groupoids, or some other suitable category, rather than in numbers. In this thesis, we will explore three related aspects of polynomial functors over $\infty$-groupoids in the framework of homotopy type theory: first, polynomial functors provide a foundation for inductively defined data types as wellfounded trees; second, polynomial functors have a notion of derivative which, viewed in light of the connection to data types, yields a computational interpretation of differentiation; and third, suitably finite polynomial functors over (higher) groupoids yield categorified generating functions, and thus subsume the theory of combinatorial species. We will develop these aspects of polynomial functors with binary trees as a recurring example, toward laying down the necessary machinery for sketching a Catalan bijection involving derivatives of polynomial functors.