合成守卫域论中的分类拓扑斯

若干不同的拓扑斯在合成守卫域论（SGDT）的发展与应用中发挥了重要作用，SGDT是一种新型合成域论，抽象了编程语言语义中频繁使用的守卫递归概念。为统一守卫递归与余归纳的表述，若干作者为SGDT增添了参数化不同时间流的多个“时钟”，导致了更为复杂且难以理解的拓扑斯模型。迄今这些拓扑斯作为预层范畴被非常具体地理解，而这些拓扑斯分类何种理论的逻辑-几何问题一直悬而未决。我们表明，SGDT的若干重要拓扑斯模型分类非常简单的几何理论，且通向各种形式多时钟守卫递归的过程可更组合地依据Vickers的下bagtopos构造及Johnstone对此的变体重新表述。我们通过将多时钟守卫递归的泛性质孤立为一种适用于任何单时钟守卫递归拓扑斯模型的模块化构造，助力SGDT的巩固。