谓词逻辑模型扩展与逻辑关系的研究及应用

可在www.sciencedirect.com在线获取理论计算机科学电子笔记347（2019）241-259www.elsevier.com/locate/entcs从谓词逻辑推导逻辑关系Claudio Hermida1 乌代S Reddy2伯明翰大学埃德蒙山口Robinson罗宾逊3，4伦敦大学玛丽皇后摘要本文将Hermida关于逻辑谓词的论文的结果从类型到逻辑关系的类型构造函数的扩展来自于对谓词逻辑模型上的这些构造函数的解释。然后通过拉回进一步扩展到n元关系。Hermida这一结果是广义的，使其更适用于左伴随，然后被证明是稳定的拉回下，从标准谓词逻辑派生帐户的n元关系一个简短的讨论解除单子谓词包括存在一个初始的这种解除，推广现有的结果。关键词：逻辑关系，纤维化，范畴类型理论，一元类型1介绍本文的目的是说明逻辑关系和预测逻辑之间的联系。我们首先重新考察在谓词逻辑中用于推理类型论的谓词可以被证明携带该类型论的结构的条件。然后，我们表明，类似的结构，二进制和更一般的n元关系，可以从一元谓词。最后，我们来看看通过单子定义的结构这种材料的核心已经1电子邮件：claudio. gmail.com2电子邮件：u.s. bham.ac.uk3电子邮件：e. p. qmul.ac.uk4这项工作得到了EPSRC基金EP/R 006865/1的部分支持，交互系统的接口推理https://doi.org/10.1016/j.entcs.2019.09.0131571-0661/© 2019作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。242C. Hermida等人/理论计算机科学电子笔记347（2019）241知道的我们扩展的结果，更清楚地带出所需要的，处理n元谓词通过改变基地，并讨论一元类型。为了做到这一点，我们利用范畴论的工具。从这个角度来看，谓词逻辑被形式化为一个代表类型论的范畴上的纤维化更准确地说，基可以被认为具有表示由变量组成的上下文的对象：类型绑定，以及由子对象给出的态射。我们首先集中在由附加定义的类型论结构（产品，函数空间和和），但我们随后讨论一元结构。逻辑关系是由戈登·普洛特金（Gordon Plotkin）提出的[13，15]。但他慷慨地给予其他人荣誉，特别是汉斯·拉乌赫利、米克·戈登和罗伯特·米尔恩。Milne在证明编程语言的不同语义的等价性方面提出了类似的想法（以包容性预测的名义）。米尔恩的见解是从那时起，这个基本思想在各种场合都得到了解释。微积分已经被引入来处理它们，[14]和其他人，并且这个想法已经从逻辑关系的范畴到底层类型的结构保持函子方面得到了解释在本文中，我们建立在这一基础上，从Hermida关于逻辑谓词的工作开始，我们稍微挖掘Hermida的工作，以表明我们并不总是需要纤维化的完整结构。这对合作产品有影响的关键点。赫米达这是一个强条件，并不适用于所有对应于逻辑的句法结构。然后我们证明了Hermida帐户的一个基础定理的变化函数空间的例子表明，这并不像第一次出现的那样简单最后，我们讨论一元类型的文件。这些行为不同于传统的类型理论结构。我们用例子来强调这一点：Set上的单子保留了monics，因此扩展到Pred上的函子，但不是所有的都是firebred（延续单子）;即使我们立即得到了Pred的扩展，我们也需要更多的工作来得到Rel的扩展（再次是延续，还有一些代数理论，如Mal我们还提出了一个单子初始提升的充分条件，并将其与Kammar和McDermott最近的工作联系起来[8]。这项工作是从[6]开始的计划的一部分，在这个计划中，我们试图将逻辑关系理论与其他形式的程序逻辑和数学推理的标准形式联系起来。本文的工作支持从谓词中导出逻辑关系的标准方式，我们期望的。这种方法的一个问题是，它要求关系具有单一的逻辑元结构，而不是在两个不同的元结构之间提供系统的链接。这可以C. Hermida等人/理论计算机科学电子笔记347（2019）241243在某种程度上可以减轻，因为所考虑的结构在产品下是封闭的，所以总是可以组合成一个单一的实体。这项工作还包含了一元类型的治疗开始。我们希望在今后的工作中对此提供更多的细节。2谓词和关系为了说明这些概念，我们使用一元和二元关系的类别：Pred和Rel。定义2.1[Pred]范畴Pred的对象是对（P，A），其中A是集合，P是A的子集。一个态射（P，A）→（Q，B）是一个函数f：A→B使得f（a）∈Q.标识和组合是从Set继承的。Pred也有一个逻辑阅读。 我们可以把（P，A）作为类型的谓词A，并将它与形式为a：AP（a）的判断相联系（读作一个态射（a：A<$P（a））→（b：B<$Q（b））有两个部分：一个替换b <$→t（a），和逻辑结果P（a）<$Q（t（a））（读作定义2.2[Rel和Reln]范畴Rel的对象是三元组（R，A1，A2），其中A1和A2是集合，R是A1×A2（A1和A2之间的关系）的子集。态射（R，A1，A2）→（S，B1，B2）是一对函数f1：A1→B1和f2：A2→B2使得a1∈A1，a2∈A2. （a1，a2）∈R<$（f1（a1），f2（a2））∈S.恒等式和组合继承自集合×集合。P Q R SFA B A1×A2f1×f2 B1×B2Reln是Rel到n元关系的明显推广。Pred具有遗忘函子p：Pred→Set，p（P，A）=A，并且类似地Rel具有一个遗忘函子q：Rel→Set×Set，q（R，A1，A2）=（A1，A2）. 这些函子具有很好的结构，对于更深入地理解结构至关重要。此外，Pred和Rel都是carbohydrate闭范畴。2.1笛卡尔闭结构Pred中的终端对象是（1，1），一个单例集，其自身作为指定子集。在Rel中，终端对象是（1×1，1，1），两个单例的总关系产 品 并不 复 杂 。 在 Pred 中 ， （ P ，A ） 和 （ Q ， B ） 的 乘 积 是（ P×Q ，A×B）。在Rel中，（R，A1，A2）与（S，B1，B2）的乘积为（R×S，A1×B1，A2×B2），其中（（ a1， b1），（ a2， b2））∈R×S当且仅当（a1， a2）∈R且（b1，b2）∈S.244C. Hermida等人/理论计算机科学电子笔记347（2019）241最后是功能空间的营造。在Pred中，函数空间[（P，A）→（Q，B）]是[R，A→B]，其中R是将P映射到Q的函数A→B的子集。在Rel中，函数空间[（R，A1，A2）→（S，B1，B2）]是（R→S，A1→B1，A2→B2），其中f1[R→S]f2当且仅当a1∈A1，a2∈A2. a1RA2f1（a1）Sf2（a2）。因此，Pred和Rel不仅都是Carnival闭范畴，而且遗忘函子p和q保持了所有的结构。2.2款项这些性质扩展到和（余积）。InPred（P，A）+（Q，B）=（P+其中c∈P+Q当且仅当c∈P或c∈Q。Rel中的和的构造类似。（R，A1，A2）+（S，B1，B2）=（R+S，A1+B1，A2+B2），其中x[R+S]y当且仅当（x= inlay = inl（b）<$aRb）<$（x= inray =inr（b）<$aSb）.3纤维化我们首先解释谓词逻辑，如p：Pred→Set。 这它的结构超越了Carnival闭范畴的同态。它是一种纤维化，具有支持谓词逻辑解释的结构。参见雅各布[7]，全面介绍了纤维化及其逻辑解释。给定一个函子p：E→C，和一个C的对象A，则p−1（A）形成一个子范畴，其中态射是映射到A的单位元上的那些。这叫做p在A上的纤维，写作EA。在纤维化的上下文中，EA的态射被称为垂直映射。在逻辑的上下文中，对象A表示一个上下文，在这个意义上，对象A表示一个给出变量类型绑定的结构，而对象A上的纤维表示在该上下文中可由结果排序的命题对于任何函子p：E→C，E的每个对象都是唯一纤维的对象。因此，E的对象是纤维对象的不相交并集，obE =A∈obCEA。但对于一般函子p，不同对象A和B上的纤维可能完全不相关，即使存在态射f：A → B。这不是p：Pred→Set的情况，或者更一般的fibrations。在p：Pred→Set中，沿着f：A→B拉回会导致函子f：PredB→PredA和重写p沿f的回调的定义属性，函子p，我们得到一个笛卡尔映射的定义定义3.1如果p：E→C是函子，则F：e1→e2被称为对任意G：e0→e2和任意因子分解p（G）=p（F）<$h关于pi∈C，则存在唯一映射H：e0→e1使得G=F<$H且p（H）=h。定义3.2函子p：E→C是纤维化，如果对任意f：c1→p（e2），存在一个卡图映射F：e1→e2使得p（F）=f（因此p（e1）=c1）。 这张地图 称为f的Carnival提升。C. Hermida等人/理论计算机科学电子笔记347（2019）241245Jφ下一个引理收集了p的性质：Pred→Set，并直接从定义中得出。引理3.3对于p：Pred →Set：(i) f：（P，A）→（Q，B）是可交换的当且仅当P=f−1（Q）（即隐式交换平方是拉回）(ii) p是一个纤维(iii) p在A上的纤维是A的子集的格。从定义中可以很容易地得出，直到唯一同构，卡里托提升都是唯一的具体地说，如果F：e1→e2和FJ：EJ1→e2都是f：c1=p（e1）=p（EJ1）→e2的进位提升，则存在唯一映射i：e1→EJ1使得F=i;F和p（i）是c1上的恒等式。映射i必然是同构。此外，假设我们给定f：A→B，对于EB的每个对象e2，f的一个选择的carnival提升，Fe：f∈（e）→e。然后f（定义在对象上）唯一地延伸到一个函子f：EA→EB。这并不意味着，如果我们被给予选择的Carnival提升，那么我们可以使用这些来导出函子p：Cop→Cat。我们可能无法选择我们的carnival提升，使得沿着态射g和f的提升的合成总是沿着合成gf的提升。相反，我们得到了一个伪函子，其中函子p<$f（gf）自然同构于（p<$g）<$f（p<$f）。这些自然同构的分量是垂直的，它们是相关纤维中的映射然而，我们将主要研究纤维是偏序的纤维化。在这种情况下，纤维中唯一的同构是恒等式，因此Carnival提升是唯一的，我们确实得到了一个函子。注意，在任何纤维化p：E→C中，E因子中的任何态射f：e1→e2为一个垂直映射，后面跟着一个carriage（carriage是p（f）的提升，垂直映射是通过三角形id上的carriage分解f得到的;p（f）=p（f））。这种分解在同构之前是唯一的，所以当纤维是偏序的时，它是唯一的。这特别适用于p：Pred→Set和q：Rel→集合×集合。一个纤维化的态（或Carnival函子）由Cat中的一个交换正方形给出，如下左所示，其中最上面的函子保持Carnival映射。由于φ上的任何Φ都保持垂直映射，因此Carnival函子也保持态射分解为垂直和Carnival。在任何函子的平方中，如左下方，Φ在纤维之间诱导函子：ΦA：EA→EφJ（A）。Since纤维化的态射保持Carnival映射，这些函子是自然的，关于重索引函子f，至少直到同构，如右图所示EΦEJEBΦBEφBpp′f（φf）C CJEAΦAEφA对于一般振动，这种自然性的精确形式表达需要246C. Hermida等人/理论计算机科学电子笔记347（2019）241X⇓χJF伪自然变换的详细相干条件，而在虚构方法中的在我们的案例中，我们处理的是部分订单，可能会合理地采用这种替代方法。逻辑关系的解释需要将类型结构从基本范畴C扩展到全局范畴E。为了做到这一点，我们需要一个由概念定义的结构。它的形式化需要函子之间的2-cell。定义3.42-categoryCat↓有：objects（0-cells）：对象是函子p：E→C态射（1-胞体）：从p：E→C到pJ：EJ→CJ的态射是一对函子Φ：E→EJ和φ：C→CJ使得pJΦ =φp。2-胞腔：从（Φ，φ）到（Φ，φ）的2-胞腔是一对自然变换X：Φ和X：φ，使得pJX=χp。ΦEEJΦE EJpp′=pφp′CCJψC CJψ2-范畴Fib是Cat↓的子范畴，其中对象是Fibrations，morphisms是Carnival函子，2-胞体是Cat↓中的2-胞体（它是局部满的子2-范畴）。设f：C→CJ和PJ：EJ→CJ是一个纤维化。然后，一个简单的检查表明，猫中p沿着f的拉回也是一个纤维化，并且拉回平方是纤维化的态射。fEJFEJf′p′C CJ注意，如果A是C的一个对象，则f∈p在A上的纤维（同构于）pJ在f（A）上的纤维。一个特别的例子是Rel，它是Pred沿着积映射Set×Set →Set的回调。Rel PredQ p设置×设置（−）×（−）设置我们将特别感兴趣的两种纤维化，语义和类型理论/逻辑。语义纤维化的典型例子是Pred。在语义纤维中，底层范畴C是一个（语义）数学对象的范畴，如Set。E在C的一个对象A上的纤维是（从）一类到C中A的映射。在Pred的情况下，这些是子集的包含重新索引是C. Hermida等人/理论计算机科学电子笔记347（2019）241247⇐η⇒GF⇒ϵϵFG⇐η∼由回调给出，因此卡里图对应于回调正方形。如果我们需要解释逻辑公式，那么我们使用标准技巧，其中A1，.，An被解释为A 1 × ...上的纤维的元素。×An. 在Pred的情况下，这表示A1上的n元谓词，.，n被解释为的子集，因此是A1×.上的一元谓词。 × An.在逻辑/类型理论的纤维化中，C的对象由上下文组成，通常是变量/类型绑定的列表：x1：A1，.，xn：An.上下文上的纤维对象由给定上下文中的类型（如果建模类型理论）或谓词（如果逻辑）组成。例如：x：A，y：A，z：B<$x=y。C中的态射是替换。所以一个来自y1：B1的态射，ym：Bm到x1：A1，.，xn：An被给予上下文y 1中的n元组项：B1，.，ym：Bm，y1：B1，.，ym：Bmti：Ai，表示替换（xi<$→ti）i=1. n.重新索引，以及纤维化的carlingmap，对应于在类型或谓词中执行这些替换如果语境承认收缩、弱化和交换的法则，那么基本范畴就有有限的产物。 如果（另外）类型论本身有有限个乘积类型，那么上下文x1：A1，.xn：An可以替换为x：A1×. × An，因此可以认为只包含一个类型。4附加物许多类型论的结构是通过分类来定义的。这包括乘积、余积和函数空间，但不是一元结构。函子F：C→D和函子G：D→C（记作FEG：C→D）之间的连接的标准定义是同构D（Fa，b）=C（a，Gb）在a和b中是自然的。 但这等价于一个公式，它允许我们在任意2-范畴中定义态射之间的一个附加定义4.12-范畴中的一个附加FEG：C→D是一对2-胞腔η：1C→GF和η：FG→1D满足CFDCFDDGCDGCID id =idID idid=id idC D CFD C DGC这给了我们Cat↓中附加词和Fib中附加词的定义。解开这些定义，我们看到，在这两种情况下，EΦEJEJEpp′CφCJpp′CJC相当于基φE中的一个附加项和在适当意义上相互重叠的全局范畴Φ E之间的一个附加项。具体地说，这意味着Cat↓中的一个附加函数（Φ，φ）E（φ，φ）恰好是一个映射（p，pJ），248C. Hermida等人/理论计算机科学电子笔记347（2019）241⊥g布吕[11]第七章：我的世界我们还将使用第三个特征的解释。引理4.2设FEG：C→D，且令f：FGd→d是id：Gd→Gd的伴随（伴随的可数）。则对任意f：Fc→d，f的伴随f ∈ F ∈ C是唯一映射f∈ C → Gd使得f = F（f∈C）;这告诉我们，如果我们考虑逗号范畴（F↓d），它的对象是D Fc→d中的态射，它的态射是C中的映射f，使得F（f）进行明显的三角交换，则F：FGd→d在（F↓d）中是终结的。反之亦然。给定F，对于D的每个对象d，在（F↓d）中选择一个终结对象：F（cd）→d，则存在唯一函子G：D→C使得Gd=cd，FEG，且G是该附连的计数一个对偶结果连接了附加映射和单位的另一个方向（id的伴随：Fa→Fa）：对于一个nyg：a→Gb，g∈，fg的伴随是唯一的映射g∈：Fa→b，使得g=η;G（g∈）。5纤维之间的连接纤维化中的每一个映射都是一个垂直部分（存在于单个纤维中的东西），后面是一个carpal部分（代表纤维之间直接平移的东西）。在这一节中，我们重现Hermida5.1基地变更在纤维化中，与卡尔维特映射等价的是一个卡尔维特函子，它通过基的变化而产生。第一个结果说，基底中的一个附加物延伸到纤维化和它的基底变化之间的一个附加物引理5.1（Hermida，[4，5]）设p：C→A是纤维化，且fEg：B→A是一个附加条件，然后有一个固定的附加条件pffCCfppFB A是的。设f∈是f∈g的计数器，c是C的对象。 则定义g（c） =（g（c），c），其中：c→c是pc：fgpc → pc的（选择的）笛卡尔提升。Q仔细观察证明，我们只使用纤维化结构来证明存在性。因此，同样的证明给出了任意类别的结果推论5.2设q：C→A，且fEg：B→A是一个伴随函数，且对所有c∈C，fEg的可数集，f：gfpc→pc有一个提升到c的carriage，则有C. Hermida等人/理论计算机科学电子笔记347（2019）241249fpffg⊥gQfpFB⊥⊥↓∗^^→E →→→→→是一个附加词pfEg：pC→C在原来的附加词，如在s e4，给予一个附加词在猫。取所有范畴的相反，我们得到左伴随的相应结果：推论5.3设q：C→A，且f：B→A有左伴随g。此外，假设附加函数的单位有一个到C的余项提升，则p f：p<$C→C有一个左伴随g<$f，并且附加函数g<$p <$f位于原附加函数g<$f之上。5.2预防措施的分解这些结果现在可以推广到任意的情况。我们证明了在某些提升条件下，一个附加函数可以由一个固定基上的附加函数（垂直部分）和一个由引理5.2中的基变化得到的附加函数（carbohydrate，水平部分）组成。下面是Hermida的一个vanilla扩展，[4，5]。我们不要求函子p和q是纤维化。命题5.4假设f：D→Coverf：B→A，则f有一个右（分别为左）的伴随g，并且该伴随的单位η和计数η都具有到C和D的任意对象的笛卡尔提升，令f因子通过拉回f <$C如下：FFDC=D Cqgp pFB A AGg则以下是等价的：(i) F有一个正确的（resp。左）伴随g在附加f E g上(ii) f有一个权利（resp.）左）在B上的恒等式上的伴随g。是的。 对于Rig htadjoint（i）→（ii）：Supose（b，c）∈ob（f<$C ）. 设ηb：ηc→gcb是单位η：b→gfb=gpc=qgc的一个（chosen）carnival提升. 定义g（b，c）=ηc。如前所述，g在B上的恒等式上正则地扩张到函子。为了建立这个附加函数，假设β=（β1，β2）：fd=（qd，fd） （b，c）在f中。我们有fβ1=pβ2：fqd=pfd fb=pc。使用基中的加法，它的右伴随是（gfβ1）η：qd gfb。但η是自然的，所以（gfβ1）η=ηβ1。现在转向附加函数fg，β 2：fd c的右伴随β：dgc存在于ηβ1上。如果η∈η是carbohoverη，则存在唯一的β∈：dη_c=g_c（b，c），位于β1之上，则η_cβ_c =β. 这种构造在bothvariables中是自然的，因此根据需要给出了位于B上的恒等式附加上的附加。对于左伴随：将结果应用于所有类别的最小值Q250C. Hermida等人/理论计算机科学电子笔记347（2019）241⊥⊥伴随的这种分解表示右伴随分两部分得到第一部分是起重机。在标准的谓词结构中，这相当于将项替换到作为参数给出的谓词中。第二部分是同一基底上两个纤维之间的连接。这一部分取决于特定逻辑结构的存在。例如，我们将看到合取用于给出乘积，析取用于求和（使用左伴随的对偶结果5.3示例在本节中，我们将看看上面的结构如何帮助定义结构，Pred →Set。例5.5【积】积是对角线的右伴随Δ设置设置×设置×考虑Pred×Pred沿Δ的回撤：ΔPredΔ˜Δ∧pΔ（p×p）设置（p×p）ΔgΔ⊥×Pred×Predp×p设置×设置在Pred上，Δ将集合A上的谓词P映射到集合对（A，A）上的谓词对（P，P）在集合A上的Δ（Pred×Pred）的纤维是Pred（A）×Pred（A），所以Δ因子通过Δ（Pred×Pred）yΔ，其中Δ在f的纤维中将P映射到（P，P）Δε（Pred×Pred）除以A。（p×p）ΔΔ现在将其映射到Pred×Pred纤维中的（P，P）超过A×A。根据引理5.1，（p×p）Δ的伴随是通过沿着基中的伴随的计数提升而给出的该计数是投影λ：（a0×a1，a0×a1）→（a0，a1）：λ（x，y）的乘积。（π0（x），π1（y））。因此，给定A上的谓词P和B上的谓词Q，g将（P，Q）ovr（A，B）映射到o（π0<$P，π1<$Q）ovrA×B。用更合乎逻辑的术语来表达：如果a：AP（a）：Pred和b：BQ（b）：Pred，则将g应用于这对谓词的结果是通过替换得到的对a<$→π0（x）为P（a），b<$→π1（x）为Q（b）：x：A×B<$（P（π0x），Q（π1x））：Pred ×Pred。此操作的目的是获取同一类型的两个谓词。如果我们写这样的东西：a：A，b：B<$（P（a），Q（b））：Pred ×Pred，这是模糊的。A的集合是A的集合，它使A上的一对（P1，P2）表示它们的交叉点，P1→P2。从逻辑的角度来看，这是一种结合。把这些放在一起，我们得到Δ的右伴随：Pred→Δ ×Δ需要C. Hermida等人/理论计算机科学电子笔记347（2019）241251−×P−BVPp（−×A）⊥g（−×A）ΔPred（−×A⊥gp设置−×A⊥（A，B）上的一对谓词（P，Q）（记为（P（a），Q（b））到A×B上的谓词P（a）<$Q（b）。这是我们所期待的。 直接计算这一点很容易，但关键是要将其视为来自我们的一般预防框架。例5.6[函数空间]对于函数空间，我们有：PredA→−Predp设置这里，P是A上的谓词，−×P是刚刚计算的函子，将B上的谓词Q发送到B×A上的Q（b）<$P（a）。如前所述，我们分阶段计算右伴随。给定Pred（B）中的（Q，B），基数中的计数是求值： evB：（A→B）×A→B。g∈（Q，B）是v∈B（Q，B），（Q，B）的拉力是v∈B. 从逻辑的角度来看，这相当于Q（b）中的替换b → f（a）。 我们将结果非正式地写为f：A→B，a：A<$Q（f（a））Pred，或者更正式地写为x：（A→B）×A<$Q（（π0x）（π1x））Pred。现在，集合C上的（−×A）Pred的纤维是Pred（C×A），−×P通过−P分解。特别地，如果R是C上的谓词，则RP是R（c）P（a），C×A上的谓词。与之相连的框架g表示一个谓词S（c，a）toa∈A.P（a）→S（c，a）. 这存在于Pred中，但如果我们在一个更一般的逻辑中编码这个逻辑有蕴涵和一阶量化就足够了。把它和前面的伴随词放在一起，我们得到Q被发送到上的谓词，A→B，其中fi∈A，P（a）→Q（f（a））成立。例5.7[副产品]副产品的理论与产品的理论相似。下图的整体结构与产品相同。但我们没有把车停在路边。特别是，Δ，Δθ和Δε（Pred×Pred）等均为前一项。左边的a和Δt是不连续的，在纤维中。为了得到（p×p）Δ的左伴随，我们使用沿着基中的单位的余余度提升。基数的单位是λ（a，b）。（inla， inrb）：（A，B）→（A+B，A+B）。这个的余项提升需要A上的一对谓词P，B上的Q到{inla ->P（a）; inrb ->False}的谓词case x和{inla ->False; inrb -> Q（b）}的谓词case x，这两个谓词都在A + B上。 这是存在量化的一种弱形式，比沿着任意映射的cocartesian提升弱得多。 沿着乘积投影的余项提升对应于标准的存在量化。252C. Hermida等人/理论计算机科学电子笔记347（2019）241不不∗ΔPredΔ˜TΔτ（Pred×Pred）∨pΔ（p×p）设置（p×p）ΔgΔ+Pred×Predp×p设置×设置6基地变更6.1结果这一节是关于第5节中的结果对于通过改变基而得到的情形的含义我们想把结构从一个原纤维化转移到另一个原纤维化，通过沿着适当的基底变化拉回原纤维化而获得另一个原纤维化。关键的例子是Pred沿着[n：Setn→Set]的回撤，它表达了一个n元关系可以被视为基础集合的乘积上的一元谓词的事实。首先，我们观察到拉回保持了笛卡尔性，即使所涉及的范畴不是纤维化。引理6.1假设下图是一个范畴拉回图，α：P0→P1在Fα上的P中是可积的，其中α：B0→B1。则（α，α）在F P上的卡里。FPpFPFppBFA为了我们的目的，我们考虑基地中的以下情况。我们有一个交换正方形，如下所示，其中水平箭头F和G有右伴随Fr和Gr。 KGr= F rH并不一定是这样的情况，尽管它们之间有一个规范的自然变换，即FK = HG上的恒等式的配偶。我们将考虑FEFr上范畴的一个附加，沿着H和K向后拉。引理6.2假设我们给定一个如上所述的交换正方形和一个A上的范畴P。这就产生了下面的立方体，其中正面和左右两侧都是回调。函子G作为明显的拉回因子分解而得到。函子F和G有右伴随Fr和GR.C. Hermida等人/理论计算机科学电子笔记347（2019）241253P⊥H PF PG⊥CGrHKBF⊥赫普FQ⊥RQFG⊥CGrHKBF⊥EKFGKFpPDp一Fr设H是G Gr的计数器，H对P有进位提升.则G在G r上有右伴随证据由于回撤是合成的，所以前面和左面的合成也是一个回撤。因此，后面和右边的合成也是如此。这反过来又意味着背面是一个回调。现在我们应用引理6.1，证明了HP具有carnival提升，并应用引理5.2得到结果。Q引理6.3假设G E Gr是Cat/B中的一个附加函数，则沿着函子K：D→B往回拉，给出D上的一个附加函数。证据沿着K拉回得到一个2-函子K：Cat/B→Cat/D。因此，K保持Cat/B中附加函数的单位和计数，以及它们满足三角恒等式的事实。 因此，它保留了附加条款。Q下面的命题将这些结果组合在一起，以说明通过沿着函子H和K拉回来改变p和q之间的附加函数的基，如下图所示。这里的输入数据由立方体克兰克GHP克尔克山口Dp一Fr所以（q，p）是一个映射且HG=FK。G是映射KQ→HP通过拉回的因式分解获得命题6.4给定一个如上所述的立方体，假设正面是一个通过命题5.4中的拉回通过因式分解获得的调整映射，并且HG=FK，进一步假设GEGr的计数器：GGr→1C具有carnival254C. Hermida等人/理论计算机科学电子笔记347（2019）241Δ⊥×集合n×集合nΔ⊥Π×Π⊥（−×Ai）Π⊥（Ai→−）−×Ai⊥Π提升至HP（例如，如果H具有提升至P的小车）。则G：K<$Q→H<$p是G E G r上的一个伴随中的左伴随，其中右伴随也是通过图5. 4中的拉回通过因式分解构造的。证据 这直接由引理6.2和6.3得出。Q6.2示例例6.5[积]我们考虑n元关系的二进制积.RelnΔReln×RelnΔPred集合nΠPred×Pred设置设置×设置×立方体的正面是我们在例5.5中看到的逻辑谓词的二进制积的构造。关系是通过从Pred沿着乘积函子：Setn→Set拉回来构造的。这将我们带到立方体的底面，它是上下班的。这一点值得详细说明。给定集合的n元组：（Ai）i∈{1. n}，沿后右侧取此值，得到（n × n）Δ（Ai）=（n Ai，n Ai）沿左前侧取此值，得到Δ n（Ai）=（n Ai，n Ai）。它们是相等的，而不仅仅是规范同构的，因此我们可以立即应用上面发展的理论来证明n元关系的乘积是如我们所期望的那样构造的例6.6[函数空间]要从一元函数空间导出n元函数空间，图是：RelnReln集合nPred集合nPred集合套网（Ai）→−然而，这个立方体的底面不通勤。考虑集合n的一个对象（Bi）。向左和向下绕广场，我们得到（Bi×AI），而向左和向下绕广场，我们得到B i ×A I，C. Hermida等人/理论计算机科学电子笔记347（2019）241255向下和向左，我们得到（Bi）×（Ai）。它们自然同构但不相等。因此，我们不能简单地应用上面的结果至少有两种方法可以解决这个问题。更有原则的是重做理论，以便它能处理到自然同构的交换。技术上更简单的替代方案是固定正方形，以便它通勤。将立方体的左前垂直边替换为其与上的不离散类别的乘积集合，集合obSetn×Set的对象是对（（Bi），C），其中（Bi）是集合的n元组，C是集合。态射（（Bi），C）→（BiJ），CJ）是函数C→CJ。 这给了我们一个等价于原始的结构，并且具有相同的形式属性。但是我们可以修改形成底部正方形边缘的两个函子。我们取第一个由（Bi）<$→（（Bi），<$Bi）给出，第二个由以下态射的自然扩张给出：F（（Bi），C）=C×<$Ai如果C=<$BiF（（Bi），C）=<$（Ai×Bi）如果C=<$Bi广场现在上下班，我们的理论适用。但由于一切都等价于原始的，函数空间的逻辑描述仍然有效。例6.7[副产品]和前面一样，副产品的故事和产品的故事是一样的。 它使用相同的图表，但理论是应用 相反的范畴，产生左伴随而不是右伴随。 特别是立方体的底面是通过对所有涉及的类别应用op从产品图的底面获得的。因此，它可以精确地上下班。7Monads单子提供了另一种定义结构的方法。给定一个表示类型的范畴B，一个表示B的谓词逻辑的范畴P，以及一个B上的单子T，那么就没有将T扩展为P上的单子的完全通用的方法。但在某些情况下还是有办法的7.1单子的初始余项提升在[8，9，10]中，单子从基B到纤维化（逻辑）的总范畴P的这种扩张被称为提升。KatsumataKammar我们确实可以在p上非常小的条件下提供这样的初始升力：定理7.1（单子的初始提升）给定一个单子（T：B→B，η，μ），当p：E → B允许η的余提升时，单子提升范畴Lift（T）允许一个初始对象。证据定义提升单子（T：E→E，η，μ）如下：对于一个对象X∈E，256C. Hermida等人/理论计算机科学电子笔记347（2019）241设ηX：X→TX是ηpX：pX→TpX在X上余卡提升。 这就定义了T和η。使用这两个单位方程，我们有μπ（η·η）=η，并且由于η·η是余度，所以存在μ上的唯一变换μ：TT→T，使得μπ（η·η）=η。Cocartesianess也证明了这些数据的单子方程，以及初始性。Q一般来说，提升的单子函子T即使在p是纤维化时也不会被纤维化，但它是纤维化的。[8，定理4.8]的初始提升是一个特例，假设函子p的纤维是小的完全前序。当p容许余度提升和余度提升时，对于ηX：X→TX，ηXEηX ：ET X→EX。假设纤维是小的，前序，伴随函子定理告诉我们，左伴随（=余项提升）计算为：{x∈ET X|y≤ηX<$x}。对于一个忠实函子p，条件y≤ηX<$x等价于在η X上存在态射y → x。这后者正是该单位在建设中尊重y的条件。[8]第254页中T的初始提升。我们在这里忽略了T中代数运算的存在，我们将在后续文章中单独处理值得注意的是，7.2monics上的象分解和monad如果P在C中被表示为一元的子范畴（例如Pred），那么T已经在P的对象上被定义，我们可以认为T（P>A）是从TP→TA定义的。如果T在我们的子范畴中保持一元论，那么这是fine。如果没有，我们可以希望使用一些图像分解TP TJP TA，如[3]。 这种提升的方法已经用虚构的语言进行了重新塑造，使用了余度提升和理解，代替了[2]中的图像因式分解。我们使用两个特殊的单子作为运行示例：列表单子L和延续单子C。列表单子是代数结构的一个例子，而延续单子不是。7.2.1集合上的单子与一元谓词设T是集合上的单子。 然后T保持monics。引理7.2（i）设F：Set→Set是函子，i：A>B是幺半群，其中A/= π，则Fi也是monic。(ii) 设M：Set→Set为单子，i：A>B为幺半群，则Mi也是幺半群.(iii) 设M：Set→Set是一个单子，则M扩张到一个函子Pred→Pred集证据（i）i具有由F保存的撤回。（ii）如果A是非空的，那么这是从前面的注释得出的。如果A为空，则有两种情况。如果C. Hermida等人/理论计算机科学电子笔记347（2019）241257∗∗M=M，则Mi： M=M=MA→MB是 自动幺半群.如果M∈M=M，则设r是 一个映射B→M∈M。MB是B上的自由M-代数，因此存在唯一的M-代数同态r：MB→M扩展它.Mi也是一个M-代数同态，因此复合r（Mi）也是。由于M是初始M-代数，它一定是单位元，因此Mi是幺半群。㈢立即。Q例7.3列表单子：LB是其元素来自B的列表的集合，因此是LA的子集。直接像幂集函子P：Set → Set，其中P（f）={b|f（a）= b}，也有性质PB<$PA，如果B <$A。连续单子定义为CA =（A→K）→K，其中K是连续单子的集合。 C_n同构于K ， 且 包含常数 泛 函 . 它 们 包 含在 任 何 类 型 的 CA 中 。如 果B≠A ， 则 CB=（B→K）→K，如果j：B→A是B包含在A中，则Cj将CB发送到{Φ：（A→K）→K|gTB = gJTB→ Φ g = Φ gJ}。但从纤维化的观点来看，有一个区别：L和P是纤维化函子，而C不是。从逻辑的角度来看，这意味着L可以很好地使用替换，但C不能。引理7.4 C不是一个有限函子。证据设A={ 0， 1}，B={a，b，c}，f：B→A定义为：fa= 0，fb=fc= 1。设P={1}<$A。 则f∈P={b，c}。 给定λ：CB，（Cf）λ = λg：A → K。 （g）考虑函数Θ：CB，定义为如果hb=hc ，则Θh==ha，如果hb hc现在，对于任何g：A→K，（（Cf）Θ）g = Θ（g<$f），但（g<$f）b = g 1 =（g<$f）c，所以（（Cf）Θ）g = g 1。因此，（Cf）θ在CP中，因此θ在（Cf）（CP）中。然而，将Θ应用于h的结果可以清楚地取决于ha。因此，Θ不在C（f<$P）中。因此，C不是一个有限的函子。Q7.2.2集合上的单子与二元关系当涉及到二进制，更一般地说，n元关系时，也有一个差异。 设R>A×B，则MR>M（A×B），存在一个正则映射M（A×B）→MA×MB，但这不一定是幺半群，因此诱导的MR→MA×MB也不一定是幺半群。引理7.5映射（CπA，CπB）：C（A×B）→CA×CB不一定是幺半群。证据CX=（X→K）→K。考虑K= 2，A=B= 2的例子。然后一个简单的基数论证表明，没有映射C（A×B）→CA×CB可以做一个莫妮卡。 |C(A × B)|= 224 = 216，而|=2 22|= 2 22 222= 2 8.Q258C. Hermida等人/理论计算机科学电子笔记347（2019）241一些单子，比如列表单子，确实有这个映射是一元的性质，因此它们保持二元关系。引理7.6如果i：R>A×B，则LR>L（A×B）→LA×LB是幺半群。是的。 令[（a0，b0）， . . （an，bn）]和[（aJ0，bJ0）， . . （amJ，bJm）]bettwotypical elemes ntsL R。 然后这些映射到（[a0， . ，an]， [b0， . ，bn]）和（[aJ0， . ，aJm]，