A cubical formalisation of topos causal models: intervention, sheaf gluing, and the intuitionistic do-calculus

• URL: http://arxiv.org/abs/2607.15629v1
• Date: Fri, 17 Jul 2026 05:05:31 GMT
• Title: A cubical formalisation of topos causal models: intervention, sheaf gluing, and the intuitionistic do-calculus
• Abstract summary: We give the first machine-checked account of a 1-topos core, in Cubical Agda.<n>We show that interventions and Pearl's rules are stable under every topology.<n>We add a phenomenon the programme does not consider: a machine-checked contextuality obstruction.
• Score: 5.076419064097734
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Intrinsic Structure: Spectral Identifiability for Mechanistic Interpretability [51.56484100374058]
  We prove the first identifiability theorem for a mechanistic-interpretability primitive.<n>The spectrum is an identifiable, model-intrinsic fingerprint with a stated error bar, not a legible decomposition.
  arXiv  Detail & Related papers  (2026-08-10T19:42:01Z)
• Infinitesimal Causality [1.3295383263113112]
  IDC captures the infinitesimal layer in which interventions act as tangent deformations of copy/discard structure.<n>Key observation is that for structural causal models, infinitesimal causality is most naturally formulated in the slice of deterministic mechanisms over visible kernels.
  arXiv  Detail & Related papers  (2026-06-23T14:20:20Z)
• The Need for an External Observer Formalizing the Sufficiency Gap: A Mathematical Extension of Mixture Identifiability and Contextual Grounding in Sequence Models [0.0]
  We construct a binary mixed-regime process with one deterministic textual regime and one random regime governed by an unobserved latent state.<n>The resulting entropy difference is not an ordinary optimization error; it is a sufficiency gap caused by marginalization over an unobserved state.<n>A corrective signal reverses the posterior odds induced by the textual history exactly when its fidelity exceeds the text-only posterior weight assigned to the misleading regime.
  arXiv  Detail & Related papers  (2026-05-26T08:53:11Z)
• Sheaf-Theoretic Transport and Obstruction for Detecting Scientific Theory Shift in AI Agents [0.0]
  This paper develops a finite sheaf-theoretic framework for detecting theory-shift candidates through transport and obstruction.<n>We evaluate the framework on a controlled transition-card benchmark designed to separate deformation within a source language from extension of that language.
  arXiv  Detail & Related papers  (2026-05-13T18:46:17Z)
• Cohomological Obstructions to Global Counterfactuals: A Sheaf-Theoretic Foundation for Generative Causal Models [7.073238726507493]
  We formalize structural causal models as cellular sheaves over Wasserstein spaces.<n>To ensure tractability, we introduce entropic regularization and derive the Entropic Wasserstein Causal Sheaf Laplacian.<n>Our framework successfully leverages thermodynamic noise to navigate topological barriers in high-dimensional scRNA-seq counterfactuals.
  arXiv  Detail & Related papers  (2026-03-18T06:07:07Z)
• Intuitionistic $j$-Do-Calculus in Topos Causal Models [1.3295383263113112]
  We generalize Pearl's do-calculus to an Intuitionistic setting called $j$-stable causal inference inside a topos of sheaves.<n>Our framework is an elaboration of the recently proposed framework of Topos Causal Models (TCMs), where causal interventions are defined as subobjects.
  arXiv  Detail & Related papers  (2025-10-20T17:12:17Z)
• Gumbel Counterfactual Generation From Language Models [64.55296662926919]
  We show that counterfactual reasoning is conceptually distinct from interventions.<n>We propose a framework for generating true string counterfactuals.<n>We show that the approach produces meaningful counterfactuals while at the same time showing that commonly used intervention techniques have considerable undesired side effects.
  arXiv  Detail & Related papers  (2024-11-11T17:57:30Z)
• Neuro-Symbolic Entropy Regularization [78.16196949641079]
  In structured prediction, the goal is to jointly predict many output variables that together encode a structured object. One approach -- entropy regularization -- posits that decision boundaries should lie in low-probability regions. We propose a loss, neuro-symbolic entropy regularization, that encourages the model to confidently predict a valid object.
  arXiv  Detail & Related papers  (2022-01-25T06:23:10Z)
• Nested Counterfactual Identification from Arbitrary Surrogate Experiments [95.48089725859298]
  We study the identification of nested counterfactuals from an arbitrary combination of observations and experiments. Specifically, we prove the counterfactual unnesting theorem (CUT), which allows one to map arbitrary nested counterfactuals to unnested ones.
  arXiv  Detail & Related papers  (2021-07-07T12:51:04Z)
• Causal Expectation-Maximisation [70.45873402967297]
  We show that causal inference is NP-hard even in models characterised by polytree-shaped graphs. We introduce the causal EM algorithm to reconstruct the uncertainty about the latent variables from data about categorical manifest variables. We argue that there appears to be an unnoticed limitation to the trending idea that counterfactual bounds can often be computed without knowledge of the structural equations.
  arXiv  Detail & Related papers  (2020-11-04T10:25:13Z)
• A Weaker Faithfulness Assumption based on Triple Interactions [89.59955143854556]
  We propose a weaker assumption that we call $2$-adjacency faithfulness. We propose a sound orientation rule for causal discovery that applies under weaker assumptions.
  arXiv  Detail & Related papers  (2020-10-27T13:04:08Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.