算术论域中有限可判定FP-草图的构造性版本和证明

理论计算机科学电子笔记122（2005）105-126www.elsevier.com/locate/entcs算术论域玛丽亚·艾米利亚·马耶蒂帕多瓦大学数学专业和应用学院Via Belzoni n.7，35100帕多瓦，意大利maietti@math.unipd.it摘要我们考虑在算术论域中的有限可判定FP-草图。 我们所说的FP-草图是指具有终端和二元乘积锥的草图 。 我 们 所 说 的 算 术 论 域 指 的 是 一 个 列 表 - 算 术 预 命 题 ， 它 是 我 们 对 由 Andr`eJoyaltoproveGodelincompletenessthe orem导出的算术论域的概念给出的一般范畴定义。然后，对于有限可判定的FP-草图，我们证明了Ehresmann-Kennison定理的一个构造性版本证明是通过使用算术论域的内部依赖型理论完成的保留字： 从属类型理论，范畴逻辑，预设，草图，草图模型。1介绍在范畴论中，草图概念是形式演绎系统概念在注释图上的范畴对应。在范畴和草图态射方面也存在相应的“理论”和“模型”的概念在本文中，我们考虑有限判定FP-草图内部的arithmetic宇宙。我们所说的FP-草图是指具有终端和二元乘积锥的草图。我们所说的算术论域是指一个列表-算术preto- pos。实际上，在[9]中，我们提出了列表算术预命题的概念，作为由Andr`eJoyal构造算术论域的一般范畴定义，以提供Godeellincoimpleteness的一个具体的预命题1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.06.054106法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105定理这个定义在[9]中被证明是正确的，因为Joyal在这里，我们通过证明有限可判定FP-草图的Ehresmann-Kennison定理的构造性版本，维克斯和其他在现场工作的人。Ehresmann-Kennison在这里，我们在有限个可判定的FP-草图上建立了一个图态射的反射，这些图态射的值在一个算术宇宙中，并进入相应的模型类别为了在算术论域内部定义一个有限的可判定的FP-草图并进行反射的证明，我们使用了一种内部语言，用于列表算术命题，该命题在马丁-洛夫的类型理论的结构中被表述为依赖类型理论（参见[ 8 ]）。这种方法把一个新的算术世界看作是对于有限的情况，我们给出的证明是关于一个小草图模型的经典证明的一个构造性的和谓词性的公式化在设置。事实上，[1]中的证明在所有模型上使用了Freyd我们证明的关键点是执行一些归纳定义，以在所考虑的草图的箭头和必须转化为模型的图态射的值上构建树。这里证明的定理也可以通过建立更复杂的树来扩展到有限个可判定的lex-sketces，并且可以应用于建立如[1]中那样的sketces的理论，但是考虑算术论域作为我们的集合论域来代替集合范畴。我们的最终希望是，这些结果，可能扩展到有限个可判定的lex-sketches也有余积，可以用于数据库建模的应用，如[6]所示。 原因是，在一个直观的谓词论域中工作，就像我们的集合论论域一样，迫使我们基于更基本的性质法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105107一而不是在集合的范畴内工作。2算术宇宙我们回忆一下[9]中算术论域的定义。定义2.1算术论域1是一个列表-算术预拓扑，也就是一个带有参数化列表对象（也见[2]）的预拓扑（也见[14]，[4在[8]中，我们证明了用Martin-Léof's类型理论y（sethethe a pendix）形式表示的依赖类型演算Au简而言之，这种算术宇宙的内部语言对应于配备了列表和子项的集合论结构的谓词连贯逻辑。相对于直觉主义逻辑，谓词连贯逻辑缺乏蕴涵和泛量化，即只有合取、假和、析取和存在量化。从[10]中，我们回忆起算术论域也有余均衡器：命题2.2在任何列表算术预拓扑U中，存在任意两个给定态射的余均衡器。从类型论或逻辑的观点来看，这个命题说，在算术论域的依赖类型演算u中，我们可以在任何不一定是等价关系的关系上定义商类型。我们将在本文中执行的构造中经常使用此属性。给定一个算术论域U，我们将通过使用附录中的类型化演算Au，在U内部引入有限可判定FP-草图的概念一个类属草图是一个具有一组恒等式、图、锥和上锥的图（关于草图及其模型的一般说明，我们参考[1，5]）。草图概念是形式演绎系统概念在注释图上的范畴对应。通过草图，我们可以以范畴的方式指定代数结构，如幺半群、群、环。在这里，我们将注意力限制在具有终端和二元乘积锥而没有上锥的有限草图实际上，我们使用的术语与具有有限乘积锥的草图相同，不一定只有二进制，因为我们总是可以通过二进制来定义有限乘积锥因为有限集合是指与集合有双射对应的集合，[1]请注意，在[18]中，使用了算术论域的一个明显较弱的一般范畴定义。108法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105→U∈∈对于小于给定自然数的自然数，我们在算术宇宙中的有限性概念意味着我们的有限集合的元素相等的可判定性，这就是为什么我们添加形容词在开始给草图下必要的定义之前，我们先做如下评论。注2.3通过内部语言Au，我们确定了算术论域U的对象A具有类型A和态射f：A→B在U中具有项f（x）∈B[x∈A]。相反，任何由附录中的Au的规则构建的闭类型表示U的对象，任何形式为f（x）∈B[x∈A]的项，具有A，B闭类型，表示U的态射。关于范畴和类型理论之间更精确的对应，见[8]。注2.4利用内部语言我们可以证明一个态射f：A的B是monic的，当且仅当我们可以得到一个证明，类型x=Ay[x∈A，y∈A，z∈f（x）=Bf（y）]其中x=Ay[x A，y A]代表附录中的等式类型Eq（A，x，y）。定义2.5我们说U的内部语言中的两个类型A，B是同构的，用AB表示，如果存在两个项f（x）∈B[x∈A]和g（y）∈A[y∈B]，使得我们可以导出g（f（x））=Ax[x∈A]的证明和f（g（y））=Ay[y∈A]的定义2.6在算术论域U内部的有限可判定FP-草图S（G，Diag，ConFP）由以下数据给出：(i) 图G ∈（G0，G1，δ0，δ1），即G0和G1是U，分别表示对象集和箭头集，U的δ0和δ1态射分别表示域映射和上域映射δOG1G0δ1使得存在两个自然数n0，n1，我们可以证明图是有限的（因此是可判定的），的g0n∈Nx≤n0G 1n∈Nx≤n1(ii) 将任何对象发送到其单位箭头中的monic单位映射id（−）：G0G1(iii) 一组由单声道Diag：D0<$z∈Cat（G）1×Cat（G）1δb0（π1（z））=G0δb0（π2（z）） ×δb1（π1（z））=G0δb1（π2（z））法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105109^ ^您的位置：≡联系我们其中Cat（G）是由图G生成的自由范畴，图G定义为[10]，δ0，δ1：Cat（G）1→Cat（G）0是定义域和上定义域映射;(iv) 由ConFP（V，ν，conFP）描述的一组终端锥和产品锥，其中V是产品锥和终端锥的顶点集，ν 是态射V：V G0将锥顶点映射到图的对象，并且任何v∈V上的锥由下式描述：conFP（v）∈（<$f1∈G1 <$f2∈G1δ0（f1）=G0ν（v）×δ0（f2）=G0ν（v））<$T注2.7在下文中，为简单起见，我们假设V P与conF P（inl（p））<$inr（p）conF P（inr（p））<$inl（πa（p）， πb（p）， eq，eq>>）其中a（p）=δ1（πa（p））且b（p）=δ1（πb（p））。我们还将使用以下缩写：vtinl（）和vpinr（p）。我们可以通过S的图上的内部图来考虑从内部草图S到算术论域U本身的底层草图的图态射（参见[1，5]）：定义2.8U中有限可判定FP-草图S（G，Diag，ConFP）上的图态射，用F：S →U表示，是U中内部图G上的内部图（关于范畴定义，例如参见[10]），也就是说，在U的内部语言中，我们可以导出依赖类型F0（x）[x∈G0]和类型化项F1（f）（z）∈ F0（y）[f∈G1，x∈G0，z∈F0（x），y∈G0，ZJ∈x=G0δ0（f），ZJJ∈y=G0δ1（f）]描述从草图的底层图到算术宇宙的图的图态射，以保持它们的域和余域的方式将对象发送到对象，将箭头发送到箭头。定义2.9给定U中的有限可判定FP-草图S（G，Diag，ConFP），从图态射F：S → U到U中的图态射H：S →U的自然变换α：F→H由项给出αx（z）∈H0（x）[x∈G0，z∈F0（x）]使得我们可以证明H1（f）（αx（z））=H0（y）αy（F1（f）（z））[x∈G0，y∈G0，f∈G1，z∈F0（x），ZJ∈x=G0δ0（f），ZJJ∈y=G0δ1（f）]现在，我们引入算术论域U中FP-草图的模型的概念。110法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105˜SU˜SU∈ ∈×∈×不苏苏美国→美国定义2.10算术论域U中的FP-草图S（G，Diag，ConFP）的模型是图态射M：S → U在U中由M0（x）[x∈G0]和datypedtermM1（f）（z）∈M0（y）[f∈G1 ， x∈G0， z∈M0（x），y∈G0，zJ∈x=G0δ0（f），zJJ∈y=G0δ1（f）]表示，使得(i) 的单位映射被发送到对应的单位映射，也就是说，我们可以推导出M1（idx）（z）=M0（x）z[x∈G0，z∈M0（x）](ii) 的图被发送到交换图，也就是说，我们可以推导出一个证明，Mf1（π1（Diag（d）=M0（δc1（π1（Diag（d）Mf1（π2（Diag（d）[d∈D0]其中M是在由草图G生成的自由内范畴Cat（S）上由M生成的自由内范畴图2（自由内范畴图M的构造见[10]）;(iii) 锥发送到圆锥极限，，也就是说，如果V P如注2.7所示，则M0（v（vt）同构于终结对象，对于每一个pP则M0（v（vp））同构于M0（a（p））M0（b（p）），如果f（z）M0（v（vp））[zM0（a（p））M0（b（p））]是同构，则我们得到一个证明，M1（πa（p））（f（z））=M0（a（p））π1（z）[p∈P，z∈M0（a（p））×M0（b（p））]并证明M1（πb（p））（f（z））=M0（b（p））π2（z）[p∈P，z∈M0（a（p））×M0（b（p））]也就是说，投影被发送到投影。现在我们给出图态射范畴和模型范畴的定义变成了一个算术宇宙对于下面的内容，我们假设S（G，Diag，ConFP）是U中的有限可判定FP-草图。定义2.11S是作为对象的图态射F和作为具有明显的组合和单位的态射的自然变换的范畴。然后我们定义保持图的图态射的范畴：[2]关于内部范畴上的内部范畴图的定义，例如参见[12]的第242页，在那里它们被简单地称为内部图。在这里，我们添加了形容词法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105111S UU3定义2.12D（，）是范畴S的全子范畴，图态射将草图的图转换为U的交换图，并将单位转换为单位，如定义2.10的点（i）和（ii）所示。定义2.13Mod（S，U）是范畴US的全子范畴，其模型为算术论域U中的可判定有限FP-草图S。在这一点上，请注意，在内部图上处理图态射与在自由范畴上处理相应的内部范畴图并没有太大的不同，自由范畴是从图中发送单元到单元并保持内部组成而生成的。 的确，由于在[10]）中，内部图G上的任何图态射都产生范畴Cat（G）上的自由内部范畴图，我们可以很容易地证明：命题2.14图态射范畴US等价于Cat（S）在U中的内部范畴图范畴3反射在这里，我们将介绍证明我们的主要定理所需的所有构造，即给定一个有限可判定的FP-草图S，存在US到Mod（S，U）的反射。这一结果将通过三个步骤实现：(i) 首先，我们观察到D（S，U）与US是互反的;(ii) 然后证明了Mod（S，U）与D（S，U）是对应的，D（S，U）是最难的部分;(iii) 最后，我们将这两个反射合成，以获得所要求的将US反射为Mod（S，U）的反射。这是第一步。命题3.1给定FP-草图S，包含函子I：D（S，U）→ US有一个左伴随证据左伴随的构造是通过模仿通常的集合论构造来完成的。对于每个图态射F，我们将图[3]这个定理对应于[ 1 ]中关于集合中草图的Ehresmann-Kennison在这里，我们更喜欢把图态射称为那些只保留了def中的图结构的图。2.8112法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105SD S U S UUS → U D S UmorphismF定义于achobjectx∈G0byco，将F应用于所有可合成态射序列对所得到的态射进行均衡在示意图中或在单元图中，可能通过用态射S的序列与HCO域NX构成M来扩展。Suchanobjec tF（x）可以通过2.2号提案来建立Q为了执行第二步，即证明 （ 、）到Mod（，）中，我们需要在内部构建一些归纳类型，这些类型部分基于可组合箭头的序列，在图表下面。因此，我们将研究使S的图可换的最小范畴。这是通过将由草图图G（在[10]中描述）生成的自由范畴Cat（S）的态射Cat（S）1在S的图下进行表示而获得的，这是可能的，这要归功于prop2.2。命题3.2在U中我们可以定义商范畴D1（Cat（S）1/Diag）和D0G0其中Diag标识符被定义为Diag索引的草图与Cat（S）中标识标识符的图与草图标识符的并集。 我们用[−]：S → Cat（S）/Diag表示将草图投影到范畴中的图态射。注意符号。请注意，在下文中，为了使公式更具可读性，我们将使用缩写：对于a，b∈GD 1（a，b）x∈D1 δ0（x）=G0a×δ 1（x）=G0b给定f∈G1，我们可以简单地写f∈D1（a，b）而不是[f]，eq，eq>>∈ D1（a，b）<3.1树木的构造在本节中，我们描述了树的构造，我们将使用它从所考虑的草图上的图态射开始为有限可判定的FP草图构建模型。这些树由以下成分组成：- 给定的有限可判定FP-草图S在U内部的态射的可合成序列;- 应用于草图对象的图形态射F：in（，下面我们将经常在对象x∈G0上使用符号F（x）或F（f）在箭头f∈G1上而不是写F0（x）或F1（f）。法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105113^^不^^^^^^≡ ×·d）、^ ^您的位置：^^其中xv（vt）∈G0. 因此，我们可以定义一个单位η：F→F^。→^F^（c）的预处理与F^（c）的预处理的组合3.1.1这个想法基本思想是能够从图态射中构建模型FF：S → U。 让我们开始考虑有一个草图只有一个终端由于我们现在知道F^（v（vt））必须是一个最小的对象，因此我们可以简单地设F（v（vt））<$T.然后，终止于终端顶点的箭头的单位自然图平凡地交换。相反，如果我们考虑G1中的箭头g：ν（vt）→a，则从下图的交换性F（ν（vt））ην（v）TF（g）JJFb（g）F（a）ηaFb（a）我们得到F（a）必须是类似于图的推出，即F（a）<$（F（a）<$D1（v（vt），a））/Rel其中Rel必须包含F（g）（y），其中y∈F（v（vt））与g有关。在这种情况下，对于x∈F（a），我们将F（g）（n）<$[inr（g）]和ηa（x）<$[inl（x）]（其中inr和inl是附录中的和型注入然后，考虑具有顶点c×d和箭头g的乘积锥的草图：c×d→a，并且为了简单 起见， 假设F （c×d ）=F （c ）×F （ d） ，并且 ην （ c×d ）ηcηd. 然后，从图F（c×d）ην（c×Fb（c）×Fb（d）F（g）JJFb（g）F（a）ηaFb（a）回想F（c）必须包括F（c）<$D1（ν（vt），c））/Rel和F（d）必须包括F（d）<$D1（ν（vt），d））/Rel，我们得出F（a）必须包括所有的F^（d）. 因此，F^（a）m不仅包括F（a），而且，例如，包括所有其它的F（a）。<其中x∈F（c），y∈F（d）.在这种情况下，为了使图可换，元素（F（πa（p））（z），F（πb（p））（z）），g>必须与任何F（g）（z）建立关系，其中z∈F（c×d）。<此外，F（a）必须包括（x，f2），g>，其中x∈F（a（p））且f2：v（vt）→d，或（f1，y），g><<其中y∈F（b（p））且f1：ν（vt）→c，或（f1，f2），g>其中当z1=-时，不存在任意的零元在任意对象M（v（vt））中，且z2= ）>. 在实践中如果给定的图态射F是一个模型，那么这样的树我们保持点和箭头的轨迹，这些点和箭头可以被适当地应用3.1.2树和相关关系在这里，我们展示了如何在算术universe内部构建所需的树。虽然我们在微积分中没有良好基础的树[15]CF法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105115一∈ ∈ ∈∈˜˜˜对于算术论域u，通过必要地使用列表，我们可以定义一些有用的归纳类型，如下面的命题所示，以满足我们的目的。回想一下，N类型是自然数的类型命题3.3在算术论域U的内部类型论中，我们可以定义一个类型n∈NR（n，s）型[s∈S]假设R（0，s）型[s∈S]在微积分中是可导的，R（n+ 1，s）∈SR（n，sJ）H（sJ，s）对于sS，nN，其中H（sJ，s）类型[s，sJS]在微积分中是可导的。此外，我们可以根据以下的排除和转换规则，通过归纳来论证类型：C（s，z）型[s∈S，z∈NR（n，s）]co（s，d）∈C（s，<0，d>）[s∈S，d∈R（0，s）]c1（s，SJ，ZJ，h，u）∈C（s，n+1，SJ，ZJ，h>）E）[s∈S，sJ∈S，n∈N，zJ∈R（n，sJ），h∈H（sJ，s），u∈C（sJ，n，zJ>）]El（c0，c1，s，z）∈C（s，z）[s∈S，z∈N∈R（n，s）]El（c0，c1，s，0，d>）=c0（s，d）∈C（s，0，d>）El（c0，c1，s，n+1，sJ，zJ，h>）=c1（s，sJ，zJ，h，El（c0，c1，sJ，n，zJ>>））∈C（s，n+ 1，sJ，zJ，h>）<证据 候选人类型为R（0，s） <$（<$w∈List<$（<$x∈S <$y∈S H（x，y）） R（0，π1（p1（w）&π2（plh（w）（w））= Ss&π1（front（w））=List（<$x∈S<$y∈SH（x，y））π2（back（w））其中，一般来说，List_n（A）表示A的非空列表的类型，pn（w）是列表w的第n个元素的投影，lh（w）是其中，π1是第一个射影π<$1（z）<$π1（z）∈S的提升对于z∈S∈H（x，y），π2是第二投影在π2（z）<$π1（π2（z））∈S对于z∈<$x∈S<$y∈SH（x，y）和front（w）取出从列表w中取出第一个元素，离开列表的前面，而back（w）从列表w中取出最后一个元素，留下剩下的尾部。Q通过3.3，我们可以证明：引理3.4（树）在U的内部类型理论中，我们可以定义一个类型Tree（F，v）[v∈V]116法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105U以下介绍规则，以形成其条款：（f）∈Tree（F，vt）p∈Px∈F0（a（p））y∈ F0（b（p））（x，y）∈Tree（F，vp）v∈ Vp∈Px∈F0（a（p）） W∈Tree（F，v） f∈D1（v（v），b（p））（x，w/f）∈ Tree（F，vp）v∈Vp∈Pw∈Tree（F，v）f∈D1（v（v），a（p））y∈F0（b（p））（w/f，y）∈Tree（F，Vp）v 1 ∈ Vv 2 ∈ Vp∈Pw 1 ∈Tree（F，v 1）w2 ∈Tree（F，v2）f1∈D1（ν（v1），a（p））f2∈D1（ν（v2），b（p）） （w1/f1，w2/f2）∈Tree（F，vp）此外，由于根据马丁-洛夫三点三然后，总是感谢道具。在图3.3中，我们可以定义一个类型，该类型包含所定义的树的分支，这些分支可能用箭头延伸，箭头终止于草图的任何对象，或者简单地用F值终止于草图对象。引理3.5（扩展分支）在的内部类型理论中，我们可以定义一个类型Bran（F，x）[x∈G0]以下介绍规则，以形成其条款：x∈G0u∈F0（x）/u∈Bran（F，x）x∈G0v∈V w∈Tree（F，v）f∈D1（v（v），x）w/f∈Bran（F，x）此外，由于马丁-洛夫类型理论[ 15 ]中所规定的相应的消元规则和转换规则，三点三此外，我们可以定义一个操作，它由一个左分支和一个适当的右分支组成一棵树：引理3.6在U的内部类型理论中，我们可以定义一个操作（z1，z2）∈Tree（F，vp）[p∈P，z1∈Bran（F，a（p）），z2∈Bran（F，b（p））]使得对于任意p∈P和任意树w∈Tree（F，vp），我们可以得到一个证明：<$z1∈Bran（F，a（p））<$z2∈Bran（F，b（p））（z1，z2）=Tree（F，vp）w然后，总是感谢prop.3.3，我们定义了一个分支上的关系，这将有助于正确地定义反射器：法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105117U（）/idy1∈ ∈ ∈∈∈ ∈ ∈∈∈ ∈J∈∈ ∈J∈11麸皮（女）2引理3.7（分支关系）在的内部类型理论中，我们可以定义归纳类型z1Bran（F）z2[x∈G0，z1∈Bran（F，x），z2∈Bran（F，x）]其形成规则如下：Tery∈F0（ν（vt））v（v t）麸皮（女）之三v ∈ V w ∈ Tree（F，v）f1∈ D1（ν（v），ν（vt））女1麸皮（女）（中文）/idv（vt）Prodp∈P bl∈Bran（F，a（p））br∈Bran（F，b（p））1（bl，br）/πa（p）麸皮（F）blProdp∈P bl∈Bran（F，a（p））br∈Bran（F，b（p））2（bl，br）/πb（p）麸皮（F）brProdp∈Pu∈F0（ν（vp））（F1（πa（p））（u），F1（πb（p））（u））/idv（vp）麸皮（F）uProdv∈Vw∈Tree（F，v）p∈Pg∈D1（ν（v），ν（vp））4（w/（πa（p）·g），w/（πb（p）·g））/idv（vp）麸皮（女）W/GProdp P bl Bran（F，a（p））blJ Bran（F，a（p））br Bran（F，b（p））x∈G0f∈ D1（v（vp），x）blBran（F）blJ5（bl，br）/f麸皮（女）（BLJ，br）/fProdp P bl Bran（F，a（p））br Bran（F，b（p））brJBran（F，b（p））x∈G0f∈ D1（v（vp），x）brBran（F）brJ6（bl，br）/f麸皮（女）（bl，brJ）/fCompv V wTree（F，v）x G0xJ G0uF0（xJ）f∈D1（v（v），x）h∈D1（xJ，x）w/fBran（F）uw/h·f麸皮（女）F1（h）（u）Compv1V w1 Tree（F，v1）v2V w2Tree（F，v2）xJ G0 xG0f1∈D1（v（v1）， x）f2∈D1（v（v2），xJ）h∈D1（xJ，x）w1/f1Bran（F）w2/f2w /h·fw/h·f 22312118法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105此外，在这种类型上，我们可以通过归纳法进行论证，这要归功于以prop风格制定的相应的消除和转换规则三点三法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105119∈Uˆ^^b0现在，为了定义反射器的对象部分，我们使用任意x上的扩展树的类型T（F）（x） G0定义为用草图箭头扩展的树与F0（x）的副本的余积：T（F）（x）v∈V Tree（F，v）×D1（v（v），x）注意，在下面我们将使用这个缩写：对于x∈G0，v∈V，w∈Tree（F，v），f∈D1（v（v），x）v<，w，f>>∈v∈V树（F，v）×D1（v（v），x）<然后，在扩展树上，我们基于分支关系定义一个关系：定义3.8[扩展树关系]在的内部语言中，我们定义类型zT（F）zJ[x∈G0，z∈T（F）（x），zJ∈T（F）（x）]对于x∈G0，z∈T（F）（x），ZJ∈T（F）（x），zT（F）zJ<$（<$u∈F0（x）z=T（F）（x）[inl（u）]&<$v∈V <$w∈Tree（F，v）<$f ∈D1（v（v），x）zJ= T（F）（x）[inr（）]&w/fBran（F）u）⊕（v1∈Vv2∈Vvw1∈Tree（F，v1） vw2∈Tree（F，v2） vf1∈D1（v（v1），x） vf2∈D1（v（v2），x）z=T（F）（x）[inr（v1，w1，f1>）]& zJ=T（F）（x）[inr（v2，w2，f2>）]&w1/f1Bran（F）w2/f2）3.2返回顶部反射函子（−）的定义：D（S，U）→Mod（S，U）如下。对于D（S，U）中的任何图态射F：S → U，我们将：定义3.9[Fon objects]对于每个x∈G0，我们定义F（x） F0（x）v∈V 树（F，v） × D1（v（v），x）T（F）定义3.10[Fon morphisms]对于任意g∈G1使得δ0（g）=x∈G0和δ1（g）=y∈G0，我们定义F^1（g）：F^0（x）−→F^0（y）120法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105^><ˆ˜^^^eFb1（g）（[z]）n>[inr（v，w， g·f>）] i f z = i n r（v，w，f>）or r v ∈ V<><>（αa（p）（x），αe（wJ）/h）ifw=（x，wJ/h）forx∈F0（a（p））andndv∈Vandndp∈P>（αe（w）/h，αb（p）（y））ifw=（w/h，y）fory∈F0（b（p））andndv∈Vandndp∈P>（αe（w1）/h1，αe（w1）/h2）ifw=（w1/h1，w2/h2）anndv1∈V，v2∈Vanndp∈P（αb）x（[z]）n>[inr（v，αe（w），f>）] ifz=inr（v，w，f>）orrv∈V：>个利用商型F0（x）上的消去法则：对任意z∈T（F）（x）8[inl（F1（g）（y））]ifz=inl（y）fory∈F0（x）：w∈Tree（F，v）且f∈D1（v（v），x）定义3.11[（−）关于自然变换]给定D（S，U）中的自然变换α：F−→H，我们定义一个自然变换α：F−→H在Mod（S，U）中，使用以下术语α（w）∈Tree（H，v）[v∈V，w∈Tree（F，v）]通过树w上的归纳定义如下：8>（）ifw=（）>（αa（p）（x），αb（p）（y））ifw=（x，y）forx∈F0（a（p）），y∈F0（b（p））andndp∈Pα（w）α>J>WJ∈Tree（F，v）和h∈D1（v（v），b（p））JWJ∈Tree（F，v）和h∈D1（v（v），a（p））w1∈Tree（F，v1）和h1∈D1（v（v1），a（p））w2∈Tree（F， v2）和 h2∈ D1（v（ v2），b（p））定义x∈G0上的任意分量的新方法是：（α^）x：F^0（x）−→H^0（x）由商类型的消去法则定义T（F）（x）F^（x）：对于每个z∈8[inl（αx（y））]ifz=inl（y）fory∈F0（x）：w∈Tree（F，v）且f∈D1（v（v），x）引理3.12F^是U中有限可分的FP-草图S的模型。证据 为了证明我们的陈述，使用定义的关系Bran（F）是至关重要的。在引理3.7中，用于定义F ^的对象部分的关系T（F）是基于该关系。>法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105121^^S → U D S U^对于Bran（F），在引理a3.7中，F^0（v（vp））是p∈P的pro导管，且请注意，由于Comp1，Comp2，F是一个定义良好的图态射F^1（πa（p））和F^1（πb（p））是ks到Prodi的映射，其中i=1，. ，6and在引理3.7中证明了Bran（F）的Compi，其中i= 1，2，并且由于引理3.7中Bran（F）的Ter1，Ter2，F0（ν（vt））同构于T。Q最后，我们将候选项定义为反射的单位，如下所示：定义3.13[单元]给定一个图态射F：in（，），我们定义一个自然变换ηF：F−→F^其分量（ηF）x：F0（x）−→F0（x）在x∈G0上定义如下：对于每个z∈F0（x）（ηF）x（z）[inl（z）]然后，我们定义候选人为附加的计数。定义3.14[计数]给定一个模型M∈Mod（S，U），我们将计数定义为自然变换εM：M^−→M通过使用术语Ap（M）（w）∈M0（v（v））[v∈V，w∈Tree（M，v）]在树W上的归纳定义如下：122法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105⎧⎪⎪⎪8>yifz=inl（y）fory∈M0（x）>1个⎪⎪⎪⎪⎪（εM）x（[z]）<$M（f）（Ap（M）（w）） 如果z=inr（）⎪⎪2∈ D1 2如果w=（x，w′/h）如果w=（w1/h1，w2/h2）如果w=（），则为Mifw=（x，y）其中x∈M0（a（p）），y∈M0（b（p）），p∈P⎪⎪Ap（M）（w）其中x∈M0（a（p））和ndw′∈Tree（M，v）且h∈D1（v（v），b（p）），其中v∈V，p∈P如果w=（w′/h，y）其中y∈M0（b（p））andw′∈Tree（M，v）和h∈D1（v（v），a（p）），其中v∈V，p∈P⎪其中w1∈Tree（M，v1），h1∈D1（v（v1），a（p）），w2∈Tree（M，v2），h （v（v），b（p））对于v1∈V，v2∈V，p∈P的连续性其中M是M0（v（vt））中的唯一元素，它必须是U中的终结对象。对于每个x∈G0，我们定义（εM）x：M^0（x）−→M0（x）通过对M^0（x）的限制规则：对于每个z∈T（M）（x），：>对于v∈V，w∈Tree（M，v）和df∈D1（v（v），x）根据所有这些定义，我们得出结论：定理3.15给定一个有限可判定的FP-草图S，包含函子J：Mod（S， U）→D（S，U）有函子（S-）：D（S，U）→Mod（S，U）法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105123^b bb bfb bf/作为左伴随。证据要证明D（S，U）中任意F图态射和x∈G0的三角恒等式（εF）x·（ηF）x=idF0（x）F1（f）·Ap（F）（ηF（w））=Fb0（x）[inrv，w，f>]为了得到这种类型的证明，我们利用草图的可判定有限性，通过包含G1的所有合适的箭头的量化，能够对树w进行归纳。 树w∈Tree（F，v）的归纳是关于类型C（w）∈List（B）（π1（l）=List（G1）g0g1. gn1）哪里B<$$>f∈G1（（δ0（f）=ν（v）F1（f）·Ap（F）（ηF（w））=Fb0（x）[inrv，w，f>]）<$δ0（f）/=ν（v） ）π1是列表上第一个投影的提升，而g0g1. gn1是G 1中所有箭头的列表，δ0（f）= ν（v）的定义归功于下式的可判定性：素描Q最后，作为推论，我们得到我们的主要定理：推论3.16给定一个有限可判定的FP-草图S，包含函子I：Mod（S，U）→US有一个左伴随证据我们认为Mod（S，U），MD（S，U），D（S，U）US通过rop3.1和第3.15个函数I=J·I得到了一个很好的结果。Q4结论对于算术论域内部的有限个可判定的lex-sketches，也可以通过构建更复杂的树来证明类似的反射。当然，我们可以在算术论域或其变体中研究更广泛的有限产品草图类的反射的存在性。我们认为，在局部封闭的算术论域中，反射应该适用于一般的内部有限产品草图，因为在本文中，草图的可判定有限性本质上只是用来量化草图箭头的子集。124法医Maietti/Electronic Notes in Theoretical Computer Science 122（2005）105这些反射可以用来建立理论的考虑草图[1]，但考虑算术宇宙作为我们的集合论宇宙的地方的范畴集。在这一点上，我们也想探索[7]中开发的技术的适用性。将来我们希望对于有限可判定的lex sketch也有上积余锥得到类似的结果，总是通过把算术论域或它的某些其他谓词变体作为我们的集合论域。实际上，我们最终希望有限