Topos causal models recast causal inference inside a topos: a causal world is a presheaf, an intervention is a characteristic map into the subobject classifier, and reasoning is carried out in the intuitionistic internal language. We give the first machine-checked account of this 1-topos core, in Cubical Agda, over a previously verified probability monad and do-calculus. We build the classifier of sieves and realize the intervention $ ext{do}(X := x_0)$ as a characteristic map with its classification theorem; prove the sheaf gluing of independent mechanisms, which the source asserts but never proves; and machine-check the Kripke-Joyal forcing clauses of the internal language. In the modal layer, we find and repair a gap: the three standard Lawvere-Tierney axioms do not force a closure operator. With the missing law restored, we exhibit the double-negation topology as a concrete instance and show that interventions and Pearl's rules are stable under every topology. Transportability of a counterfactual across a cover of regimes then coincides with this $j$-stability, understood as invariance across the cover. We further add a phenomenon the program does not consider: a machine-checked contextuality obstruction, where pairwise-consistent local data admit no global model. The development assumes no axioms and typechecks under Agda's --safe flag, with the ordered field discharged concretely at $ ext{Q}$; the scope is the presheaf (1-topos) fragment, with type-level sheafification and the directed lift left to future work.
Blogger's Review: This paper presents a novel perspective on causal inference through machine-checked formalization, highlighting the potential application of intuitionistic logic in complex systems. The repair of the Lawvere-Tierney axioms and the introduction of double-negation topology are refreshing, suggesting profound implications of the interplay between topology and causal inference. Future research could further explore its applicability in real-world models.