弱ω-广群胚的正则性及其相等性证明

可在www.sciencedirect.com在线获取理论计算机科学电子笔记308（2014）229-244www.elsevier.com/locate/entcs用参数理论研究弱ω-广群律的正则性马克·拉森INRIA Paris-Rocquencourt，PiR2，Univ Paris Diderot，Sorbonne ParisCité F-78153 Le Chesnay法国摘要我们证明了从类型的ω-广群结构证明广群律的项在命题上都是相等的。我们的证明减少了这个问题的唯一性的典范点在第n圈空间，并得出结论，使用Bernardy关键词：类型论，参数性，圈空间，群胚，单位类型1介绍由单叶基础程序[8]提出的弱ω-广群的综合方法是这样一种思想，即（同伦）型理论应该是导出空间、点、路、同伦的原始按照这种方法，空间由类型表示，点由居民表示，路径由点之间的等式（也称为单位类型）表示，这些对象的代数性质不应该先验地（例如通过公理），而应该直接从语言中导出。为了证明综合方法的合理性，人们应该证明每个定义的规范性，在这个意义上，不应该通过选择一个定义的特定实现而不是另一个来做出重要的选择。Garner，van den Berg [9]和Lumsdsaine [5]分别证明了在类型论中，每个类型都可以具有弱ω-群胚的结构。为此，他们证明了马丁-洛夫类型理论的一个最小片段，其中单位类型是唯一允许的类型构造子，具有弱ω-范畴结构。在形式上，这些结果陈述了将弱ω-广群的代数性质表示为类型的可能性，并且在每种情况下找到这些类型的典型居民，反映了该性质成立的事实的恒等式、倒置和连接1电子邮件：marc. inria.frhttp://dx.doi.org/10.1016/j.entcs.2014.10.0131571-0661/© 2014 Elsevier B. V.保留所有权利。230M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229►∀∀∀→来处理身份类型a=b（1）A. B. C.D. C. D这个翻译可以扩展：a=b→要成为谓词的类型路径、结合性、反演对合、2-路径的水平和垂直合成规范证人的广群法律在这里意味着有一个路径之间的任何两个居民的法律证明他们的平等，而且这条道路应该是规范的：应该有一个路径之间的任何两个路径之间的两个居民的同一法律，等等.这个正典性在片段中已经是一个已知的事实。本文的主要结果是将正则性推广到整个Martin-Löf型理论。在这项工作中，我们遵循Brunerie [3]启发的句法方法来形式化广群律的概念。我们称广群律为任何闭类型Γ.c，使得Γ. c：Type在极小片段中可导，并且使得上下文Γ是可收缩的。可收缩上下文是以下形状的上下文：A：类型，a：A，x1：C1，y1：M1=x1，...，xn：Cn，yn：Mn=xn其中xi不出现在Mi中。这些上下文的形状通过路径归纳是稳定的，它允许通过连续的路径归纳找到任何广群律的居民。我们表明，这个居民是典型的，即使在片段之外证明的主要思想是利用连续路径归纳法将给定广群律的唯一性问题归结为参数环空间中唯一的标准点的唯一性问题。给定一个基类型A和一个点a：A，第n个循环空间及其典范点归纳定义为：Ω0（A，a）：=AΩn+1（A，a）：= Ωn（a=a， 1a）ω0（A，a）：=aωn+1（A，a）：=ωn（a=a， 1a）其中1a：a=a表示反射率。因此，对于任何整数n，X：Type，x：X。Ωn（X，x）是一个群胚律，满足λX：Type，x：X.ωn（X，x）（注意，使用一个论域，可以内在化n上的量化;无论是否使用，我们在这里陈述的一切都将为真）。我们称这个广群律为n次参数循环空间.第0个参数循环空间，是多态型X：X型X的单位函数，它的典型居民是λX：类型，x：X.x，即。身份功能。这一术语是唯一一个达到居住在其类型中的功能外延的术语。证明这类性质的标准工具是使用Alfred系统F）。它指的是这样一个概念，即良好类型的程序不能检查类型;它们必须对抽象类型保持一致的行为。Reynolds通过证明多态程序满足由类型结构归纳法定义的所谓逻辑关系来Bernardy等人[2]将该工具扩展到依赖类型系统。它提供了术语、类型和上下文的统一翻译，保留了类型（所谓的抽象定理）。在它的一元版本中，这是这项工作唯一需要的，逻辑关系是通过关联到任何良构的typeA：类型 a谓词A：A→类型和任何居民M：A一个证人λp：a=b.p（<$a））=<$b）其中p是谓词生成器沿着p的第一个transm）运动M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229231C∈M由A和B的共同类型表示。然后，很容易（尽管相当冗长）找到标识类型的引入和消除规则的翻译，以及检查这些翻译是否保留计算规则。这允许将Bernardy的抽象定理扩展到身份类型。使用这个框架，我们能够推广的唯一性性质的多态单位类型的任何参数循环空间。证明过程中的循环空间的索引上进行归纳，并使用代数性质的运输。论文概要在第2节中，我们介绍了本文中使用的类型理论设置。第三节证明了Bernardy在第4节中，我们使用这个平移来证明loop空间的正则性结果;我们证明了参数loop空间的所有居民在命题上是相等的（定理4.3）。在第5节中，我们引入了类型论的MLID片断来定义广群律的概念，并证明了第4节的结果可以推广到所有广群律（定理5.6）。最后，第6节专门讨论各种问题。2语法的表示为了重用文[2]中提出的parametricity理论，我们给出了一个接近纯类型系统语法的带有单位元类型和论域的Martin-Löf类型理论[1].在这个框架中，计算规则以无类型的方式处理，并使用为扩展构造演算引入的Luo累积关系实现论域的子类型化读者可能更习惯于类型论的判断性陈述，其中每个计算步骤都被检查为良好类型。这仅仅是一个表述的问题;这里提出的所有材料都可以不经过太多的调整来适应使用判断等式的类型系统。此外，使用累积并不是真的需要，但使我们的结果更一般，更接近实现，如coq。系统的术语由以下语法给出：A、B、C、M、N、U、V：=X|（男/女）|λx：A.M|A.B.| Typei|1M|J = x：C，y：M = x.A（B，U，V）|J∀x:C,y:M=x.A(B, U, V)其中类型i的宇宙由iN索引。变量被认为是α-转换，我们写M[N/x]来表示通过将M中x的所有自由出现替换为N而获得的项。为了便于阅读，我们允许自己省略一些类型注释，当它们可以从上下文中猜测出来时（特别是M=N，1M和J（B，U，V）将在本文中经常使用）。术语的语法是通过在纯类型系统的语法中添加以下内容获得的：• 类型构造器M=AN，用于形成标识类型，• 单位类型的引入规则，1C，证明反射率M=CM，232M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229M···∀∀►• 消除规则（也称为给定依赖于点x和从基点M到x的路径y的任何依赖类型A（x，y），给定A（M，1M）的见证（归纳的基本情况），给定点U和路径V，路径归纳提供A（U，V）的居住者。这个路径归纳的公式，由于Paulin-Möhring（也称为基于路径归纳），等价于另一个版本，其中A由两个点和它们之间的路径参数化我们使用符号来表示术语之间的语法相等（直到α转换）。项之间的转换记为M <$βN，它被定义为包含通常的β-约化（λx：A.M）N <$βM [N/x]和单位元类型的计算规则J<$x：c，y：M=x，Δ.P（N，M，1C）<$βN的最小同余。 而累积序被定义为最小的偏序“与β相容并满足i ≤ j：A1，.， x n：A n. 类型i“x1：A1，.， x n：A n. j型就像在扩展的构造演算中，累积性规则对于函数的定义域不是完全逆变的（AJ 上下文是x1：A1形式的有限列表，，xn：An映射变量的类型。类型系统的规则如图1所示。由于我们遵循标准路线，我们不详细发展系统的元理论路径归纳的非依赖版本称为传输，并定义为通过Px：C.X（M）Jx：C，y：U=x.X（M，V，P）其中y不出现在X中。它经常被用来在类型族之间进行强制：给定一个类型族X：C→Typei，两点U，V：C之间的路径P：U=V，以及X U中的一个项M，M沿着P的迁移P<$x：C.X（M）存在于XV中。它满足以下可导出规则：Γ，x：C<$X：类型jΓ<$P：U=CVΓ<$M：X[U/x]ΓP<$x：C.X（M）：X[V/x]运输港当可以从上下文中猜到类型家族时，我们有时也会省略它。计算规则告诉我们，沿反射面传输等于什么也不做：1U<$（M）<$βM。3将关系参数性扩展到标识类型在这一节中，我们解释如何将Bernardy的参数性转换扩展到原始单位类型。然后我们证明了这种扩张保持了类型性（定理3.2）.这里是翻译的定义为纯语法M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229233⟨⟩►►►∀►► ∀ ►►J► ∀M►<$<$）<$）<$Type）<$λx：Type.x→Typeiii（10）R100R（）（）（）（Ⅲ）（）（）C∈<$CM=M）<$）¢）C¢1CMWFwf-eMPTyΓwfΓB：类型ir，x：BwfWFΓwfI型：I型+1UnIVΓwf（x：A）∈Γ x：AVaRI aBLESr，x：AM：BΓλx：A.M：x：A.B一个bstr ac tionΓM：x：A.BΓ护士：一Γ（M N）：B[N/x]应用程序ΓM：AJΓA：类型iAA AΓM：ACO nveRSIO nΓA：类型iΓ，x：AB：类型iΓx：A.B：类型i产品ΓM：CΓN：CΓC：类型iΓM：CΓM=CN：类型iΓ1C：M=CM我和你rM：C自反性中文（简体）Γ，x：C，y：M=x<$P：类型iΓ<$B：P[M/x，1M/y]P（B，U，V）：P[U/x，V/y]PaTH-InFig. 1.类型理论与身份类型（MLTT）V：M=U类型系统：（A.B）λf：λx：A. B。A，x R：x∈A）。（f x）∈<$B）λx：A.Mλx：A，x R：x∈A . M（M）N（N）其中M A只是代表A M的符号（它使公式更容易阅读）。如引言中所述，由单位类型M=CN生成的谓词由M=CN上的类型族定义，选择传输到N（M）M=CN：M=CN→类型M=CN<$λp：M=CN.p<$x：C.x∈C（M）=C NN多亏了计算法则x：c.x∈C）M∈<$M=CM）<$β1M<$（<$M））=M∈<$C）<$M）<$β<$M）=M∈<$C）<$M）翻译M∈C）M）：1C反射率的C是反射率：1 M（M）1：1234M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229. 最后，消除规则被转换为嵌套路径-M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229235（1）（2）（3））（Ⅲ）(iii) 如果M“M j，则<$M）“j <$M）。（）（）（）（）（）（）（）（）（）（）（M）（Ⅲ）（）（）Q此外，如果Γwf，则Γ wf（c）诱导：J=x：C，y：M=x.P（B，U，V）J∈x R：U∈C，y R：V∈（M）=x R. J∈x：C，y：M=x.P（B，U，V）∈P[U/x，V/y]（J=x：C，y：M=x. J<$x：C，y：M=x.P（B，x，y）∈P[y<$（M）/xR，1y<$（M））/yR]（B，U，V）路径归纳谓词的翻译相当冗长，使翻译难以阅读。然而，如果我们忽略注释，我们看到翻译J（B，U，V）J（J（B，U，V），U，V）仅仅是路径归纳的复制，应该与抽象和应用中的复制相比较我们可以检查这个翻译在替换和转换方面表现良好：引理3.1（替换和转换引理）我们有：(i)M[N/x]≡ M[N/x，N/xR]，(ii) 若M <$βMJ，则<$M）<$β<$MJ）。证据（i）的证明是M上的一个常规归纳证明。（三）是（二）的一个相当直接的结果。为了证明（ii），我们在这里只做了Bernardy翻译中没有的唯一检查C c CJ（N，M，1 M）（J（N，M， 1M），M， 1M）[J（J（<$N），M，1C），<$M），1M∈<$C））M<$βJ（<$N），<$M），1M∈<$C）（M）（N）现在我们可以检查这个扩展是否保留了类型：定理3.2（抽象）若Γ<$M：A，则.ΓM：A（a）<$r）<$M）：M∈<$A）（b）是的。通过对推导的归纳，给出了抽象定理. 以每份ch计证明命题（a）是简单的。由于对其他规则的处理现在是标准的，我们在这里只处理关于身份类型的规则。尽管我们在这里没有详细说明，但对coversion的处理使用了前面的引理。• 归纳假设：归纳假设给我们 Γ► M：M ∈ C（1）、 Γ ►<$N）：N∈<$C）（2）和<$r），x：C<$x ∈ <$C）：类型i（3）。 使用TRANSANS端口，236M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229（）（（M））CC（10）M=U（10）（5）（V∈M=U）（Ⅲ）（2）（）（）（）（）（）（）r，p：M=CN到由（1）和（3）导出：<$r），p：M=CN<$p<$λx：C.x∈C（<$M））：N∈<$C）。（M）（M）而对于（<$r），x：C，y：M=x1y（<$M））：y（<$M））=y（<$M）），它们很容易被M∈C然后利用（2）我们建立了一个推导，p<$λx：C.x∈C（M）=N ∈ CN，最后得出了具有bstr的Γ<$MN→Type i.=CN）：M=C• 自反性：通过归纳论证，我们得到：M∈C）（1）。使用(1) 我们可以检验出<$r）<$1M∈<$C）：<$M）=<$，它可转换为MMM.<$r）=1M∈ <$C）：1C（<$M））=M∈ <$C）<$M）。因此，我们得出<$r）<$<$1C）：1C∈<$C）• （b）的归纳假设是：Γ► M：M ∈ C（1）Γ，x：C，y：M=x≠ P：P→类型i（2）（3）（4）（5）（6）（7）（8）（9）（10和（a）的归纳假设是：Γ，x：C，y：M=x<$P：类型i（7）<$r）βB：P[M/x，1M/y]（8）<$r）βU：C（9）设T为下列项：J=x：C，y：M=x. J（B，x，y）∈P）[y（<$M））/xR，1y（<$M））/yR]（B，U， V）首先，我们必须通过证明ΓT：J（B，U，V）∈ P[y（M）/xR，1y（M）/yR，U/x，V/y]（U）这意味着，使用Pa-I-UCTIOn，检查：·谓词是格式良好的：Γ，x：C，y：M=x<$J（B，x，y）∈ P[y（M）/xR，1y（M）/yR]：类型这是通过使用下式的推导将xR和yR代入（2）中获得的：（C），x：C，y：M=x∈（C）从（1）导出，并通过应用替代推导。其中，x：C，y：M=x<$J（B，x，y）：P·论证是正确的：我们推导出M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229237<$r）<$B）：J（B，M，1M）∈<$P）[y<$（<$M））/xR，1y<$（<$M））/yR，M/x，1M/y]238M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229（1）（）（）（）（Ⅱ）（）（）（）（）（）（）（）（）（））（（Ⅲ）∗.∀→.通过使用计算规则注意到：J（B，M，1M）∈P[y（M）/xR，1y（M）/yR，M/x，1M/y]βB∈ P[M/x，M /xR，1M/y，1yR（M）/yR]因此，我们可以从（1）和（3）中得出结论。最后，我们必须检查目标点和路径是否正确。ΓU：C和 ΓV：M=U，由（9）和（10）给出。设K为下列项：J∈x R：U∈C，y R：V∈（M）=x R. J<$x：C，y：M=x.P（B，U，V）∈P[U/x，V/y]（T，U，V）我们现在要检查：ΓK：J<$x：C，y：M=x.P（B，U，V） P[U/x，V/y]使用PaTH-INDUCTIO n，我们必须证明：·谓词是格式良好的：Γ，x R：U∈C，yR：V（M）=xRJ<$x：C，y：M=x.P（B，U，V）∈ P[U/x，V/y]：类型i其通过使用（9）和（10）替换（2）中的x和y并通过ap-将Γ_（？）J_（？）x：C，y：M=x，P（B，U，V）：P[U/x，V/y]应用于代换导子.·参数是正确的：我们使用（*）来确定T和w使用（4），(5)用于类型检查 U和V（2）4参数loop空间本节的目的是证明定理4.3。 下面的引理是进行引理4.2中的主归纳所需要的。 证明术语在作为一种半正式的阅读文体，它们可以很容易地从散文中构建出来。然而，作为定理4.3的结果，这些项的精确形状并不重要。 在本节中，我们使用p。 q和p−1分别表示路径和逆的级联。引理4.1设P：A→Type是一个类型族，u：P a对于某个a：A，并假设我们有φ：x：A.P xa=x。 然后，对于所有p：a=a使得p∈（u）=u，我们有1= p。证据利用φa对p∈（u）=u的路的函子作用，得到了一条二维路φa（p∈（u））=φa（u），并利用输运的自然性（引理2.3.11），我们得到一条路径p<$（φa（u））=φa（u）. 左手边路径p<$（φ a（u））是在单位类型上的传输，因此我们有p（φ a（u））=φ a（u）p，因此φ a（u）。p=φa（u）。因此，我们通过φa（u）和对称性的抵消得出1 =p。Q下面是主要的归纳法，它使我们能够导出定理4.3：QM. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229239（Ⅲ）（Ⅲ）∈<$）→n））−→引理4.2设A，P，a，u和φ的 定 义 与前面引理相同。 那么对于所有的 n-维循环p：Ω n（A，a），型族Ωn（A，P，a，u）：Ωn（A，a）→类型满足：p：Ωn（A，a）。 Ωn（A，P，a，u）p→ωn（A，a）） =p.证据通过对n的归纳，基情形正好由φ证明。对于归纳步骤，我们需要证明p：Ωn+1（A，a）.pΩn+1（A，P，a，u）ωn+1（A，a）=p，可转换为：Ωp：Ωn（a=a，1）.p∈Ωn（a=a，λq：a=a.q<$（u）=u，1，1）→ωn（a=a，1）=p因此，我们可以通过提供一个证明来应用归纳假设，即：a.q<$（u）=u→1=q，由前面的引理给出。Q我们可以推断：定理4.3（循环空间的标准性） 如果M：A：类型，则a：A。Ωn（A，a）则有一项π使得<$π：<$A：Type，a：A.ω n（A，a）= M A a.证据 抽象定理给了我们一个证明 MA：Type，AR：A→类型，a：A，a R：A R a。（M A a）Ωn（A，AR，a，ar）通过用λx实例化AR：A.a=x，我们可以通过应用前面的引理得出结论。Q请注意，作为推论，证明π是唯一的，直到命题等式（等等）。如果我们有两个这样的证明π和πJ，那么（πA a）。（πJA a）−1的类型为ωn（A，a）=ωn（A，a），即Ωn+1（A，a）。因 此，通过应用前面的定理，我们得到了（πA a）的证明。（πJA a）−1=ω n+1（A，a）也是（πA a）。（πJA a）−1=1ω（A，a）.因此，我们得出（πA a）=（πJA a）。5广群律在本节中，我们首先描述前面的类型系统MLTT的片段MLID。这个子系统用于证明广群律。非正式地说，它是从MLTT中通过删除规则aBSTR ac tion，aPPLIC a tion和UnI- veRES并通过将有效序列限制在引言中定义的可收缩上下文在函数空间不存在的情况下，规则P_I_duction必须被加强，以便能够沿着不是上下文的最后一条路径进行路径归纳因此，我们需要扩展术语的语法在MLID中，具有以下形状的项：J=x：C，y：M=x，Δ.P（B，U，V，W−→），其中Δ是一个常数并且其中向量符号-W→表示元组（W1，.，Wn）的条款。图2中给出了类型规则。在形式上，上下文Γ被称为con-i。tractible如果Γcontr是可推导的;读者应该注意到，在MLID的推导中出现的所有上下文都是可推导的。 在打字规则中，我们写为Γ−W→：Δ表示r∈Wk[A1/y1，·· ·，Ak−1/yk−1]中k=1，···， n的合取：Ak当Δ的形状为y1：A1，···，yn：An时，此外，[W /Δ]表示迭代替换[W1/y1，·· ·，Wn[A1/y1，· · ·，An−1/yn−1]/yn]。240M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229M►►►M∀►M···M控制剂B：0型控制剂M：BA：0型，x：A控制我在它r，x：B，p：M=Bx控制公司简介I型：I型Γ-谷氨酰胺M：CΓ-πdM=CN：类型0[化]化合物1C：M=CM我和你Γcontr（x：A）∈Γ自反性ΓidM：AJΓidAJ：类型0AJAΓidx：A瓦里阿布勒Γ-谷氨酰胺M：CridM：A新的βΓ-α-U：CΓ，x：C，y：M=x，ΔIDP：0型Γ，Δ[M/x，1C/y]ΔIDB：P[M/x，1C/y]V：M=UΓπd−W→： ΔP（B，U，V，−W→） ：P[U/x，V/y，−W→/Δ]扩展型相位调制图二. 具有单位类型的类型论的最小片段MLID为了将MLID嵌入到MLTT中，我们根据以下转换将扩展路径归纳转换为正常路径归纳：J<$x：C，y：M=x，Δ.P（B，U，V，−W→）<$λ−→x：Δ。（J=x：C，y：M=x. P（λx：Δ[M/x，1C/y]. B，U，V）−→x）其中−→y：Δ意味着y1，，yn是在Δ中指定的变量，其中Δ、λΔ和（J−→x）分别表示迭代的产品、抽象和应用。阳离子。然后，可以直接检查扩展P-I推理是否是MLTT的可接受规则。在MLID中，群胚定律的特征在于可收缩的上下文和可导出的类型（图3包含了群胚定律的一些示例定义5.1[广群律]广群律是一个具有以下形状的项：Γ.C，使得ΓidC：0型。在“初始”可收缩上下文A：Type，a：A中唯一的广群律由于在这一节中我们不改变循环空间的基类型和基点，我们简单地用ω n（resp.Ωn）项ω n（A，a）（分别为Ωn（A，a））。使用这些符号，我们有：引理5.2如果A：类型，a：A_idT：类型0，则(i) 存在|不|∈ N使得T <$βΩ|不|、(ii) 而且，如果A：Type，a：A≠W：T，则W <$βω|不|.证据 我们通过归纳法来推导A：Type，a：A idT：Type0。我们注意到，只有两个可能的最后使用的规则是IDEnTIT y和vaRI aBLEM. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229241M| |≡≡ ≡≡refl：X：Type，x：X.x=xsym：X：Type，x：X.x=y→y=xconcat：X：Type，x：X，y：X.x=y→z：X.y=z→x=zasc：xx：x，y：X，p：x = y，z：X，q：y = z，t：X，r：z = t。concatXxz（ concatXxy p z q）tr= concatXxy pt（ concatXyz qt r）neutral：X：Type，x：X，y：X，p：x =y。（concatXx y p y（reflX y））=pidem：X：Type，x：X，y：X，p：x=y. symXy x（ symXx y p）=phorizontal：X：Type，x：X，y：X，p：x=y，p′：x=y.p=p′→z：X，q：x=z，q′：x=z.q=q′→concatXxy p z q=concatXxyp′zq′图3.第三章。具有规范居民别名的广群律的例子由于类型0并不存在于类型0中，因此不可能调用扩展的P_I_I_INSTRUCTION，也不可能调用conversion。(i) 在可变的情况下，我们必然有T A，因此我们可以得出结论，|不|=0。在这种情况下，T的形状为M=CN，通过归纳假设M<$βω|C|，Nβω|C|和CβΩ|C|.所以我们得出结论，|不|为|C|+1。(ii) 不失一般性（MLTT是归一化的），我们可以假设W是以正常的形式。我们通过推导A：Type，a：A的（嵌套）归纳来进行，我们处理每个可能的情况（IDENTITy和conversion显然是不可能的，因为T不可能是Type0）：• 变量：在这种情况下，我们必须有Wa和Ta。所以我们有|=0且W <$ω 0。|=0 and W ≡ ω0.• 自反性：在这种情况下，W和T是形状1C的自反性，M=CM。 通过归纳假设，我们有M <$βω|C|. 因此|不|为C+1和Wβω|C|+1。• 这实际上是一个不可能的情况。我们将得到J=x：C，y：M=x，Δ.P（B，U，V，-→Z）的W，并通过归纳得到结论，我们就有Mβω|C|βU和Vβ ω|C|+1。因此V是一个自反性，W不是正规形式。Q前面的引理允许我们找到由下式给出的任何可收缩上下文的规范实例：（A：类型，a：A）+=（A，a）（r，x：A，y：M = C x）+=（Γ +，ω|C[Γ+/Γ]|，ω|C[Γ+/Γ]|+1）下面的引理说明这个实例化是正确的：242M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229►►引理5.3Γcontr蕴涵A：类型0，a：A_iΓ-拟T：类型0蕴涵T[Γ +/Γ]<$βΩ|T [Γ+/Γ]|（二）Γ_（？）idT：0型和Γ_（？）idM：T蕴涵M<$βω|T [Γ+/Γ]|（三）证据我们继续归纳MLID中的衍生物的大小。我们通过检查最后一个可能的规则来证明（1）：• 其中，r具有形状A：类型0，a：A并且r+=（A，a）。 通过使用两次变量，我们检查：（A：Type0，a：A）标识符（A，a）：（A：Type0，a：A）。• c_n可转换：r的形状为Δ，x：B，p：M=Bx，其中Δ x_idB：类型0和r_idM：B 。通 过 归 纳 假 设 ， 我 们 有 A ： 0 型 ， a ： A≠Δ+ ： Δ ， B[Δ+/Δ]<$βΩ|B[Δ+/Δ]|和M [Δ +/Δ]<$βω|B[Δ+/Δ]|. 然后，很容易检查使用具 有（A：Type0， a：A）id（Δ+，ω）的函数|C[Γ+/Γ]|，ω|c[Γ+/Γ]|+1） ：（Δ，x：B，p：M =Bx）。为了证明（2）和（3），我们注意到在T_idT：Type0的推导中，存在严格较小的T_contr的推导，因此我们可以使用归纳假设来获得A：Type0，a：A_idT+：T。现在通过替换，我们导出A：类型 0，a：A_idT[Γ+/Γ]：类型 0和A：类型 0，a：A_idM[Γ+/Γ]：T[Γ+/Γ]。我们得出结论：T[Γ +/Γ]<$βΩ|T[Γ+/Γ]| 和Mβω|T[Γ+/Γ]| 前一个lemmaQ引理5.4（所有群胚律都是可居住的）若Γ_∞T：0型，则存在θ_∞.T使得Γ_∞θ_∞.T：T.证据可收缩上下文Γ具有以下形状：A：类型0，a：A，x1：C1，y1：M1 = x1，...，xn：Cn，yn：Mn= xn我们通过n个连续的扩展路径诱导（从左到右）构造θr.c在所有的归纳之后，剩下的是在上下文A：Type0，a：A中找到T[Γ+/Γ]的居民。 但由于前面的引理，我们知道T[Γ +/Γ]<$βΩ|T[Γ+/Γ]|，因此，使用COVERSION，我们可以使用ω|T[Γ+/Γ]|.拼出，项θr.T为：θ r.TJx1：C1，y1：M1 = x1，.，xn：Cn，yn：Mn = xn.T（J）=（x2：C2，y2：M2 =x2，.，xn：Cn，yn：Mn = xn.T）[ω|C1|/x1，ω|C1|+1/y1]（···J（xn：Cn，yn：Mn=xn.T）[Δ+/Δ]（ω|T[Γ+/Γ]|，xn，yn）···，x2，y2），x1，y1）其中Δ是上下文，使得Γ= Δ，xn：Cn，yn：Mn=xn。Q作为推论，我们得到以下定理：定理5.5（MLID中群胚律的标准性）如果Γ_n_idT：Type并且如果我们有两个项M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229243M和N使得Γ_n_idM：T和Γ_n_idN：T，则存在一个证明π使得Γ_n_idπ：M = N。证据 简单地注意到，Γ M = N：输入0并应用前面的引理。Q244M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229►►►► ∀ ► ∀►►JJ. 这篇译文打字很读者在这里应该注意到，证明π也是唯一的平等（通过应用定理M=N）。我们现在准备表明，以前的定理可以推广到整个系统MLTT通过使用参数理论。定理5.6（MLTT中群胚律的居民的标准性）若Γ idT：Type，M：Γ.T，N：Γ.T，则re是π的pro，使得−→γ： Γπ：（M−→γ） =（N−→γ）.证据 通过连续的扩展路径归纳（从左到右），我们可以导出−→γ：Γ（M−→γ）=（N−→γ），由A：Type0， a：A的推导得出（MΓ+）=（Nr+）。 我们注意到（MΓ+）的类型是T[Γ+/Γ]，它在MLID中是可分型的;通过替 换 ， 我 们 有 A ： Type0 ， a ： A_idT[Γ+/Γ] ： Type0 。 因 此 ， 引 理 5.3 给 出 了T[Γ+/Γ]<$βΩn，其中n∈N。使用卷积，我们有A：Type0，a：A（MΓ+）：Ωn。因此（MΓ+）是参数环空间的居民;因此我们可以引用定理4.3来证明（MΓ+）=ωn。类似地，我们有一个证明（NΓ+）=ωn，通过连接它们，我们得到一个（M−→γ） 的 p ro =（N−→γ）。Q最后，使用与第4节末尾相同的论证，我们可以证明：π是唯一的，直到命题相等（等等）。6讨论6.1广群律我们对MLID的定义受到Brunerie写的一个未发表的笔记的启发[3]。我们对可收缩上下文的语法更一般一些：在Brunerie的定义中，出现在奇数位置的路径的起点总是可变的（即。Mk始终是一个变量），并且在他的语法中没有计算规则。Brunerie将ω-群胚定义为其语法的模型，因为计算规则的缺失使得他的框架在如何处理连贯性问题上更加自由。然而，我们的语法的目标不是给出弱ω-广群的一般语法，而是只研究在类型论的特殊情况下的广群结构，其中计算规则是处理一致性的自然方法。然而，在ω-广群胚的其他定义和MLID模型之间进行精确的比较将是一个有趣的未来工作。Garner和van den Berg [9]的语义性质使其很难与我们的工作联系起来，但我们相信Lumsdaine6.2n元情况在本文中，我们只使用参数性理论的一元情况，但它可以很容易地推广到二元情况，沿着两条路径传输：<$x=y）2<$λ（p：x=y）（q：x=y）.p<$（q<$（xR））=yRM. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229245（Ⅲ）（Ⅲ）（）（））（Ⅲ）（<$∈<$）X 2X轴x′sRRXX 2XR通过嵌套2+1路径归纳来获得路径归纳：在二进制转换α下：类型i，x：α，y：α，由下式给出（2）ααJ：类型i，αR：α→αJ →类型i，x：α，xJ：αJ，xR：αR x xJ，y：α，yJ：αJ，yR：αR yyJ翻译1α：1α。1α（x）<$= 1α的x由1α<$1αRxx给 出，在翻译的语境下定义 α：类型，x：α。 同样，翻译（2）J JJ（B，U，V）2<$ J（ J（ J（B2，U，V），U，V），U2，V2）推广第3节的抽象定理是一种例行检查，to have a binary二进制version版本ofparametricity参数.同样地，n元情形，通过沿n条路径传输而获得，并且路径归纳的平移通过嵌套n+1个路径归纳而获得。6.3用归纳族编码标识类型。在支持归纳家族的依赖类型系统中，可以通过归纳谓词对标识类型进行编码[4]。例如，在Coq Proof Assistant中：归纳路径（A：Type）（a：A）：A →Type：=idpath：paths A a a.正如[2]（5.4节）中所解释的，参数性平移很好地扩展到归纳族。其思想是用一个新的归纳I R来翻译一个归纳类型I，这个新的归纳I R的构造函数是I的构造函数的翻译。同样地，IR的消去方案是I的消去方案的翻译。归纳路径_R（A：类型）（A_R：A →类型）（a：A）（a_R：A_R a）：对于所有x，A_R x →路径A a x →类型：=idpath_R：paths_R A A_R a a_R a a_R（idpath A a）。在这个归纳类型和我们的恒等式翻译之间存在类型等价（在同伦论意义上，见[8]）它是通过使用与一个方向上的路径R相关联的归纳原理;以及通过在p上的嵌套路径归纳和在另一个方向上沿着p的运输的证明而获得的。这表明它们在道德上是相同的;它可以使读者相信，最后两部分的结果可以使用编码而不是身份类型的原始概念来6.4处理公理当形式化证明需要独立的公理时，通常的做法是简单地将它们添加到上下文中。然后，如果要使用参数化翻译，还需要提供公理的参数化证明。因此，能够证明其自身参数性的公理相对于平移而言表现良好。更正式地说，我们说一个封闭类型P：Type是可证明参数的，如果类型h：P，h P是居住的。现在我们将给出两个使用可证明参数的单位类型的公理246M. Lasson/Electronic Notes in Theoretical Computer Science 308（2014）229（1）（2）（3）（4）∀∈≡ ∀）（kA P φ）∈ <$Contr（λx：A.P x））（Ⅲ）→ ∀ ∀→≡ ∃∀≡ ∀（2）（Ⅲ）（<$∈<$）∈ ∀（<$∈<$）≡ ∀ → ∀ →∀（Ⅲ）• 唯一性证明（UIP）：设uip为以下类型uipX：Type，xy：X，p q：x =y.p = q。我们想找到一个居住在f：uip.fuip的人。语句fuip展开为X：Type，xy：X，p q：x=. 结论是路径之间的等式，所以它是y . （f A x y p q）（pR）=qR可证明的使用f.• 函数扩展性：设funext为以下类型funextA：Type ，B：AType ，fg：x：A.Bx。（x：A.f x=g x）f=g.在他最初的发展中，Voedvoesky证明了funext在逻辑上等价于所谓的弱可拓性（参见[8]）。它的定义是weakext A：Type，P：AType。（x：A. 控制P x）控制（x：A.P x）），其中对照Ax：A. y：A.x=y是可收缩的谓词类型; ie.与singleton类型等价的类型。现在我们来简单地证明we