Several different topoi have played an important role in the development and applications of synthetic guarded domain theory (SGDT), a new kind of synthetic domain theory that abstracts the concept of guarded recursion frequently employed in the semantics of programming languages. In order to unify the accounts of guarded recursion and coinduction, several authors have enriched SGDT with multiple "clocks" parameterizing different time-streams, leading to more complex and difficult to understand topos models. Until now these topoi have been understood very concretely qua categories of presheaves, and the logico-geometrical question of what theories these topoi classify has remained open. We show that several important topos models of SGDT classify very simple geometric theories, and that the passage to various forms of multi-clock guarded recursion can be rephrased more compositionally in terms of the lower bagtopos construction of Vickers and variations thereon due to Johnstone. We contribute to the consolidation of SGDT by isolating the universal property of multi-clock guarded recursion as a modular construction that applies to any topos model of single-clock guarded recursion.

翻译：在合成守护域理论（SGDT）的发展与应用中，多种不同的拓扑斯扮演了重要角色。SGDT是一种新型的合成域理论，其抽象化了编程语言语义中常用的守护递归概念。为统一对守护递归和余归纳的阐释，多位研究者通过在SGDT中引入参数化不同时间流的多个“时钟”对其进行扩充，从而形成了更复杂且难以理解的拓扑斯模型。迄今为止，这些拓扑斯一直被具体地理解为预层范畴，而关于这些拓扑斯所分类的理论的逻辑-几何问题仍未得到解答。我们证明，SGDT的若干重要拓扑斯模型分类了极为简单的几何理论，并且向多种形式的多时钟守护递归的过渡可被更组合化地重新表述，其基于Vickers提出的下束拓扑斯构造及Johnstone对此构造的变体。通过将多时钟守护递归的泛性质分离为一种可应用于任意单时钟守护递归拓扑斯模型的模块化构造，我们为SGDT的整合做出了贡献。