Sina Hazratpour: Polynomial Functors in Lean 4
[Note: we meet in room 3.06]
Sina Hazratpour (Johns Hopkins University, USA)
Abstract: Polynomial functors, a categorification of the ordinary notion of polynomials in algebra, are a key tool in category theory with applications to various areas such as semantics of dependent type theory and programming languages, operadic higher algebra, combinatorial species, and categorical dynamical systems. In this talk, I shall report on a recent formalization of polynomial functors in the Lean theorem prover. I will discuss the design of the library and potential API improvements.
As an application, I will discuss a collaborative work-in-progress with Steve Awodey and Mario Carneiro on obtaining a groupoid model of HoTT in Lean4 using the polynomial based natural model of dependent type theory.
Formalization repositories:
