A cubical formalisation of topos causal models: intervention, sheaf gluing, and the intuitionistic do-calculus
Logic in Computer ScienceArtificial Intelligence
Summary
The authors provide the first computer-verified formalization of a topos-based approach to causal reasoning using the Cubical Agda proof assistant. They represent causal worlds as presheaves and model interventions as characteristic maps, proving key properties that were previously asserted without proof. They identify and fix a missing law in the modal layer’s axioms, show stability of interventions under various topologies, and introduce a machine-checked example where local data cannot form a global consistent model. Their work is fully constructive and verified without extra assumptions, focusing on the fundamental 1-topos structure.
Authors
Karen Sargsyan
Abstract
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 realise the intervention $\mathrm{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 programme 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 $\mathbb{Q}$; the scope is the presheaf (1-topos) fragment, with type-level sheafification and the directed lift left to future work.