合成域理论中的拓扑及其在Agda中的形式化
Topology in Synthetic Domain Theory and its Formalisation in Agda
浏览论文内容
中文总结 AI 辅助
研究合成域理论中Phoa原理，通过定义对偶单形、脊和清醒同构概念给出新解释，提出假设完备性定理，还包括区间类型公理抽象及主要定理形式化证明。
中文摘要 AI 辅助
本项目研究合成域理论（SDT）中的Phoa原理，并将其推广到超限情形。Phoa原理在SDT中通过展示路径如何给出区间类型及其他代数结构上的信息序而发挥关键作用。项目定义了对偶单形和脊，并引入清醒同构概念，这有助于对Phoa原理及其推广进行新解释。最后，基于对Phoa原理的研究提出一个可能统一SDT中Segal完备性和链完备性的假设完备性定理。项目还包括在立方Agda中对区间类型进行公理抽象及对主要定理的形式化证明。
英文摘要
This project investigates the Phoa principle in synthetic domain theory (SDT), and provides a generalisation to the transfinite cases. The Phoa principle plays a pivotal role in SDT by illustrating how the paths give the information order on the interval type and other algebraic structures in SDT. The project defines the dual simplices and spines and introduces the concept of sobriomorphisms, which contributes to a new interpretation of the Phoa principle and its generalisations. Finally, the project proposes a hypothetical completeness theorem that may unify the Segal completeness and the chain completeness in SDT based on investigations on the Phoa principle in the project. The project also includes axiomatisation of the interval type in Cubical Agda and the formalised proof for the main theorems.
