Cartesian polynomial monads in HoTT

Abstract

Modern math has shown the necessity of higher categories and higher structures. Infinite coherence data arises quite naturally as one considers various types of topological spaces and homotopy theory, as well as modern treatments of algebraic geometry. One can see simple versions of this problem already when looking at path composition in a topological space. Path composition is not strictly associative, but only associative up to a higher cell. One promising method of presenting higher structures is the development of homotopy type theory, which formulates spaces (up to homtopy equivalence) as its basic objects. However one major obstacle is notating the infinite coherences of infinity categories in homotopy type theory. This is due to the autophagy problem: how can one talk about algebraic structures on types, if the algebraic structures themselves are encoded as types? Here we discuss a solution to the problem by Finster, Allioux, and Sozeau by axiomatizing the nature of polynomial monads, hence allowing themselves certain computational equalities. They then go on to use these polynomial monads to discuss higher structures including higher categories. Essential to their method is Baez and Dolan’s slice construction, which is able to capture infinite coherences of polynomial monads even if one starts from very strict, classical polynomial monads. This integration of HoTT with polynomial monads I believe is incredibly interesting and could prove to be a very useful foundation/computational system.