拓扑因果模型将因果推断重构于拓扑空间内：因果世界是一个预层，干预是一个特征映射到子对象分类器，推理在直觉主义内部语言中进行。我们在Cubical Agda中首次机器检查了这一1-拓扑核心，基于先前验证的概率单子和因果演算。我们构建了筛子的分类器，并将干预 $ ext{do}(X := x_0)$ 实现为一个特征映射及其分类定理；证明了独立机制的层粘合，这在源文献中提出但未被证明；并机器检查了内部语言的Kripke-Joyal强迫条款。在模态层中，我们发现并修复了一个缺口：三个标准的Lawvere-Tierney公理并不强制闭包算子。随着缺失法则的恢复，我们展示了双否定拓扑作为一个具体实例，并表明干预和Pearl规则在每种拓扑下都是稳定的。跨越状态覆盖的反事实的可传输性与这种 $j$-稳定性相吻合，理解为跨覆盖的不变性。我们进一步添加了一个程序未考虑的现象：机器检查的上下文障碍，其中成对一致的局部数据不允许存在全局模型。该开发不假设任何公理，并在Agda的 --safe 标志下进行类型检查，具体在有序域 $ ext{Q}$ 下被处理；范围为预层（1-拓扑）片段，类型级层化和有向提升留待未来工作。
博主点评： 本文通过机器检查的形式化方法，为因果推断提供了新的视角，展示了直觉主义逻辑在复杂系统中的应用潜力。对Lawvere-Tierney公理的修复和双否定拓扑的引入，令人耳目一新，预示着拓扑与因果推断结合的深远影响。未来的研究可以进一步探索其在真实世界模型中的适用性。