The double category Int(Poly_+) models control flow and data flow

Author

David Spivak

Published

July 15, 2025

Abstract
(Joint work in progress with Grigory Kondyrev @ Noeon).
The category Set_+ of pointed sets is traced cocartesian monoidal, which means it supports a notion of While-loops. In fact, it has an additional property, called uniformity, which implies a lot of nice things, including that Int(Set_+) has a double category structure and that Fun(C, Set_+) is uniform traced cocartesian monoidal for any small category C. It follows that Poly_+ is also traced cocartesian monoidal. I’ll explain that Int(Poly_+) is a double category that corresponds to nice working diagrams modeling data and control flow.