2023/03/10 by Thomas Ehrhard, Ehrhard, Thomas, Aymeric Walch +1
Computer Science · Mathematics · #Logic, Reasoning, and Knowledge #Homotopy and Cohomology in Algebraic Topology
paper · pdf · doi:10.48550/arxiv.2303.06952
We extend to general Cartesian categories the idea of Coherent Differentiation recently introduced by Ehrhard in the setting of categorical models of Linear Logic. The first ingredient is a summability structure which induces a partial left-additive structure on the category. Additional functoriality and naturality assumptions on this summability structure implement a differential calculus which can also be presented in a formalism close to Blute, Cockett and Seely's Cartesian differential categories. We show that a simple term language equipped with a natural notion of differentiation can easily be interpreted in such a category.