同伦类型论中的多项式作为Kleisli范畴

范畴中的多项式已被研究为数学中传统概念的推广。其构造最近已由Finster、Mimram、Lucas和Seiller扩展到高群胚，后者在同伦类型论中形式化，从而得到一个笛卡尔闭双范畴。我们在多个方向上精炼并扩展了他们的工作。我们首先推广自由对称幺半群独异点在类型上的构造，以处理任意宇宙中的元数。然后，我们将这个独异点扩展到类型跨态的（野）范畴，并通过自对偶性得到一个余独异点。最后，我们证明由此产生的Kleisli范畴等价于传统的多项式范畴。这从而确立了多项式作为（同伦）线性逻辑模型。事实上，我们解释了它与Melli\`es引入的微分线性逻辑的双范畴模型密切相关。