群胚细跨的笛卡尔闭双范畴

近来，作为编程语言双范畴模型的研究日益受到关注，这类模型具有“证明相关”的特性，即它们对导致相同可观测结果的执行轨迹加以区分记录，同时将归约路径赋予形式化意义，视其为同构。本文引入一个新模型，称为群胚细跨 (thin spans of groupoids) 的双范畴。它在概念上接近 Fiore 等人的广义结构物种与 Melliès 的同伦模板博弈，但在资源复制及其产生的对称性处理方式上有根本不同。那些模型是饱和的——其解释因语义个体可能携带任意对称性而膨胀——而我们的模型是细的，从细并发博弈中汲取灵感：项的解释不携带对称性，但语义个体满足通过双正交性定义的微妙不变式，从而保证其在对称性下的不变性。我们首先构建群胚细跨的双范畴 $\mathbf{Thin}$。其对象是带有附加结构的某些群胚，其态射是由普通拉回复合的跨，恒等态射为恒等跨，其 $2$-胞腔是使诱导三角形仅在自然同构意义下交换的跨态射。随后我们为 $\mathbf{Thin}$ 装备伪余单子 $!$，并最终证明 Kleisli 双范畴 $\mathbf{Thin}_{!}$ 是笛卡尔闭的。