The Cartesian Closed Bicategory of Thin Spans of Groupoids
share
Recently, there has been growing interest in bicategorical models of programming languages, which are "proof-relevant" in the sense that they keep distinct account of execution traces leading to the same observable outcomes, while assigning a formal meaning to reduction paths as isomorphisms. In this paper we introduce a new model, a bicategory called thin spans of groupoids. Conceptually it is close to Fiore et al.'s generalized species of structures and to Melliès' homotopy template games, but fundamentally differs as to how replication of resources and the resulting symmetries are treated. Where those models are saturated – the interpretation is inflated by the fact that semantic individuals may carry arbitrary symmetries – our model is thin, drawing inspiration from thin concurrent games: the interpretation of terms carries no symmetries, but semantic individuals satisfy a subtle invariant defined via biorthogonality, which guarantees their invariance under symmetry. We first build the bicategory 𝐓𝐡𝐢𝐧 of thin spans of groupoids. Its objects are certain groupoids with additional structure, its morphisms are spans composed via plain pullback with identities the identity spans, and its 2-cells are span morphisms making the induced triangles commute only up to natural isomorphism. We then equip 𝐓𝐡𝐢𝐧 with a pseudocomonad !, and finally show that the Kleisli bicategory 𝐓𝐡𝐢𝐧_! is cartesian closed.
READ FULL TEXT