A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory
A Cartesian Bicategory of Polynomial Functors in Homotopy Type Theory
复制标题
同伦型理论中多项式函子的笛卡尔二范畴
DOI：
--
复制
发表时间：
2021
期刊：
影响因子：
--
通讯作者：
Thomas Seiller
中科院分区：
文献类型：
--
作者：
Eric Finster;S. Mimram;M. Lucas;Thomas Seiller
多项式函子是多项式概念的范畴推广，它在更高范畴和类型论中有许多应用：这些函子是由多项式生成的，多项式由变量集构建的一组单项式组成。它们可以被组织成一个笛卡儿双范畴，不幸的是，由于两个原因，该范畴未能闭合，我们在这里通过适当修改模型来解决这一问题。首先，朴素闭包太大而无法良好定义，这可以通过限制为有限的多项式来克服。其次，由此产生的假定闭包没有适当地考虑2-范畴结构。我们主张在这里，这可以通过考虑群胚中的多项式来解决，而不是集合。对于这些，合成中涉及的构造必须执行到同伦，这在同伦类型论的背景下可以方便地处理：我们在这里使用它来正式执行在Agda中建立我们的笛卡尔双范畴所需的构造。值得注意的是，这需要我们在有限类型的小宇宙中引入公理化，作为自然数和双射的适当的高级归纳类型。
Polynomial functors are a categorical generalization of the usual notion of polynomial, which has found many applications in higher categories and type theory: those are generated by polynomials consisting a set of monomials built from sets of variables. They can be organized into a cartesian bicategory, which unfortunately fails to be closed for essentially two reasons, which we address here by suitably modifying the model. Firstly, a naive closure is too large to be well-defined, which can be overcome by restricting to polynomials which are finitary. Secondly, the resulting putative closure fails to properly take the 2-categorical structure in account. We advocate here that this can be addressed by considering polynomials in groupoids, instead of sets. For those, the constructions involved into composition have to be performed up to homotopy, which is conveniently handled in the setting of homotopy type theory: we use it here to formally perform the constructions required to build our cartesian bicategory, in Agda. Notably, this requires us introducing an axiomatization in a small universe of the type of finite types, as an appropriate higher inductive type of natural numbers and bijections.
-作为分析单子的操作
影响因子：
1
作者：
Gepner, David;Haugseng, Rune;Kock, Joachim
通讯作者：
Kock, Joachim
影响因子：
1.1
作者：
Altenkirch, Thorsten;Ghani, Neil;Morris, Peter
通讯作者：
Morris, Peter