The Cartesian Closed Bicategory of Thin Spans of Groupoids

TL;DR

This paper introduces a new bicategorical model called thin spans of groupoids, which captures proof-relevant semantics of programming languages with a focus on resource replication and symmetries, differing from saturated models.

Contribution

The paper constructs a bicategory of thin spans of groupoids with a pseudocomonad, demonstrating that its Kleisli bicategory is cartesian closed, offering a novel approach to bicategorical semantics.

Findings

The bicategory of thin spans of groupoids is well-defined and structured.

The pseudocomonad $!$ on the bicategory leads to a cartesian closed Kleisli bicategory.

The model guarantees invariance under symmetries through a subtle biorthogonality invariant.

Abstract

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\`es' 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 $\mathbf{Thin}$ 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 $\mathbf{Thin}$ with a pseudocomonad $!$, and finally show that the Kleisli bicategory $\mathbf{Thin}_{!}$ is cartesian closed.