多项式函子在具有对称性和多项式函数的数据类型中的应用

可在www.sciencedirect.com在线获取理论计算机科学电子笔记286（2012）351-365www.elsevier.com/locate/entcs群胚上具有对称性和多项式函子的数据类型Joachim Kock约阿希姆·科克1，2DepartamenteMatem`atiquesUnivrsitatAut`onomadeBarcelonaSpain摘要多项式函子（在Set或其他局部Carnival闭范畴上）在数据类型理论中很有用，它们通常被称为容器。 它们在代数学、组合学、拓扑学和更高范畴理论中也很有用，在这个更广泛的视角中，多项式方面往往是突出的，并证明了术语的合理性。例如，Tambara在这次演讲中，我将解释如何从集合到群胚（或其他局部carnival闭2-范畴）的理论升级对于处理具有对称性的数据类型是有用的，并为商容器（在Abbott等人的意义上）提供了一个共同的概括和一个干净的统一框架种类及分析函子（Joyal 1985），以及Baez和Dolan的stuff类型。多变量设置还包括关系和跨度、多跨度和填充运算符。 这个理论的一个吸引人的特点是，使用正确的同伦方法--同伦切片、同伦拉回、同伦余极限等--群胚的情况看起来和集合的情况完全一样。在一些标准的例子之后，我将用微扰量子场论的例子来说明具有对称性的数据类型的概念，其中图的复杂树结构的对称性起着至关重要的作用，并且可以使用群胚上的多项式函子来优雅地处理。（这些例子，虽然超越了物种，但纯粹是组合的，可以在没有量子场论背景的情况下理解。L o c a l l y c a r a l y c a r a l e c a l e d 2-c a t e g o r a l e g o r a l e c a l e d 2-c a t e g o r a l e d v e r a l e dM a r t i n-L o f i n t e n s i o n a l e d 2-c a t e g o r a l e d v e r a l e d 2-c a t e d v e r a l e d v e r a l e d 2-ca t e d v e r a l e d v e r a l e n n M a r t i n-L o f i n s i n s i o n a l e d 2-c a t e d v e r a l e d v e r a l e d 2-c at e d v e r a l e d v e r a l e d 2-c a t r a t e d v e r a l e d v e n l e r a l e d 2-c a t对于一个成熟的类型理论，似乎需要局部carbohydrate闭∞-范畴。 这些理论正在由David Gepner和作者作为同伦物种的设置进行开发，这次演讲中暴露的几个结果只是与Gepner联合工作中获得的∞结果的截断。细节将出现在其他地方。关键词：多项式函子，群胚，数据类型，对称性，物种，树。1集合上的多项式函子和数据类型1.1 单变量多项式函子 在最简单的形式中，多项式1Email：koc k @mat. u a b. 卡特2Andr e Joyal、NicolaGambi n o、A n - d er s Kock、ImmaGalve z、AndyTonk s和nd o tavidGe pn e r为R o rel ab o r ab o n o提供了一个完整的数据库。非常感谢西班牙的MTM 2009 -10359和MTM 2010 -20692文件的所有支持。1571-0661 © 2013 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2013.01.001352J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351函子是集合的闭函子，形式为ΣX›→XEb.（一）b∈B这 里 的 和 号 是 不 相 交 的 集 合 并 ， XEb 表 示 hom 集 合 Hom （ Eb ， X ） ， 并 且（Eb|b∈B）是一个B-指标集族，方便地编码为一个集的单映射E → B。作为一个数据类型构造函数，E→B通常被称为容器[1，2，3，4，5，7];然后B被认为是一组形状，纤维Eb是在形状对应于b。 要插入到这些位置的数据可以可以是任何类型X：多项式函子接收一个类型X（一个集合），并返回新的更精细的类型XEb。多态函数对应于自然多项式函子的变换，这些可以根据仅表示集合E→B，参见[1]，[18]，和下面的2.6。一个基本的例子Σ是列表函子，X<$→n∈N Xn，其与集合X关联列表集合X中的元素。 这里n∈N是形状，n表示n元集{0，1，. . . ，n-1}的位置。多项式函子在类型论中还有另一个重要的用途：人们将E→B视为生成代数的签名，即多项式函子的初始代数。多项式函子的初始代数是归纳的数据类型，将数据集中到W-类型中（例如）Martin-Léoft类型[42]，[40]。类似地，终端余代数是余归纳数据类型（有时称为M-类型），通常被解释为程序或系统（例如参见[43]，[23]）。1.2 物种和解析函子。一个函子是有限的，当它保持ω-滤除余极限。对于多项式函子，这等价于E→B有有限纤维。设Bω表示有限集和双射的广群。一个物种[26]是一个函子F：Bω→Set，写作S<$→F[S];集合F[S]可以被认为是可以放在集合S上的F-结构的集合。F的扩张是闭函子设置−→设置（2）[n]×XnX−→n∈NAut（n）它是F沿（非完全）包含Bω-集的左Kan扩张。这种形式的函子称为解析函子[27]。Joyal建立了一个等价的类和解析函子之间的范畴，并将解析函子表征为保持共滤极限和弱回调的有限函子[27]，参见[24]和[6]。有限多项式函子是严格保持回调的解析函子。就物种而言，它们对应于那些对称群作用是自由的物种。种中的幺半群（在替换运算下，对应于解析函子的合成）精确地是运算。许多重要的多项式函子都具有单子结构。例如，列表函子有一个J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351353∆自然单子结构的串联列表。多项式单子配备了一个Carnummonad映射到列表单子是一样的非对称操作数[37]。更一般地说，有限多项式单子对应于投影运算[32]（即，每一个人，都有自己的归宿。1.3 多变量多项式函子。在[18]之后，多项式是集合sptI<$−E−→B−→J，（3）而相关的多项式函子（或多项式的扩张）由复合函数给出。Set/I−→ 设置ΠpΣ/E−→Set/B−→设置/J、（四）其中，Sfs是沿s的拉回，Slp是拉回的右伴随（称为依赖积），Sdt是拉回的左伴随（称为依赖和）。 对于映射f：B→A，我们有三个显式公式：f（Xa|a ∈ A）=（Xf（b）|b ∈ B）（5）Σ（Y b）|b ∈ B）=（b∈BaQ（Y b）|b∈B）=（b∈Ba黄蓝|a ∈ A）（6）黄蓝|a∈ A），（7）共给出以下公式（4）Σ（X i）|i ∈ I）−→（YXs（e）|j ∈ J），b∈Bje∈Eb当I=J= 1时，其专门化为（1多变量多项式函子对应于索引容器[7]，它们的初始代数有时被称为一般树类型[41，Ch.16]。从伴随的抽象描述中，可以得出多项式函子的概念（以及大多数理论）在任何局部Carnival闭范畴中都是有意义的，多项式函子是此类范畴切片之间最自然的函子类。它们被内在地刻画为局部的右伴随[31]1.4 简化对称性。容器是一种严格的数据结构：它不允许数据以任何方式在给定形状的位置之间进行排列。在许多情况下，希望允许置换，以便某些位置-一个形状内的点变得难以区分。在量子物理学中，不可区分粒子的原理在基本水平S不354J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351上强加了这种对称性。一个基本的例子是多集数据类型，它的扩展是函子ΣX›→Xn，（8）n∈NAut（n）J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351355它是解析的但不是多项式的。为了解释这种具有对称性的数据类型，Abbott等人[5]（也参见Gylterud [22]）通过“手动”添加对称性扩展了容器形式主义：对于每个形状（B中的元素b），现在有一组纤维E b的对称性，插入到相应位置的数据通过这个组动作被 不难看出（参见）。也[6]），在有限的情况下，这正是物种和解析函子的概念事实上，物种应该是数据类型理论的一个很好的框架已经有一段时间了（例如[14]，最近[12]，[47]）本文的论点是，群胚上的多项式函子提供了一个清晰的统一框架：在群胚的设定中，“解析”和“多项式”之间的本质区别消失了从物种的角度来看，这种升级还有其他原因。事实上，组合学家很快就意识到，1985年的解析函子的概念对于枚举的目的来说并不是最优的：基数并不能产生枚举组合学的核心指数生成函数（如果解析函子是多项式，则会这样。）事实上，《物种书》[11]根本没有提到解析函子。这个问题由Baez和Dolan [9]整理出来：问题是，从同伦理论的观点来看，（2）中的群作用是一个坏商，并且在基数方面表现不好。为了得到正确的基数，必须使用同伦基数，结果不再是一个集合而是一个广群，基数必须是同伦基数。因此，有必要从群胚而不是集合开始工作。贝兹和多兰在群胚引入了物种（3.6），称它们为填充类型，证明同伦基数给出了正确的生成函数，并通过展示量子谐振子的组合描述所需的类型是填充类型而不是经典物种来说明更广泛的普遍性的有用性[9]。与David Gepner的共同工作通过观察到在群胚上，种/解析函子与离散有限多项式函子是同一回事（3.7），从而结束了这个循环;因此多项式的简洁形式为（商）容器和种提供了一个自然的统一框架。2广群上的多项式函子广群是所有箭头都可逆的范畴一个有用的直觉，目前的目的是，groupoid是从正确的同伦观点来看，群胚的行为非常像集合。我们感兴趣的是群胚直到等价，由于这个原因，许多熟悉的1-范畴概念，如拉回和纤维，是不合适的，因为它们不是不变的under等价。好的概念是相应的同伦概念，356J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351✻我们简要回顾一下。它们都可以从Joyal [28，29]为了将范畴理论推广到拟范畴（Lurie [38]称为∞-范畴）而发展的美丽的单纯机制中推导出来。 由于群胚的2-范畴Grpd具有只有可逆的2-胞腔，它是一个准范畴的例子。 从现在开始当我们比如说2-范畴，我们的意思是2.1 切片。如果I是广群，则同伦片Grpd/I是以I为基的射影锥的2-范畴（参见：[28]）：它的对象是映射X→I;它的箭头是带2-胞元的和2-箭头是图表X轴✻✻⇒✻我X轴z，Y✟✟✟，中国5岁，✻✻✻⇒⇒✟✟✟你好，我与结构三角形交换。更一般地，如果d：T→Grpd是任何图，则存在以d为基的2-范畴投射锥Grpd/d。2-范畴C中的同伦终结对象是对象t，使得对于任何其他对象x，广群C（x，t）是可收缩的，即等价于点。更一般的同伦极限可以用同伦片来定义：函子d：T→Grpd的同伦极限定义为同伦片Grpd/d中的同伦终端对象。同伦极限是唯一的等价。2.2 拉回和纤维。给定一个由实线箭头表示的群胚X、Y、S的X×SY，zY布吕格Xfz，S同伦拉回是同伦极限，即，作为在所讨论的形状的立体图上的投影锥的某个切片2-范畴中的同伦终端对象给出，并且因此它被唯一地确定直到等价。一个特定的模型是广群X×SY，其对象是三元组（x，y，φ），x∈X，y∈Y，φ：fx→gy是S的一个箭头，且它们的箭头是成对的（α，β）：（x，y，φ）→（x′，y′，φ′）由α：x→x′和β：y→y′Y中的箭头，使得下图在SFXφz，gyf（α）fx，'φg（β），zgy，′.(One应该注意，如果f或g是纤维化，则朴素集合论拉回等价于同伦拉回。）′J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351357B中的对象b上的态射p：E→B的同伦纤维Eb是p沿着包含映射1pb'，z B的同伦拉回Eb❴1，pb，zEp，zB，.(Note同伦纤维Eb一般不是E的子群胚，尽管映射Eb→E总是忠实的。但同样，如果p是纤维化，则集合论纤维等价于同伦纤维。）2.3 同伦等价物。 当群G作用在集合或广群X上时， 同伦商X/G是通过对每个g∈G在x和y之间的路径（即箭头）中粘合而获得的广群，使得gx=y。更正式地说，它是预层G→Grpd的Grothendieck构造的全空间，它是同伦上极限的一个特例（符号X//G）经常使用[9]。如果G作用在点广群1上，则1/G是具有一个对象和顶点群G的广群。若p：X→B是群胚的态射，则对b∈B，但Aut（b）正则地作用在Xb上，同伦商Xb/Aut（b）恰好提供了缺失的箭头，从而使自然映射Xb/Aut（b）→X完全忠实。由于每个对象x∈X必须映射到B的某个连通分支，我们发现等价ΣX轴b∈π0BXb/Aut（b）=：b∈BXb，（9）将X表示为纤维的同伦和，或者等价地表示为群胚的族（以π0（B）为索引，并且每个群胚中具有群作用给定态射pf对于群胚Y→B→A，我们有下面的b∈BYba∈A黄蓝这实际上是“相关和”函子的公式Grpd/A由postcomposition给出在族记法中，公式如下：b∈Ba（Y b）|b∈B）=（Yb|a ∈ A），正如在Set情况下的公式（6）。沿f的拉回：B→A，记为f，是f的右伴随。 这当然意味着同伦伴随，相当于映射Gr pd/A（Y，X）<$Gr pd/B（Y，X）的自然等价。这一前提是基于回调的唯一属性人们可能会注意到以下回调公式，在家庭符号：f（Xa|a ∈ A）=（Xf（b）|b ∈ B），358J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351再次完全类似于Set情况（公式（5））。广群的2-范畴是局部Carnival闭的。这就意味着，在这种情况下，所有的缓冲区都有一个如下的连接：Gr pd/B→Gr pd/A。对于Mua，Mu a的映射是一个等价的;对于Y→B，如果Yovera∈A，则Mu a的fi可显式地表示为映射广群（Ba，Y）a= GrpdB（Ba，Y）.（在下面的离散情况下，将推导出更明确的公式。）2.4 多项式函子。多项式是群胚sptI←− E −→ B −→ J。相关的多项式函子（或多项式的扩展）作为复合函数给出。一级 −n→s Grpd布吕普/E−→Grpd/B −t→tGrpd/J.2.5 Beck-Che valle y，di s t ribut i v i t y，and c om p os it i o n.给我一个homomo otopypullback square·ψ，z·❴✤α β·ϕz， ·函子之间存在自然等价α通常称为贝克-谢瓦利条件。该理论的一个更微妙的特征是分配性，在这种情况下，它是一个等价物，说明如何在相关和上分配相关乘积（并且可以解释为选择公理的类型论形式[39]）。 我们在这里不需要细节。 见[18]的经典案例，和韦伯[46]的更深入的处理。Beck-Chevalley2.6 自然变化。正如在经典情况[18]中一样，多项式函子（在一个变量中）的同伦Cartesian自然变换P′P精确地对应于同伦Cartesian图E′，zB′❴E，zB，.J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351359这是贝克-谢瓦利的一个简单结果。更一般地证明了任意自然变换本质上是由图唯一给出的E，′，zB′·z，B′❴、Ez，B是一个有点复杂，并依赖于一个同伦版本的米田引理。(At在写这篇文章的时候，这个结果不像[18]的一维情况那样精确。）2.7 跨度和材料运算符。群胚的跨距是群胚多项式的特殊情况，其中中间映射是单位映射（或等价映射）。这些构成了矩阵代数的一个分类，被Baez和Dolan称为填充算子 [9];它们被用来给出Hecke代数和Hall代数的某些方面的广群模型[10]。3组合多项式函子;正合[21]中的下列结果实际上是在更丰富的背景下证明的：∞-广群，但证明也适用于1-广群。我们现在压制笨拙的定理3.1（Gepner-Kock [21].） 一个函子Grpd/I → Grpd/J是多项式的当且仅当它是可达的并且保持锥极限。所谓圆锥极限，我们指的是有一个终端顶点的图上的极限。回想一下，函子是可访问的[38，CH。[5]当它对某些正则基数κ保持κ-滤余极限时。这里的正则基数的特征是明确的：p命题3.2（[21]）由I←E →E →J给出的多项式函子保持κ-滤余极限当且仅当p有κ-紧纤维。一个重要的例子是κ=ω。一个广群是ω-紧的，当它有许多分支时（即，π0（X）是一个有限集），所有的顶点群都是有限的.3.3离散性。对于实际中出现的许多数据类型（包括物种和下面的所有示例），尽管它们可能具有对称性，但每个形状中的位置形成离散广群，即广群等价于集合。在多项式形式中，这相当于具有离散纤维的中间映射p：E→B。在这种情况下，相关乘积公式简化为Y（pY）b=e∈π0（Eb）是的，360J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351ωωω类似于（7），因此所有公式看起来完全类似于集合的情况。相应的精确性条件是保持筛选的共极限。一个κ-筛选上极限是一个图D上的上极限，其对角线D→DS对每个基数<为κ的集合S都是共尾的[38，Ch.5]。p命题3.4（[21]）由I←E →E →J给出的多项式函子保持κ-筛余极限当且仅当p有κ-紧离散纤维。3.5 组合多项式函子我们称一个多项式函子I←pE→B→J组合，如果p的纤维等价于有限集（即，是ω-紧离散）。3.6 群胚（groupoid）（stuff types）Baez-Dolan填充型 [9]是群胚F→Bω的映射。我们更喜欢在群胚中使用物种这个名字。（一个经典的物种是当地图有离散的纤维，或者等价地是忠实的。它的延拓是n<$→Fn沿Bω<$Grpd的左同伦Kan延拓：Grpd −→GrpdΣX−→n∈π0（Bω）=NFn×Xn.Aut（n）(That’s a homotopy quotient of这个函子是多项式[21]：表示广群映射是回调Ez，F❴B，′z，B.ωω这个映射有有限离散纤维，因为B′→Bω有。 (HereB′是广群（有穷有穷）。 相反，给定一个群胚多项式E→F，离散纤维，有限离散纤维化）产生群胚中的物种。 可以检查多项式的扩展与物种的扩展一致最后总结：命题3.7（[21]）组合多项式函子Grpd → Grpd与解析函子是一样的（在Baez-Dolan的意义上）。结合这些结果，我们得到一个推论3.8（[21]）函子Grpd → Grpd是解析的（在Baez- Dolan意义下）当且仅当它保持ω-筛余极限和锥极限。3.9 广义物种。多项式函子和[15]的广义种类之间的关系已经由甘比诺和作者（未发表）概述。一个广义的物种依赖于两个类别I和J，并且具有作为前-张力是广义解析函子PrSh（I）→PrSh（J）;这推广了1985年的概念，但不是贝兹-多兰的概念。如果I和J是群胚，则这些群-广义的解析函子对应于组合多项式在群胚上的J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351361ωωωωω3.10 例子. 群 胚多项式在群胚中编码数据类型。对于前-例如，B′→Bω编码多集数据类型：有限集的广群Bω而双射是形状的广群--多重集的形状实际上是集合索引它的元素，而不仅仅是它的大小。有N个同构类，同构应解释为命题相等.S∈Bω上的纤维是S中位置的离散广群，即统一的职位规定，由S索引的多集。事实上，由于B′→Bω是纤维化，因此纤维是正则的。与集合S本身相同-注意它的自然Aut（S）-作用。 离散性这意味着位置之间的命题相等可以被视为定义相等。这个商容器的扩张自然是一个内函子Grpd→Grpd。但我们得到一个内函子Set→Set（在这种情况精确地（8））通过与自然包含集→Grpd和后-使用π0：Grpd→Set合成。 第一种是无害的。 第二个对应把所有的同构分解为同一性，即将命题平等解释为定义平等。如果参数是一个集合，唯一的坍缩是从同伦商到朴素商（集合上的作用）的传递。循环表的数据类型是群胚多项式，用C′→Cω表示，其中Cω是有限循环序集的广群，C′是广群循环有序有限集的集合从1.1开始，列表数据类型由N′→N表示，解释为线性有序有限集的群胚和点同上。群胚的图N′，zN❴C，′，zC，❴B，′z，B，ωω现在表示从列表到循环列表再到多重集的Caribbean自然变换或多态函数。4树木Martin-L？ofyypeypeycoresponon omial函子的iialalgbra（[40][17][18][19][ 1 +P的初始代数也可以描述为P上的自由单子的运算集合，而自由单子又是P-树的集合。P-树（P是集合或任何lccc上的多项式函子抽象树，另一方面，承认对称性，所以它们不是任何集合多项式函子P的P-树，它们既不是经典意义上的W-类型也不是容器。相反，根据[32]，抽象树本身是多项式函子。用下面的树的特征来定义是方便的：✤ω362J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351ω4.1 树（[32]）（有限）树是有限集合的图sptA←−M −→N −→A满足以下三个条件：(1) t是单射的(2) s是具有单元素补的单射（称为根，记为1）。当A= 1 +M时，通过1›→ 1定义走到根函数σ：A→A，e<$→t（p（e）），其中e∈M.(3)<$x∈A：<$k∈N：σk（x）= 1。A的元素称为边。 N的元素称为节点。 对于b∈N，边t（b）称为节点的输出边t是单射的意思是每条边最多是一个节点的输出边。对于b∈N，元素Σb的输入边称为b的输入边。 因此，整个集合M=b∈NMb可以被认为是具有标记输入边缘的节点的集合，即，对（b，e），其中b是节点，e是b的输入边。maps返回标记的边。条件(2)说每个边都是唯一节点的输入边，除了根边。条件（3）说，如果你向根走，在有限的步骤，你到达那里。不在t的图像中的边称为叶子。4.2 装饰树：P-树（[32];参见[33，34，35]）编码和操纵树的装饰的有效方法是根据多项式内函子。设P是由I给出的多项式内函子图DQ←E →BC→I. P树是一个A MZuz，N❴z，A（十）我，我，、、、Ez，Bz，I，上面一行是树正方形在同构之前是可交换的，重要的是将2-胞室指定为结构的一部分。展开定义，我们看到P-树是一棵树，它的边用I装饰，它的节点用B装饰，并且具有等价Mn<$Eb的附加结构对于每个带有装饰b∈B的节点n∈N（这本质上只是一个双射，因为纤维是离散的），在边m∈Mn的装饰和相应的d（e）之间的I中的iso，最后在输出的装饰之间的In和c的边（b）。4.3 P树的例子自然数是单位单子P（X）=X的P-树，也是列表单子的运算集合。平面有限树是列表单子P的P-树，并且也是自由非随机操作单子的操作的集合[37]。这两个例子是第一个条目归纳数据类型的规范序列的几种方法，以更高的范畴理论，opetopes：opetopes在维度n是P-树P一个集多项式函子，其操作是（n-1）opetopes [35];因此opetopes是高维的树抽象有限树是多集函子1<$B′→Bω→ 1的P-树，但J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351363不能实现为P-树的任何集合多项式P。4.4 树木的费曼图表。在 的 所谓BPHZ 在微扰量子场论的重整化中，人们关注1-粒子不可约（1 PI）费曼图的嵌套，即没有单个边缘移除断开。Kreimer [36]发现BPHZ过程被编码在（非平面）根树的Hopf代数中，表示图的嵌套。第二章：第三节：在图中，中间的组合树表示左边的1 PI子图的嵌套;这样的树在Kreimer的BPHZ的霍普夫代数方法中是足够的，但不捕获图的对称性。为此，树中需要进一步装饰，如右侧部分所示。首先，树中的每个节点都应该由它在嵌套中对应的1PI图装饰，其次，树应该有对应于图的顶点的叶子（输入槽）。装饰树应该被看作是一个配方，通过插入装饰图到父节点的图的顶点重建图。边上的数字表示每个替换的类型约束：图的外部接口必须匹配它被替换到的顶点但是树装饰的类型限制不足以重建图，因为例如小图可以将左侧节点的装饰替换到图的各种不同顶点中。在[34]中找到的解决方案是考虑P-树，对于P，多项式endo-spt由I←E→B→I给出的函子，其中I是相互作用标签的广群，理论（在这种情况下，单顶点图B是该理论的连通1PI图的广群，E是具有标记顶点的1PI图的广群。映射s返回标记处的单顶点子图，p忘记标记，t返回图的外部接口，即通过将所有东西收缩到一个点而获得的图，但保留外部线。因此，P-树是一个类似于（10）的图，具有指定的2-胞元.这些2-细胞携带大部分结构：例如，右边的2-cell表示装饰给定节点的1 PI图必须具有与节点的输出边的装饰相同的轮廓-或者更准确地说，更现实地说：指定同构（它是单顶点图的外部线之间的双射）。类似地，左侧的2单元格指定对于每个带标记入边的节点x′∈M，一个顶点图装饰该边，图的标记顶点装饰标记节点x′。因此，P-树的结构不仅是一个完整的配方，哪些图应该被替换成哪些顶点，而且如何：333333 3233364J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351判定双射规定了哪些外部线应当与接收图中的哪些线相标识。事实上，在嵌套图和P-树之间存在群胚的等价性[34]。这是利用在[16]建立代数恒等式有关图解释为同伦基数的等价群的装饰树。注意多项式函子P是组合的，因为每个图都有一个离散的有限顶点集。但它不是经典意义上的物种：分类映射B→Bω将一个图发送到它的顶点集，由于一个图可能有固定每个顶点的非平凡自同构，这个映射没有离散纤维。5观一个2-范畴被称为局部卡图闭的，当对每一个箭头f：B → A，我们都有一个连接f的连续环或一个连接f的连续环. 这是一个基本的结构，它包含了Beck-Chevalley等价性和分配性，这是最小的要求多项式函子的合理理论强度理论几乎可以从[18]一字不差地照搬过来，而且[18]的表示定理似乎也延续了下来。虽然局部carry闭范畴为Martin-Léoftypetheory[44]，[13]的扩展版本提供了语义，并且局部carry闭范畴捕获了一些2-截断版本（[25]，[19]），但最近对同伦类型的理论强有力地表明，从长远来看，∞-广群和其他局部Carnival闭∞-范畴的情况将是类型论的真正内容。多项式函子的∞-理论的大部分，以及理论的各个方面面向同伦型理论的局部Carnival闭∞-范畴已经在与大卫·盖普纳的联合工作中完成，并将在其他地方出现[21]，[20]。尽管如此，广群的情况本身就很有趣，因为它已经涵盖了重要的应用：特别是对于组合性质的许多目的，1-广群是处理对称性问题所需要的时间会告诉我们，为了程序语义的目的，也足够了-否则它是进入∞-世界的一个很好的垫脚石。引用[1] Abbott，M.，“集装箱的类别”，博士。论文，莱斯特大学，2003年。 购自http：//www. mcs. 勒河AC. 英国/~ma 139/do cs/t h esis. PD F.[2] Abbott，M.，T. Altenkirch和N. Ghani，容器的类别，在：软件科学和计算结构，计算讲义Sci. 第2620（2003）号来文，第2620（2003）页。23比38[3] Abbott，M.，T. Altenkirch和N. Ghani，Containers：Constructing Strictly Positive Types，Theoretical. Comput. Sci. 342（2005），pp. 3-27号。[4] Abbott，M.，T. Altenkirch，N. Ghani和C. McBride，容器的衍生物，在：类型lambda演算和应用程序（瓦伦西亚，2003年），计算讲义。Sci. 第2701（2003）号来文，第2701（2003）页。16-30[5] Abbott，M.，T. Altenkirch，N. Ghani和C. McBride，用商类型构造多态程序，在：程序构造的数学，计算机讲义。Sci. 第3125（2004）号来文，第3125（2004）页。2比15J. Kock/Electronic Notes in Theoretical Computer Science 286（2012）351365[6] 你好，J。 和J。 Vele bil，Analyticfuctorsandwekpulbacks，TheoryAppl. Cate g. 21（2008），pp.191-209.[7] Altenkirch ， T. 和 P. Morris ， Indexed containers ， in ： Proceedings of the Twenty-Fourth AnnualIEEE Symposium on Logic in Computer Science（LICS 2009）（2009），pp. 277-285。[8] Awodey，S.， N. Gambino和K. Sojakova，同伦类型理论中的归纳类型，预印本，ArXiv：1201.3898。[9] Baez，J. C.和J. Dolan，从有限集到费曼图，在：B. Engquist和W. Schmid，editors，Mathematicsunlimited-2001 and beyond（2001），pp. 29-50. ArXiv：math.QA/0004133.[10] 贝兹，J.C.，A. E. Hoffnung和C. D.沃克，高维代数VII：群化，理论应用分类。24（2010），pp.489-553. ArXiv：0908.4305。[11]Bergeron，F.，G. Labelle和P.Leroux，[12] Carette，J. and G. Uszkay，Species：Making Analytic Functors Practical for Functional Programming（2008），可从http：//www. 卡湾mcmaster. 我的意思是，我的意思是，[13] C lairambault， P.和P.Dybjer， Thebie euivalenceofflocalycarrtesiann closedcategoriesanddMartinn-Loftype theories，preprint，ArXiv：1112.3456.[14] Fiore，M.，计算和组合结构的数学模型（邀请演讲），收录于：软件科学和计算结构的基础，计算机课程讲义。Sci. 第3441（2005）号来文，第3441（2005）页。25比46[15] Fiore，M.，N. Gambino，M. Hyland和G. Winskel，广义结构种的笛卡尔闭双范畴，J. Lond。（2）77（2008），pp.203-220.[16] G'alvee z-Carrillo ， I. ，J.KockandA.Tonk s ， GropoidsandFa`diBr unor mulaeforen functionsinbialgebras of trees，preprint，ArXiv：1207.6404.[17]Gambino，N.和M. Hyland，Wellfounded trees and dependent polynomial functors，in：S。贝拉尔迪，M. Coppo和F. Damiani，editors，TYPES 2003，Lecture Notes in Comput. Sci. 第3085（2004）号来文，第308页。210- 225[18] Gambino，N.和J.Kock，Polynomial functors and polynomial monads，出现在Math.Proc.CambridgePhilos.Soc.，ArXiv：0906.4931。[19] 加纳河，类型论的二维模型，数学。结构。Comput. Sci. 19（2009），pp.687-736 ArXiv：0808.2122。[20] Gepner，D.和j.Kock，Univalence in localized carbohydrate closed∞-categories，预印本，ArXiv：1208.1749。[21] Gepner，D.和j.Kock，Polynomial functors over infinity categories，in preparation.[22] 吉尔特鲁德， H、对称容器，硕士 论文， 大学 的 奥斯陆，2011. 购自http：//www. 朵你好。没有/20 1 1/1 4 46 1 7/这是科学研究。p d f.[23] Hancock，P.和A.Setzer，依赖类型理论中的交互式程序，在：计算机科学逻辑（Fischbachau，2000年），计算机讲义。Sci. 1862（2000），pp.317-331,[24] 长谷川河，解析函子的两个应用，定理。Comput. Sci. 272（2002），pp.113-175[25] Hofmann，M.和T. Streicher，类型理论的群胚解释，在：25年的建设性类型理论，牛津逻辑指南36，牛津大学出版社，1998年，页。83-111[26] 我是A， 如果你不想让我的朋友们为你做点什么，我会告诉你的。 MATH。 42（1981），pp. 1- 8 2.[27] 我 也 是 ，一 、Foncteurs一 个 简 单 的 问 题etesp`ecesDe这是 一 个 很 好 的 例 子 ，in ：Commbinnatoireenumérative（Monttréréal/Quéebec，1985），Lecture Notes inMathematic s 1234，Spri nger，1986，pp. 126-159.[28] Joyal，A.，拟范畴和Kan复形，J. Pure Appl. Alg. 175（2002），pp. 207-222[29] Joyal，A.，“准范畴理论”，高等数学单纯形方法高级课程，卷。 我，Quadern s，num。 45（2008），pp. 147- 4 9 7，C R M B a r c e l o n a。Availableathtt p：//mat. u a b. 45 - 2. p df.366J