Coalgebras 的自然显示拓扑

拓扑学中的一个经典结果表明，针对 topos 上的笛卡尔 comonad 的 coalgebras 范畴仍然是 topos (Kock 和 Wraith, 1971)。有必要将此结果细化到包括宇宙的拓扑语境中。为此，我们引入自然显示拓扑和自然笛卡尔显示 comonad 的概念，并表明自然显示拓扑上针对自然笛卡尔显示 comonad 的 coalgebras 的自然模型仍然是自然显示拓扑。作为一个应用，这个结果将 Hofmann 和 Streicher (1997) 的宇宙方法从 presheaf toposes 扩展到具有足够点的 sheaf toposes。与自然显示拓扑提供扩展型 Martin-Löf 类型论的范畴语义相反，我们也证明了我们的主要结果在更一般的自然 typoses 范畴中成立，这涵盖了 intensional Martin-Löf 类型论的模型。自然笛卡尔显示 comonad 可用于作为依赖类型论的模型，引入 S4 盒子算子或 comonadic 模态 (如 Nanevski 等人, 2008 所述)。被视为困难处理的模态语境在本方法中被解释为 coalgebras 的自然 typoses 中的语境。我们概述了该方法中的解释。在上述框架内，我们引入了对自然模型（见 Awodey, 2018）的一种细化，这种细化严格等价于 full, split comprehension category（见 Jacobs, 1993），而非 Cartmell (1978) 的 category with attributes。