Proofs Verified with Lean4 (leanprover/lean4:v4.8.0-rc1)

Lean4 Formalization Of Polynomial Functors

This repository is a Lean 4 formalization of the theory of Polynomial Functors. Polynomial Functors categorify polynomials.

Acknowledgment

The work has been done during the Trimester Program "Prospects of formal mathematics" at the Hausdorff Institute (HIM) in Bonn.

Content (under development)

As part of this formalization, we also formalize locally cartesian closed categories in Lean4.

• Polynomial functors as endofunctors on the category of types
  • Definition of univariate polynomials as a type family
  • The construction of a bundle map associated to a polynomial
  • The construction of associated polynomial functor
  • Definition of multivariate polynomials and the associated polynomial functor
  • Monomials
  • Linear polynomials
  • Sums of polynomials
  • Products of polynomials
  • Composition of polynomials
  • The classifying property of polynomial functors
  • The category Type [X] of polynomial functors in one variable
  • Differential calculus of polynomials
• Polynomial functos in locally cartesian closed categories
  • Definition of locally cartesian closed category
  • Beck-Chevalley condition in LCCCs
  • Polynomial functors in LCCCs

Resources

• Tutorial on Polynomial Functors and Type Theory, Steve Awodey
• Polynomial functors and polynomial monads, Nicola Gambino and Joachim Kock
• Notes on Locally Cartesian Closed Categories, Sina Hazratpour
• Notes on Polynomial Functors, Joachim Kock