谓词纤维化与关系双范畴

我们调和了谓词逻辑中正则理论的两种不同范畴语义。构造了一个“正则纤维化”的2-范畴，以及“正则proarrow装备”的2-范畴，并证明两者等价。正则装备是满足某些公理的“笛卡尔装备”，而笛卡尔装备是笛卡尔双范畴的轻微推广。这是通过定义一个三范畴Biprof（其对象是双范畴，态射是取值于范畴的profunctor）来实现的，然后将装备定义为该三范畴中的伪幺半群（pseudo-monad）。将得到的装备概念与几个已有概念进行比较。最重要的是，这涉及证明Biprof中的每个伪幺半群都有Kleisli对象。我们确定了一个在局部离散基双范畴上的严格2-范畴装备，并将笛卡尔装备定义为该2-范畴中的笛卡尔对象。因此笛卡尔装备自身构成一个2-范畴，并证明它容许一个从正则纤维化2-范畴出发的2-完全忠实函子。该函子像中的笛卡尔装备被刻画为满足某些公理的那些，从而确定了一个与正则纤维化等价的“正则装备”的2-范畴。然后证明正则纤维化承认谓词的理解（comprehension）当且仅当其对应的正则装备承认态射的制表（tabulation），并且进一步，态射制表的存在等价于余幺半群（co-monads）的Eilenberg--Moore对象的存在。最后，我们结合前述内容简要考察了有效topos的两种不同构造，即通过triposes和通过assemblies。