aiqbench analysis
This paper establishes the first axiom-free, machine-checked formalization of topological causal models using Cubical Agda, rigorously verifying core concepts like Kripke-Joyal forcing and do-calculus. Beyond faithful transcription, it identifies a previously unaddressed contextuality obstruction where pairwise-consistent local data lacks a global model and clarifies that interventions correspond to surgery on kernels rather than simple subobject classifications. These foundational advances in categorical logic provide essential theoretical grounding for building robust, formally verified causal inference systems resistant to confounding variables.
A cubical formalisation of topos causal models: intervention, forcing, and a contextuality obstruction
arXiv:2607.15629v2 Announce Type: replace-cross Abstract: 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 $j\top = \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 $\mathbb{Q}$; type-level sheafification and a directed do-calculus are future work.
Abstract: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 $j\top = \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 $\mathbb{Q}$; type-level sheafification and a directed do-calculus are future work.
Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI); Category Theory (math.CT)
arXiv:2607.15629 [cs.LO]
(or arXiv:2607.15629v2 [cs.LO] for this version)
https://doi.org/10.48550/arXiv.2607.15629 Focus to learn more arXiv-issued DOI via DataCite
arXivLabs is a framework that allows collaborators to develop and share new arXiv features directly on our website.
Both individuals and organizations that work with arXivLabs have embraced and accepted our values of openness, community, excellence, and user data privacy. arXiv is committed to these values and only works with partners that adhere to them.
Have an idea for a project that will add value for arXiv's community? Learn more about arXivLabs.
Full text under the publisher's open licence · 327 words
Related coverage
A cubical formalisation of topos causal models: intervention, sheaf gluing, and the intuitionistic do-calculus
arXiv · Jul 20, 2026
Does Your LLM Trust You?
LessWrong · Aug 4, 2026
Game Design Creativity evals
LessWrong · Oct 12, 2026
Position, Not Provenance: Separating Reasoning Mediation from Sycophancy in Medical Vision-Language Models
arXiv · Jul 31, 2026