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.

翻译：最近，人们对编程语言的二范畴模型兴趣日益增长，这些模型在"证明相关"的意义上，能够区分导致相同可观察结果的执行轨迹，同时为作为同构的归约路径赋予形式化含义。本文引入了一个新模型，即称为群胚薄跨的二范畴。该模型在概念上接近Fiore等人的广义结构种和Melliès的同伦模板博弈，但在资源复制及由此产生的对称性处理方式上存在根本差异。那些模型是饱和的——语义个体可能携带任意对称性导致解释膨胀；而我们的模型薄化则受薄并发博弈启发：项的解释不携带对称性，但语义个体通过双正交性满足一个精妙的不变量，确保其对称不变性。我们首先构建群胚薄跨的二范畴$\mathbf{Thin}$，其对象为具有附加结构的特定群胚，态射为通过普通拉回组合的跨（单位态射为单位跨），2-胞腔为仅使诱导三角形在自然同构意义下交换的跨态射。随后为$\mathbf{Thin}$配备伪余单子$!$，最终证明Kleisli二范畴$\mathbf{Thin}_{!}$是笛卡尔闭的。