一句话：提出群胚的 thin spans 双范畴，并证明其 Kleisli 双范畴在伪余单子 ! 下是笛卡尔闭的。
语言的双范畴语义需要区分执行迹，并将归约路径解释为同构，但已有广义结构物种、同伦模板博弈等模型因语义个体可携带任意对称性而呈饱和、解释被膨胀。本文提出“薄”模型：群胚的 thin spans 双范畴。其对象为带额外结构的群胚，态射为跨度，按普通拉回复合，恒等为恒等跨度；2-胞是使诱导三角形仅在同构意义下交换的跨度态射。作者构造双范畴 Thin，为其配备伪余单子 !，并证明 Kleisli 双范畴 Thin! 是笛卡尔闭的。模型借鉴 thin concurrent games：项的解释不携带对称性，而语义个体通过双正交性满足一个精细不变式，从而在对称性下不变。
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 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 Thin with a pseudocomonad !, and finally show that the Kleisli bicategory Thin! is cartesian closed.