🤖 AI

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

This paper presents the first machine-checked formalization in Cubical Agda of topos causal models, verifying core concepts like intervention as characteristic maps and sheaf gluing, while identifying and repairing a gap in Lawvere-Tierney axioms to establish the stability of Pearl's rules and demonstrating a contextuality obstruction within a safe, axiom-free framework.

Original authors: Karen Sargsyan

Published 2026-07-20

📖 7 min read🧠 Deep dive

CC BY 4.0

Original authors: Karen Sargsyan

Original paper licensed under CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

The Detective's Dilemma: Why Causality Needs a New Map

Imagine you are a detective trying to solve a mystery. You have a list of clues: "It rained," "The grass is wet," and "The sprinkler was on." In the past, scientists treated these clues like a simple list of facts. If the grass is wet, they might guess it rained. But real life is messier. What if you made the grass wet by turning on the sprinkler? Does that change the fact that it rained? This is the heart of causal inference: figuring out not just what happens together, but what causes what, especially when we intervene and change the rules of the game.

For decades, experts have used diagrams and math to track these cause-and-effect chains. But recently, a new idea emerged: what if we treat the entire world of causes not as a static picture, but as a shifting landscape that changes depending on where you are looking? This is the realm of Topos Theory, a branch of mathematics that studies how shapes and structures fit together. Think of it as a universal language for "gluing" pieces of information. If you have a puzzle where the pieces fit perfectly in your hands but don't make a complete picture when you try to put them on the table, that's a problem this new math tries to solve. The big question is: Can we use this high-level math to build a foolproof system for understanding cause and effect, even when we are changing the world by testing things?

The Paper's Journey: Building a Causal Lego Set

This paper is a massive, computer-checked construction project. The authors, led by Karen Sargsyan, took a bold new theory called "Topos Causal Models" and rebuilt it from the ground up inside a computer program called Cubical Agda. Think of this program as a super-strict Lego master that refuses to let you snap two bricks together unless the connection is mathematically perfect. The goal was to verify a theory proposed by a researcher named Mahadevan, which suggests that we can describe the entire universe of cause-and-effect using the rules of a "Topos" (a mathematical universe).

The authors didn't just copy the theory; they tested it, fixed it, and found things the original author missed. Here is what they discovered, explained through the lens of their digital construction site.

1. The "Do-Button" and the Truth Filter

In the original theory, an intervention (like forcing a variable to be a specific value, written as do(X = x)) is described as a special "characteristic map." Imagine you have a giant map of a city (the causal world). If you want to force a specific street to be closed, you don't just erase the street; you draw a special "truth filter" over the map. This filter highlights exactly where the street is closed and nowhere else.

The authors built this filter in their computer code. They proved that this filter works exactly as promised: it perfectly identifies the "closed street" and nothing else. They showed that this isn't just a clever trick; it's a fundamental rule of this mathematical universe. If you try to force a value that doesn't fit the natural flow of the map, the system rejects it. This confirms that the "Do-Button" is a solid, reliable tool in this new framework.

2. The Glue That Sometimes Fails

One of the most exciting promises of the original theory was Sheaf Gluing. Imagine you have three different detectives looking at a crime scene from three different angles. If Detective A agrees with Detective B, and Detective B agrees with Detective C, you might assume they all agree on the whole picture. In this math, "gluing" means taking these local views and snapping them together into one giant, global truth.

The authors proved that for two detectives, this always works. If their views overlap and match, they can be glued together perfectly. However, they found a glitch when three or more detectives are involved. They constructed a scenario (a "Specker's triangle") where every pair of detectives agrees perfectly, but when you try to combine all three, the picture falls apart. There is no single global story that fits all the local clues. This is a "contextuality obstruction." It's like having three puzzle pieces that fit together in pairs, but when you try to put them all on the table, they form a hole in the middle. The authors proved this isn't a bug in their code; it's a real feature of the math. It means that in complex causal systems, just because local parts agree doesn't mean a global solution exists. You need a global check, not just local ones.

3. Fixing the "Magic Modality"

The theory uses a special tool called a Lawvere-Tierney topology (let's call it a "Magic Modality") to decide which causal facts are "stable" or "true" across different situations. The original paper listed three rules for this magic tool. The authors ran the numbers and found a problem: those three rules weren't enough! They found a weird, three-step ladder where the tool followed all three rules but still broke the logic (it wasn't "inflationary," meaning it didn't always keep things the same or bigger).

They fixed this by adding a fourth rule. With this new rule, the magic tool works correctly. They then showed that this tool makes the "Do-calculus" (the rules for calculating cause-and-effect) stable. No matter how you slice the world or change the perspective, the core rules of causality hold firm. They even showed a specific example of this "magic" in action: the "double-negation" topology, which acts like a filter that turns fuzzy, uncertain truths into clear, classical facts.

4. Transporting Truth Across Worlds

Finally, the authors tackled Transportability: Can a rule we learn in one world (like a hospital in Tokyo) be trusted in another (a clinic in New York)? In their framework, moving a causal fact from one place to another is the same as checking if it is "stable" under the Magic Modality. If a fact is stable, it travels safely. If it's not stable, it might break when you move it. They proved that for certain types of facts (like those involving interventions), this stability is guaranteed. However, they noted that for more complex, real-world scenarios where facts might change values between worlds, the math gets trickier and requires more work to fully solve.

The Bottom Line

This paper is a triumph of verification. It didn't just say, "This theory looks cool." It built the theory in a computer, forced it to follow strict logical rules, and found that:

The "Do-Button" works perfectly as a truth filter.
Local agreements can sometimes fail to make a global truth (the "three detectives" problem).
The original rules for the "Magic Modality" were incomplete and needed a fourth rule to work.
Once fixed, the system proves that causal rules are stable and can be transported across different environments.

The authors are very sure about these results because they are machine-checked. Every single step was verified by the computer, with no assumptions or "maybe" moments. They didn't just simulate this; they proved it mathematically. However, they are careful to say this is just the "1-topos" version (a specific, simpler kind of mathematical universe). They haven't solved the entire problem of causality yet, especially the parts involving directed arrows (where A causes B, but B doesn't cause A) in a fully asymmetric way. But for the part they tackled, they have built a rock-solid foundation, proving that the math behind causal models is not just a pretty idea, but a verified, working reality.

Technical Summary: A Cubical Formalisation of Topos Causal Models

Problem and Motivation
The paper addresses the verification of "Topos Causal Models" (TCMs), a framework proposed by Mahadevan [Mah25c, Mah25b, Mah25a] that recasts causal inference within the category of a topos. In this framework, a causal world is a presheaf, interventions are characteristic maps into the subobject classifier $\Omega$ , and reasoning occurs in the intuitionistic internal language. While the source material provides a conceptual reformulation where standard causal machinery (intervention, mechanism assembly, counterfactuals) corresponds to topos-theoretic universal properties, it remains a paper-based development. Key central claims in the source are stated without proof, and some axioms are left abstract or potentially incomplete. The problem is to provide a machine-checked verification of this 1-topos core, ensuring the logical consistency of the framework and identifying any gaps in the original axiomatic presentation.

Methodology
The authors implement the formalisation in Cubical Agda, a proof assistant based on cubical type theory. The development is a direct sequel to a companion paper [Sar26] which verified a probability monad and Pearl's do-calculus rules.

Foundations: The work operates over the presheaf topos $\mathbf{PSh}(\mathcal{C}) = \mathbf{Set}^{\mathcal{C}^{op}}$ over an abstract base category $\mathcal{C}$ of contexts.
Safety and Axioms: The entire development typechecks under Agda's --safe flag, meaning it contains no postulates, holes, or unsafe features. The underlying ordered field is concretely instantiated as the rational numbers $\mathbb{Q}$ , avoiding abstract postulates.
Structure: The formalisation builds the subobject classifier $\Omega$ as a presheaf of sieves, defines the internal language via Kripke-Joyal forcing, and constructs a Lawvere-Tierney topology to model the $j$ -do-calculus modality.

Key Contributions and Results

The Intervention Classifier (Section 3):
The authors construct $\Omega$ as the presheaf of sieves and realise the intervention $do(X := x_0)$ as a characteristic map $\chi: X \to \Omega$ . They prove the classification theorem in both directions: $\chi_c(b) = \top \iff b = x_0^c$ . Crucially, they establish that for the construction to be topos-internal, the fixed value $x_0$ must be a natural global element (a value natural in the context), not merely a context-indexed family. This proves that $\Omega$ is the subobject classifier, satisfying the universal property that every restriction-closed sub-presheaf is uniquely classified by a map into $\Omega$ .
Sheaf Gluing of Independent Mechanisms (Section 4):
The source material asserts that local mechanisms agreeing on overlaps can be "collated" into a unique global mechanism but provides no proof. The authors prove this as a pullback limit in the presheaf topos. They demonstrate that for two mechanisms $p: X \to Z$ and $q: Y \to Z$ , the pullback $X \times_Z Y$ exists contextwise, and any cone of agreeing mechanisms factors uniquely through this pullback. This confirms the "gluing" property without requiring a Grothendieck topology or sheafification, as it holds for all presheaves.
The Internal Language (Section 5):
The paper defines Kripke-Joyal forcing for the internal logic and machine-checks the clauses for all connectives ( $\top, \bot, \land, \lor, \Rightarrow$ ) and quantifiers ( $\forall, \exists$ ). They verify the locality (monotonicity) property, ensuring that forcing is stable under restriction, which is the defining characteristic of Kripke semantics.
Correction of the Lawvere-Tierney Axioms (Section 6):
A significant finding is a gap in the standard definition of a Lawvere-Tierney topology provided in the source. The three standard axioms (preservation of $\top$ , preservation of $\land$ , and idempotence) do not entail inflationarity ( $S \leq j(S)$ ). The authors provide a counter-model (a three-element chain) satisfying the three axioms where inflationarity fails, meaning the operator is not necessarily a closure operator. They add inflationarity as a fourth axiom to ensure $j$ is a closure operator (nucleus).
- Concrete Instance: They exhibit the double-negation topology ( $\neg\neg$ ) as a non-degenerate concrete instance.
- Stability: They prove that interventions and Pearl's three do-calculus rules are $j$ -closed (stable) for every topology. However, they note this is trivial for rules whose conclusions are proven equalities (truth value $\top$ ). The substantive result concerns contingent claims (e.g., conditional independences that hold in some regimes but not others), showing that their truth values are $j$ -closed under the double-negation topology.
Contextuality Obstruction (Section 7):
The authors introduce a phenomenon not considered in the original programme: a cohomological obstruction to gluing. While two mechanisms always glue, three contexts can fail to admit a global model even if they are pairwise consistent. They machine-check Specker's triangle (three Boolean observables with pairwise anti-correlations) as a minimal witness.
- They formalise the obstruction as a non-zero class in the first Čech cohomology ( $H^1$ ) of the cover with $\mathbb{Z}_2$ coefficients.
- They prove that a global section exists if and only if the holonomy of the cocycle is trivial. Specker's triangle has non-trivial holonomy, confirming the absence of a global model.
Transportability as Invariance (Section 8):
The paper identifies transportability of a counterfactual across a cover of regimes with $j$ -stability (invariance). A counterfactual holds globally (is transportable) if and only if its internal truth value is $j$ -closed. They prove soundness: if a counterfactual is $j$ -stable and holds in a $j$ -dense environment, it holds globally.

Significance and Claims
The paper claims significance in two primary areas:

Assurance: The central claims of the TCM framework are now certified rather than asserted. This is critical for automation, as a verified core is necessary to check machine-generated causal models.
Practical Findings: The mechanisation revealed two practical insights:
- The guarantees of the modal layer depend on $j$ being a closure operator; the original axioms were insufficient.
- Modular assembly of causal mechanisms (map-reduce style) is not guaranteed by pairwise agreement alone; a global consistency check is required to detect cohomological obstructions (contextuality).

Scope and Limitations
The authors explicitly limit the scope to the 1-topos (presheaf) fragment.

They do not formalise type-level sheafification (the associated-sheaf reflector on the whole topos).
They do not address the directed or $\infty$ -categorical lift of the framework, which would require directed type theory to model the asymmetry of causation (causal arrows are symmetric in the current presheaf model).
The transportability result is established as an equivalence with invariance under a specific density hypothesis, but the completeness equivalence with the graphical $s$ -hedge criterion remains future work.

The development is openly available and represents the first machine-checked account of the 1-topos core of topos causal models, correcting the modal axioms and proving previously unverified gluing and obstruction properties.