# A cubical formalisation of topos causal models: intervention, forcing, and a contextuality obstruction

arXiv: https://arxiv.org/abs/2607.15629 · HTML: https://mlsanity.com/paper/2607.15629/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 5 of its 29 references that are in the map.
- First posted on arXiv 17 Jul 2026.

## Builds on (most cited first, 5 of 5)

- [Intuitionistic j-Do-Calculus in Topos Causal Models](https://mlsanity.com/paper/2510.17944/) (2025)
- [Unveiling the Structure of Do-Calculus Reasoning via Derivation Graphs](https://mlsanity.com/paper/2606.03719/) (2026)
- [The Topology of Causality](https://mlsanity.com/paper/2303.07148/) (2023)
- [Directed univalence in simplicial homotopy type theory](https://mlsanity.com/paper/2407.09146/) (2024)
- [A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness](https://mlsanity.com/paper/2606.20351/) (2026)

## Abstract (arXiv)

Topos causal models recast causal inference inside a topos: a causal world is a presheaf, an intervention is a sub-model named by a characteristic map into the subobject classifier Om, and reasoning is Kripke-Joyal forcing in an intuitionistic internal language. We give the first axiom-free machine-checked account of this 1-topos core, in Cubical Agda over a previously verified probability monad and do-calculus; the framework is otherwise developed on paper, with central claims stated rather than proved. Three of our results go beyond faithful transcription. We exhibit a contextuality obstruction the programme does not treat: pairwise-consistent local causal data with no global model, detected by a degree-one holonomy class. We delimit the claim that interventions are modelled by the subobject classifier: an intervention and an observation name the same subobject, so Om fixes the target of a do-operation but not the operation itself, which is surgery on the kernels --- where, on a confounder, the interventional and observational laws differ. And we settle the modal unit --- inflationarity is derivable from jtop = top and naturality, not a fourth axiom. We also machine-check the classifier of sieves with its classification theorem, the pullback collating local mechanisms, and the Kripke-Joyal forcing clauses. The development assumes no axioms and typechecks under Agda's texttt--safe flag, with the ordered field discharged at mathbbQ; type-level sheafification and a directed do-calculus are future work.