广群模型的高阶归纳类型构造与消除规则及依赖类型理论的研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记336（2018）119-134www.elsevier.com/locate/entcs广群模型中的有限高阶归纳Peter Dybjer彼得·迪比耶1，2查尔姆斯理工瑞典哥德堡Hugo Moeneclaey3Ecolenormalesup'erieuredeParis-Saclay巴黎，法国摘要级别1（1-hit）的更高归纳类型仅具有点和路径的构造函数，而级别2（2-hit）的更高归纳类型也具有曲面的构造函数。我们把注意力限制在更高的归纳类型，并提出了一般图式的类型，其点，路径和表面的构造。我们还从1-命中和2-命中的构造函数类型中推导出了消除和相等规则此外，我们构造了具有2-命中的依赖类型理论的广群模型，并指出通过截断广群模型，我们得到了具有1-命中的依赖类型理论的集模型关键词：直觉类型论，单位类型，同伦类型论，高阶归纳类型，setoids，groupoid1介绍[14]的Martin-Lé提出了一般的恒等式I（A，a，AJ），其要点是证明a和AJ是A的等价元素.由于A可以是任何类型，甚至是单位类型，我们可以将这个类型形式化，并得到一个无穷大的更高的单位类型A，I（A，a，aJ），I（I（A，a，aJ），p，pJ），I（I（I（A，a，aJ），p，pJ），θ，θJ），等等。在外延类型论[15，16]中，这个层次崩溃了，因为它有一个规则强制I（A，a，aJ）最多有一个元素。然而，在内涵类型理论中并非如此[14，17]。正如Hofmann和Streicher[12]所示，它有一个模型，1第一位作者得到了瑞典研究委员会（Vetens kapsrandomadet） 的 部 分 支 持 ， 该 委 员 会 批 准 了 《 证 明和 程 序 的 类 型 》 。2电子邮件：peterd@chalmers.se3电子邮件：hmoenecl@ens-paris-saclay.frhttps://doi.org/10.1016/j.entcs.2018.03.0191571-0661/© 2018作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。120P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119广群模型，其中I（A，a，aJ）可以有多个元素。事实上，后来证明内涵类型理论在Kan中有无限维模型。单纯集[25]和Kan三次集[2]，支持有趣的新公理，如Voevodsky在Bauer、Lumsdaine、Schulman和Warren的意义上，更高的归纳类型（hit）是一种所有迭代的身份类型都是归纳生成的类型。高阶归纳类型在同伦类型理论中占据中心地位，其中单位类型的塔被赋予拓扑解释：上面的a和aJ是空间中的点，p和pJ是从a到aJ的路径，θ和θJ是p和pJ之间的同伦（或曲面），等等。某些空间，如区间、圆、球面、环面等。虽然高级归纳类型背后的思想很简单，但仍然缺乏对其语法和语义的全面描述。有工作的范畴语义[13，24]和语义的一些例子在立方集[3]。然而，这两部著作都没有回答什么是高级归纳类型我们引用霍特的书[22，第179页]：在本书中，我们并不试图给出什么构成“高级归纳定义”以及如何从这样一个定义中提取排除规则的一般公式相反，我们将依靠一些一般性的非正式讨论和许多例子。因此，我们想知道命中的构造函数的类型一般是什么样的我们还想提供一个模型，它显示了更高归纳类型的一般理论的一致性。事实上，它们的基础地位如何，它们与马丁-洛夫的意义解释[ 15，16 ]的关系如何通过将高级归纳类型的含义简化为标准归纳类型或归纳递归类型，可以在没有高级归纳类型的类型论中对具有高级归纳类型的类型论进行建模吗？因此，我们的目标是建立一个类似于归纳族理论[5，4]和归纳递归定义理论[8，9，10]的高级归纳类型的一般理论。在本文中，我们采取了一个步骤实现这一目标，限制自己的最简单的命中，1命中只有点和路径的建设者和2命中可能有表面建设者太多。此外，我们将自己限制在fentinary这样的构造函数在某种意义上，将在下面作出精确我们提出了一般图式的引进规则，并从引进规则的消除和平等的规则派生的方法。1-hits的模式可以在setoid模型中解释，其中类型被解释为setoid（具有等价关系的集合）。类似地，我们在群胚模型中解释我们的2-hit模式，其中类型是群胚（所有箭头都是同构的类别）。文件计划在第2节中，我们给出了一个1-命中的例子，其中点是组合项，路径是两个组合项是可转换的证明。我们还将这个1-hit的解释描绘为setoid。这里的目的是强调P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119121BJf（x）=f（x）.p1-hits与方程理论的密切联系。在第3节中，我们首先回顾归纳类型和归纳定义的二元关系的一般模式。虽然这些图式允许无限分支树的广义归纳定义（例如W型的元素），但我们解释了为什么我们在这里将注意力限制在由无限归纳定义给出的1-命中上。我们提出了这样的类型的引入规则的架构在第4节中，我们回顾了2-hit如何表示环面。在第5节中，我们提出了一个2-命中的扩展模式。我们还讨论了在HotTT书中的命中是由我们的模式覆盖，哪些不是。在第6节中，我们展示了如何将2-hit建模为群胚。由于空间的原因，我们不单独呈现1-hits的相反，groupoid模型以这样一种方式呈现，即setoid模型可以被视为groupoid模型的截断版本。在第七节中，我们提到了一些相关的工作和进一步研究的建议。2组合逻辑作为一次命中我们首先介绍依赖类型理论的一个小片段，依赖函数类型写为（x：A）→B（x），非依赖函数写为A→B。标识类型写为a=AaJ而不是I（A，a，aJ）。对于这个理论，我们补充说，一击CL的规则及其形成规则、得分引入规则和路径、消除和相等规则。我们使用“数学”符号f（x）用于函数应用，f（x，y）用于f（x）（y）等。此外，x 1：A 1，.，x n：A nA表示A是上下文中的类型x1：A1，.，x n：A n. 如果x：AC是依赖于变量x的类型（或项），我们经常（但不总是）使用符号C（x）来强调这种依赖性，并且也写C（a）来表示在C中用a替换x的结果。标识类型的引入规则是：（x：A）→x=Ax对于任何类型的A。消除规则和相等规则（Paulin[21]）是JC： （x：A）→C（x，req（x））→（y：A）→（z：x=Ay）→C（y，z）JC（x，d，x，req（x））=d其中x：A，y：A，z：x=Ay<$C（y，z）。等式推理的通常规则（传递性、对称性、对等替换）可以从这些规则中推导出来规则我们还将推导出异构身份类型a=BaJ的规则，它让我们比较元素a：B（x）和aJ：B（xJ），其中p：x=AxJ，但B（x）和B（xJ）不一定在定义上（判断上）相等。另一个可推导的规则是函数f：（x：A）→B（x）必须保持恒等式：apdf：（p：x= AxJ）→p2.1组合逻辑作为一次命中的规则形成规则指出CL是一个类型。引入规则分为两部分：点构造函数K， S：CL和app：CL→ CL→ CL的类型和路径构造函数（用于组合转换）的类型122P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119Kconv（x，y）Kconv：（x，y：CL）→app（app（K，x），y）=CLxSconv：（x，y，z：CL）→app（app（app（S，x），y），z）=CL app（app（x，z），app（y，z））组合转换的其他规则（反射性、传递性、对称性、应用保持相等）来自=CL是单位类型的事实CL的消元规则表示如何定义函数f：（x：CL）→C（x）通过点和路径构造函数的结构归纳（表明它preser veside nti ty）。该规则具有asumptionsK：C（K），S：C（S），app：（x：CL）→C（x）→（y：CL）→C（y）→C（app（x，y）），并且Kconv：（x，y：CL）→（x：C（x））→（y：C（y））→app（app（K，x）， app（K，K，x，x），y，y）=CxSconv：（x，y，z：CL）→（x：C（x））→（y：C（y））→（z：C（z））→a pp（app（app（S，x），y）， app（app（S，x）， a p p（S，S，x，x），y，y），z，z）CSconv（x，y，z）平等规则是a pp（app（x，z）， app（x，x，z，z），app（y，z），app（y，y，z，z））f（K）=Kf（S）=Sf（app（x，y））=app（x，f（x），y， f（y））apdf（Kconv（x，y））=Kconv（x，y，f（x）， f（y））apdf（Sconv（x，y，z））=Sconv（x，y，z，f（x）， f（y）， f（z））2.2Setoid模型上面的理论，依赖类型理论，（x：A）→B（x），a=AaJ，CL，有一个setoid模型[11]。在这个模型中，类型被解释为setoid A，一个集合A0和一个等价关系R。 这里我们把等价关系表示为二元集合族（A1（x，XJ））x，x′∈A0，如果A1（x，XJ）是唯一的，则R（x，XJ）成立，否则为空. 此外，两个setoid A= （ A0 ， A1 ） 和B = （ B0 ， B1 ） 之间 的setoid 映射 是一 个函 数 f0 ：A0→B0，并证明它保持等价关系：f1：（A1（x，XJ））→ B1（f（x），f（XJ））.有两个原因，这种代表性。虽然我们通常使用集合论作为我们模型构造的元语言，但我们推测该构造可以在扩展类型论中进行，其中等价关系将由类型族实现。(Cf Hofmann和Streicher但是，还有另一个优点：然后，可以将setoid模型看作groupoid模型的截断版本。一个广群的对象集合A0与满集A1（x，XJ）一起形成一个setoid。 在下文中，我们将不区分A1族和它所代表的等价关系R。(We也注意到可拓类型论在经典集合论中有一个直接的解释[4]，所以类型论符号可以被理解为抽象集合论。关于用族构造范畴的细节，参见Moeneclaey[18]。=P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119123[6]支持依赖函数类型、内涵标识类型和CL的setoid和setoid映射在这里，我们将类型CL解释为setoid（CL0， CL1），其中CL0是由K， S和app生成的归纳类型，CL1是由Kconv和Sconv以及用于传递性，自反性，对称性和保持相等的构造函数生成的归纳族[5，4]3一次命中的模式现在我们问自己，点和路径的引入规则一般是什么样的。我们还构建了一个setoid模型，这样一个一般的概念，1击中。如上所述，我们正在寻找一个符合归纳族模式风格的模式[5，4]。显然，第一个尝试是尽可能接近该模式，并规定命中的点构造函数的类型可以与归纳类型的构造函数的类型具有相同的形式;命中的路径构造函数的类型可以与归纳类型的构造函数的类型具有相同的形式。 二元归纳法归纳类型H的构造函数的类型的一般形式是（x1：A1）→· · ·→（xm：Am（x1，... x m−1））→（B1（x1，.，x m）→ H）→· · ·→（B n（x1，.，x m）→H）→H其中A1是类型，...，A m（x1，.，x m−1）是一个类型，如果（x1：A1，.，xm−1：A m−1（x1，...，x m−2）），和B1（x1，.，x m），.，B n（x1，.，x m）是类型，如果x1：A1，.，x m：A m（x1，...，x m−1），并且所有这些判断在没有H的规则的情况下在理论中都是真的。所以Ai和Bj不依赖于H。这个一般形式是通过将归纳族[5，4]的模式专门化到归纳类型的情况而得到的。我们注意到Bj实际上可以是任何类型p的序列。我们称xi：Ai为非归纳前提（或边条件），dyj：Bj（x1，...，xn）→ H是一个归纳前提。 如果Bj是所有j的空序列，那么我们有一个普通的或无限的归纳定义，否则我们有一个广义的归纳定义。注意，这只是W型构造函数类型的温和推广[15]，它是通过设置m=n= 1获得的。事实上，在外延类型论中，任何具有上述形式构造函数的归纳类型都等价于W-类型。这是关于严格正归纳类型编码为W-类型的更一般定理的特殊情况[7]。然而，在对击中H的广义归纳定义的setoid解释中出现了一个复杂的问题例如，假设H有一个点构造函数c0：（B→H）→H，并且它由点集H0和族来解释。的路径集H1（x，y），其中x，y∈H0.因为函数必须保持等价性关系，我们期望H0的解释构造函数的类型为c00：（f∈B0→H0）→（（x，XJ∈B0）→B1（x，XJ）→H1（f（x），f（XJ）→H0（注意，这是元语言中的一种类型，我们使用“∈”而不是“：“表示集合/类型成员资格。）由于H1将被解释为一个归纳族，我们得出结论，H 0和H1同时由一个归纳-归纳族定义。124P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119..定义。然而，我们不想使元理论复杂化--毕竟归纳-归纳定义的理论是复杂的[20，19]。出于这个原因，我们在这里选择限制在更简单的情况下，即仍然覆盖HotTT书[22]中的大多数命中，见5.3节。正如读者将看到的，无限2-命中理论已经相当复杂，我们认为最好把广义归纳定义的额外复杂性留给将来的工作。3.1点构造函数对于有限命中，点构造函数的类型的一般形式是c 0：（x1：A1）→···→（x m：A m（x1，.， x m−1））→ H →···→ H → H其中A1是一个类型，... . ，以及Am（x1，.，x m−1）是一个类型，如果x1：A1，.，xm−1：A m−1（x1，...，x m−2），所有这些判断在没有H的规则的情况下在理论中都是真的。3.2路径构造函数的模式有限命中的路径构造函数类型的一般形式是：c 1：（x1：B1）→· · ·→（x n：B n（x1，.，x n））→（y1：H）→···→（yn′：H）→p1（x1， . ，xn，y1， . ，yn′）=Hq1（x1， . ，xn，y1， . ，yn′）.→pn′′（x1， . ，xn，y1， . ，yn′）=Hqn″（x1， . ，xn，y1， . ，yn′）→pJ（x1， . ，xn，y1， . ，yn′）=HqJ（x1， . ，xn，y1， . ，yn′）其中H和=H都不能出现在Bi中。此外，条款p1（x1， . . . ，xn，y1， . ，yn′），q1（x1， . ，xn，y1， . ，yn′），. 、pn′′（x1， . ，xn，y1， . ，yn′），qn′′（x1， . ，xn，y1， . ，yn′），pJ（x1， . ，xn，y1， . ，yn′），qJ（x1， . ，xn，y1， . ，yn′）是根据以下语法构建的点构造函数模式p：：= y|c 0（a1，.，a m，p1，...， p k）其中y：H是在y 1中的变量a， . ，yn′，其中pj：H是pi nt构造器模式，并且其中x1：B1，.，xn：B n（x1，.，xn）A i：A i（a1，...，a i−1）是不使用任何H规则的项。注意，如果我们删除路径构造函数c 1的类型的第二行，该模式看起来完全像二元无穷归纳族的构造函数模式[5]（除了当前模式只允许点构造函数模式，而不允许pj的一般类型）。 然而，我们不知道H是否能出现在边条件Bj中。不幸的是，它不能以任意的方式出现P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119125zc1（x，y，z）因为H的负出现可能导致矛盾。因此，我们简单地禁止H出现在Bj中，并有一个形式为yk：H的单独的前提列表3.3点和路径构造函数的简化形式为了简化消元规则和等式规则的表示，我们只列出了一个点构造函数m= 1（单侧条件）和一个归纳前提的特殊情况c0：A→H →H和一个路径构造器，其中n=nJ=nJJ= 1：c1：（x：B）→（y：H）→p（x，y）=Hq（x，y）→pJ（x，y）=HqJ（x，y）我们强调，这种简化只是一种表述方式。将这种简化的形式推广到普通命中的构造函数的一般形式是例行的，但很冗长。(The一般形式当然是必要的，以获得有趣的命中。）3.4消除和平等规则消元规则表达了如何通过点和路径上的结构归纳来定义函数f：（x：H）→C（x）（表明函数保持恒等式）。更具体地说，鉴于c ≠0：（x：A）→（y：H）→C（y）→C（c0（x，y））c1：（x：B）→（y：H）→（y：C（y））→（z：p=Hq）→T0（p）=CT0（q）→T0（pJ）=CT0（qJ）其中T0（p）：C（p）是p：H的提升（定义如下），我们可以定义f为：f（c0（x，y））= c <$0（x，y，f（y））apdf（c1（x，y，z））= c <$1（x，y，f（y），x，apdf（z））请注意，第二个等式是一个定义等式，而不仅仅是一个比例等式，就像在HotTT书[22]中一样。这个定义上的相等性将由下面的广群模型验证。3.5提升功能我们用T 0（p）：C（p）表示点构造函数模式p：H的其思想是T0（p）将等于f（p），但后者尚未定义。例如，在方程中的两个构造器模式的提升为K_convT0（app（app（K，x），y））=a pp（app（K，x）， app（K，K，x，x），y，y）T0（x） =xCL的提升函数定义为yT0（x）=x，T0（y）=y，T0（K）=K，T0（S）=S，T0（app（t，TJ））=ap p（t，T0（t），TJ，T0（TJ））在一般（简化）模式中，T0（p（x，y））：C（p（x，y））的定义如下：关于点构造函数模式p（x，y）的形式的归纳：126P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119θ路径路径1Fp2=冲浪T0（y） =yT0（c0（a，p））= c <$0（a，p，T0（p））因此，x：B，y：H，y=C（y）≠T0（p（x，y））：C（p（x，y））和T0（p）（x，y，f（y））=f（p（x，y））。因此，上面的apdf（c1（x，y，z））的方程是良好类型的。我们建议读者参考Moeneclaey[18]关于1-hits模式的setoid模型，并再次指出它是通过截断群胚模型而产生的。4作为2-Hit我们现在将考虑除了点和路径构造器之外还具有曲面构造器的2-命中一个例子是下面的命中，它将环面T2表示为CW-复合体[22]。它有四个构造函数：基础：T2路径1：base =T2base路径2：base=T2 base冲浪：路径1路径2=基本=T2基本路径2路径1为了说明它的消除原理，我们将利用层次2的异质性。Leta，AJ：A，p，pJ：a=AaJ，θ：p=a=Aa′ pJ，b：B（a），bJ：B（aJ），q：b=BbJ，qJ：b=BbJ. 我们写pp′q=b=B b′qJ对于路径q，q，J的异构身份。我们现在可以证明函数通过恒等式消去保持二级恒等式。如果f：（x：A）→C（x），则2Jf（x）=Cf（x′）Japdf：（θ：p=x=Ax′p）→apdf（p）=θapdf（p）现在我们可以用公式表示T2的消去法则.假设x：T2<$C（x），P2b：C（碱），p21：P2b=C1b，p2 also，s：pJb=C◦JP注意异构路径的组合则存在函数f：（x：T2）→C（x）使得f（base）=bapdf（path1）=p1apdf（path2）=p2apd2（surf）=s最后一个方程是使用定义等式apdf（p<$q）很好地类型化的。 =apdf（p）≠apdf（q），这在广群模型中是成立的 这些等式（和21P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119127对于异构逆，类似的）是我们的模式是良好类型的所必需的128P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119CG5有限2-命中的一个模式5.1曲面构造器的模式现在我们将给出2-命中的一般模式。点和路径构造函数的形式与1-hits相同曲面构造函数的简化形式是c2：（x：D）→（y：H）→（z：p3（x，y）=Hq3（x，y））→g1（x，y，z）=p4（x，y）=Hq4（x，y）h1（x，y，z）→g2（x，y，z）=p5（x，y）=Hq5（x，y）h2（x，y，z）(In一般形式的四个前提x：D，y：H，z：p3=Hq3，ZJ：g1=p4=Hq4h1成为四个有限的（可能是空的）前提序列。Cf的一般形式3.1中的点构造函数和3.2中的路径构造函数） 这里D是正确的类型在没有H规则的理论中，H， =H和==H都不可能出现在其中.此外，在对点构造函数c0的H-形成和H-引入的理论中，x：D，y：H和p3，q3，p4，q4，p5，q5：H都是点构造函数模式（由c0的变量建立），g1，h1，g2，h2是由以下文法建立的路径构造函数模式g：：= z |c 1（a，p，g）|格沃格|ID |g−1其中z：p3=Hq3是路径变量，x：Da：B是不使用H规则构建的项，p：H是假设下的点构造器模式 x：D，y：H。每个路径构造器模式都带有一些定义等式，这些等式在广群模型中有效增加第四个“违约”也是很自然的构造函数”ap c0 （对应于中的点构造函数的箭头部分）模型）到用于路径构造器模式的语法。然而，在广群模型中检查apc0的解释需要很长的计算，我们还没有完成。5.2消除和平等规则消元规则表达了如何通过归纳法定义函数f：（x：H）→C（x），对于点、路径和曲面构造函数中的每一个都有一种情况。为此，我们假设我们有阶跃函数c0和c1，如1-命中的消除规则中那样，此外还有用于表面构造器的阶跃函数c=2：（x：D）→（y：H）→（y=C（y））→（z：p3=Hq3）→（z：T0（p3）=zT0（q3））→（t：g1=p4=Hq4h1）T0（p4）=HT0（q4）T0（p5）=HT0（q5）→T1（g1）=tT1（h1）→T1（g2）=c2（x，y，z，t）T1（h2）提升T1（g）：T0（p）=C路径构造器模式g：p=Hq的T0（q）是以类似于点构造器模式的提升T0（p）的方式定义：T1（z） =zT1（c1（x，y，g））= c <$1（x，y，T0（y），g，T1（g））P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119129T1（ggJ）= T1（g）JT1（gJ）T1（id）= idT1（g−1） = T1（g）−1′其中p−1′表示路径p的逆。f的等式规则是：f（c0（x，y））= c <$0（x，y，f（y））apdf（c1（x，y，z））= c <$1（x，y，f（y），z，apdf（z））apd2（c2（x，y，z，t））= c2（x，y，f（y），z，apdf（z），t，apd2（t））f f请注意，所有三个等式规则都是定义等式，在群胚模型中有效。最后一个方程的类型检查与第二个方程的原因相似（见3.5节我们通过路径构造模式的归纳证明，T1（g）（x，y，f（y），z，apdf（z））=apdf（g（x，y，z））. 这个证明使用了定义等式a pdf（p<$q） =a pdf（p）<$Ja pdf（q）和da pdf（p−1） =a pdf（p）−1′，其中ch在群胚模型中有效。即使没有这些等式，等式两边的类型也是同构的。因此，可以在任何地方添加合适的同构，但会出现一些相干问题5.3在HotT-书中的点击数HotTT书中的许多命中都是我们一般句法模式的实例。例如，区间、圆、命题截断、悬置和推出都是我们的1-命中模式的实例。2-球面、环面、0-截断和集商是我们的2-命中模式的实例。然而，使用中心和辐条[22，p192]的环面的替代定义不是我们的1-hits模式的实例，因为它打破了在路径构造器类型的索引（端点）中只允许点构造器模式的要求。此外，0-截断的另一种定义[22，p199]使用了广义归纳，并且也没有被我们的模式所覆盖62-命中模式的广群模型我们建立在Hofmann和Streicher就像霍夫曼和斯特雷彻，我们工作在集合论的元语言，但猜想该模型也可以进行扩展类型理论。为了说明为什么是这种情况，我们将以类型论的风格来写我们的定义，并使用扩展类型论有一个集合论模型的事实，见g[4]。一个广群H（在类型论风格中，参见setoids表示的讨论）是一个元组（H0，H1， H2，n， id，（-）1， tran， re， sym， w0， w1，α，λ，p，ι0，ι1），其中H0是ob∈ H的集合，H1（a，AJ）a，a′∈H0 是从a到AJ的连续流的集合，H2（f，FJ）f，f′∈H1（a，a′）是连续流f和FJ 的等式的集合. More-over，n，id，（−）1分别表示复合、恒等式和逆运算。130P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119JF选项。其余的分量证明了箭头相等是一个同余关系（w0， w1），它满足结合性（α）、恒等式（λ，ρ）和逆律（ι0，ι1）。当映射到一个广群时，我们通常忽略所有的分量，除了前三个分量：H =（H0， H1， H2）。集合论中通常的群胚概念可以通过定义hom-set为同分元素H1（a，AJ）/R（a，AJ）来恢复，其中R（a，AJ）是由H2生成的a和AJ之间的箭头的等价关系。此外，当我们使用集合论方法时，为了简单起见，我们将确定箭头相等的所有证明，θ，θJ∈H2（f，FJ）有θ = θJ.我们称这种独特的元素为“”。这种表示不仅为广群的类型论实现铺平了道路模型，但也为扩展我们的工作的解释3-命中在一个弱2-广群模型。在群胚模型中，一个类型族x：AC（x）被解释为从群胚A到群胚范畴我们让C0表示该函子的对象部分，使得C0（x）对于x∈A0是广群，C1表示箭头部分，使得C1（f）：C0（x）→C0（XJ）是f∈A1（x，XJ）迁移函子进一步，我们用符号C1J（x，XJ，f，y，YJ）表示f∈A1（x，XJ）， y∈C0（x），YJ∈C0（XJ）.对于不同纤维中的点之间的异质路径的集合（由transprt介导）。 当f，FJ∈A1（x，XJ）， θ∈A2（f，FJ）， z∈C（x），ZJ∈C（xj）， g∈C1 j（z，zj，f），gj ∈C1J（z，ZJ， fj）时，记为C2 j（f，fj，θ，z，ZJ， g ， gj）.异质路径g，g的新的相等性（由传输介导）。一个功能-f：A→B被解释为群胚之间的函子F。它表示类型-理论上由一个三元组（F0，F1，F2）表示对象，箭头，并证明保持平等的箭头部分。类似地，函数x：Af（x）：C（x）被解释为源广群和纤维广群族之间的我们参考Hofmann和Streicher [12]的解释细节。请注意，我们也证明了apf和ap2的定义计算规则，而在HotTT书中，有一个关于导致这些模型的非正式讨论计算规则仅为命题等式下面的群胚模型捕捉了到达同伦的路径的结构。例如，我们可以证明在这个模型中，击中T2可以由它的基本群胚1（T2）来解释（即同构于Z<$Z）。然而，广群模型并没有捕捉到更高维度的结构例如，尽管2-球面是2-命中，但广群模型并不能在维度上捕捉其非平凡结构2. 类似地，虽然我们可以表明圆S1可以用y=1（S1）y=Z来解释，在广群模型中，它在setoid模型中是微不足道的6.1形成规律回想一下上面示意图2-hit的点和路径构造器的类型：c0：A→H →Hc1：（x：B）→（y：H）→p=Hq→pJ=HqJc 2：（x：D）→（y：H）→（z：p3= Hq3）→g1= p4=Hq4 h1→g2= p5=Hq5 H2P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119131设类型A由群胚（A0，A1，A2）解释，B由群胚（B0，B1，B2）解释，D由群胚（D0，D1，D2）解释。此外，p被解释为依赖函子（p0，p1，p2）（参见广群上下文中的术语模型，参见Hofmann-Streicher或Ruch），由对象、箭头和保留相等部分组成对于PJ，QJ，p3，q3，p4，q4，p5，q5也是如此。g1，h1，g2，h2的解释也是依赖函子.我们把示意击中H解释为归纳生成的广群（H0，H1，H2），它的构造子将保证2-击中理论中的点、路和面构造子的类型被解释为广群之间适当关键的观察是，这样得到的所有构造子都有类型，这些类型是有限归纳族的构造子的类型的一般形式的实例[5]。因此，我们猜想，2-hits的群胚模型可以在一个扩展了这些无穷归纳族的模式的• H是由点构造函数的对象部分的构造函数归纳生成的c00∈A0→ H0→ H0使用c00，项p0（x，y）∈H0，其中x∈B0且y∈H0，可以通过对点构造器模式p的结构的归纳来定义：y0（x，y）=y（c0（s，t））0（x，y）= c00（s0（x），t0（x，y））其中s0由假设s是A型项，其中H不出现，而t0由归纳假设提供•H1是由以下方式感应产生的：· 路径构造函数对象部分的构造函数c10∈（x∈B0）→（y∈H0）→H1（p0（x，y），q0（x，y））→H1（pj0（x，y），Q0J（x，y））· 点构造函数的箭头部分的构造函数：c01∈（x，XJ∈A0）→A1（x，XJ）→（y，YJ∈H0）→H1（y，yJ）→H1（c00（x，y），c00（xJ，yJ））· 构造器的组成，身份，和逆的路径n ∈（x，y，z∈H0）→H1（x，y）→H1（y，z）→H1（x，z）id∈（x∈H0）→H1（x，x）（−）−1∈（x，y∈H0）→H1（x，y）→H1（y，x）对于点构造子模式p和x，XJ∈B0，y，YJ∈H0，ex∈B1（x，XJ），ey∈H1（y，YJ）我们定义p1（ex，ey）∈H1（p0（x，y），p0（XJ，YJ））为：y1（ex，ey）=ey（c0（s，t））1（ex，ey）=c01（s0（x），s0（XJ），s1（ex），t0（x，y），t0（XJ，YJ），t1（ex，ey））其中s1来自s是群胚映射的事实，t1来自归纳假设。132P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）1190类似地，对于g，一个从p到q的路径构造模式，x∈D0，y∈H0，z∈H1（（p3）0（x，y），（q3）0（x，y）），我们定义g0（x，y，z）∈H1（p0（x，y），q0（x，y）），z0（x，y，z）=zc1（s，t，gJ）0（x，y，z） =c10（s0（x），t0（x，y），g0J（x，y，z））其中s是一个项，t是一个点构造函数模式和g0J被省略了。通过感应。恒等式、合成式和逆方程•H2（表示路径相等）由下式感应生成：· 表面构造函数c20∈（x∈D0）→（y∈H0）→（z∈H1（（p3）0，（q3）0））→H2（（p4）0，（q4）0，（g1）0，（h1）0）→H2（（p5）0，（q5）0，（g2）0，（h2）0）· 路径构造函数的箭头部分：c11∈（x，XJ∈B0）→（ex∈B1（x，XJ））→（y，YJ∈H0）→（ey∈H1（y，YJ））→（z∈H1（p0（x，y），q0（x，y）→（ZJ∈H1（p0（XJ，YJ），q0（XJ，YJ）→H2（p0（x，y），q0（xJ，yJ），z<$q1（ex，ey），p1（ex，ey）<$zJ）→H2（pJ0（x，y），q0J（xJ，yJ），c10（x，y，z）<$q1J（ex，ey），p1J（ex，ey）<$c10（xJ，yJ，zJ））· 点构造函数的曲面（保持箭头相等）部分：c02∈（x，xJ∈A0）→（ex，exJ∈A1（x，xJ））→A2（x，xJ，g，gJ）→（y，YJ∈H0）→（ey，EYJ∈H1（y，YJ））→H2（y，YJ，ey，EYJ）→H2（c00（x，y），c00（xJ，yJ），c01（x，xJ，ex，y，yJ，ey），c01（x，xJ，exJ，y，yJ，eyJ））· 点构造函数的函子定律：cid∈（x∈A0）→（y∈H0）→H2（c00（x，y），c00（x，y），c01（x，x，idx，y，y， idy），idcc<$0∈（x，xJ，xJJ∈A0）→（ex∈A1（x，xJ））→（exJ∈A1（xJ，xJj））→（y，YJ，YJJ∈H0）→（ey∈H1（y，YJ））→（EYJ∈H1（YJ，YJJ））→H2（c00（x，y），c00（xJJ，yJJ），c01（x，xJ，ex，y，yJ，ey）=c01（xJ，xJJ，exJ，yJ，yJJ，eyJ），c01（x，xJJ，exXJ，y，yJJ，eyxeyJ））· 证明H2是一族等价关系：tran∈（x，y：H0）→（u，v，w：H1（x，y））→H2（u，v）→H2（v，w）→H2（u，w）re∈（x，y∈H0）→（u∈H1（x，y））→H2（u，u）sym∈（x，y∈H0）→（u，v∈H1（x，y））→H2（u，v）→H2（v，u）· 证明复合保持相等：w0∈（x，00P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119133y，z∈H0）→（u，v∈H1（x，y））→（w∈H1（y，z））→H2（u，v）→H2（u<$w，v<$w）w1∈（x，y，z∈H0）→（u，v∈H1（y，z））→（w∈H1（x，y））→H2（u，v）→H2（w<$u，w<$v）· 群胚定律的见证者：（x，y））134P. Dybjer，H.Moeneclaey/Electronic Notes in Theoretical Computer Science 336（2018）119A∈（x0，x1，x2，x3∈H0）→（u∈H1（x0，x1））→（v∈H1（x1，x2））→（w∈H1（x2，x3））→H2（（u<$v）w，u<$（v<$w））λ∈（x，y∈H0）→（u∈H1（x，y））→H2（u，idx<$u）ρ∈（x，y∈H0）→（u∈H1（x，y））→H2（u，u∈y）ι0∈（x，y∈H0）→（u∈H1（x，y））→H2（u<$u−1，idx）ι1∈（x，y∈H0）→（u