Polynomial Functors in Agda: Theory and Practice

Abstract

The category of polynomial functors - Poly - has been studied for over two decades and is well known for its relevance to computer science [1] and deep mathematical structure [2]. In recent years, new interpretations of Poly have been found in dynamical systems theory [3]. This thesis formalizes Poly in Cubical Agda and showcases its use in dynamical systems, contributing to the Poly code ecosystem.

The first part, theory, formalizes the category Poly itself and many of its categorical constructs, including the initial and terminal objects, product, coproduct, equalizer, composition and parallel product. Then Chart is formalized, together with its own categorical constructs. Finally, Poly and Chart morphisms are combined via commuting squares.

The second part, practice, builds upon the theory by using these categories to implement dynamical systems. It covers how morphisms in Poly represent dynamical systems, how polynomials act as interfaces, how systems are wired together, how behavior is installed into wiring diagrams, and how to run systems arriving at concrete programs. Many dynamical system examples are given, such as a Fibonacci sequence generator, the Lorenz system, the Hodkgin-Huxley model, and an Echo-State Network that learns the Lorenz dynamics. Commuting squares are used as a way of showing that one dynamical system can be made to simulate another.