Polynomial fixpoint equations and bialgebras of inductive datatypes The combinatorial Dyson-Schwinger equations are fixpoint equations, commonly formulated inside predefined Connes-Kreimer-style Hopf algebras. Their solutions are infinite series, which can be accessed and manipulated thanks to their recursive structure, as exemplified by antipodes and BPHZ renormalisation. The aim of this talk is to explain how similar mechanisms play an important role in the foundations of mathematics, more concretely in constructive type theory. Here infinite structures are introduced in terms of syntactically defined induction principles, which simultaneously specify how terms can be constructed and how they can be accessed. The fundamental example is the set of natural numbers and ordinary induction. The induction principles are specified in terms of the basic type constructors: dependent sums and dependent products. In the categorical semantics, these are polynomial endofunctors, and the resulting inductive type is interpreted as the least fixpoint of the endofunctor (initial algebra). Combinatorially, the datatypes are always some kind of tree structures, and they always generate a graded bialgebra containing a canonical copy of the Faa di Bruno bialgebra. The recent homotopy interpretation of type theory facilitates the handling of symmetries, so as to make formal sense of the statement that Feynman graphs are inductive datatypes.