Pith. sign in

REVIEW 3 major objections 6 minor 13 references

The paper gives a machine-checked account of topos causal models showing that the subobject classifier names only the target of an intervention, and that pairwise-consistent local causal data can lack any global model.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

A Cubical Agda formalisation verifies the classifier, forcing and modal do-calculus of topos causal models, and adds a machine-checked contextuality obstruction for pairwise-consistent local models.

T0 review reviewed 2026-08-04 challenge →

load-bearing objection Serious, carefully scoped mechanisation of topos causal models; the headline assurance rests on an unpinned companion development, so the central claims are conditional on external artifacts. the 3 major comments →

arxiv 2607.15629 v2 pith:624W7VO3 submitted 2026-07-17 cs.LO cs.AImath.CT

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

Karen Sargsyan This is my paper
classification cs.LO cs.AImath.CT MSC 03B3503G3018B2568V20
keywords topos causal modelssubobject classifierKripke-Joyal forcingLawvere-Tierney topologydo-calculuscontextualitycohomological obstructionmachine-checked proof
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper tries to establish that the core of topos causal models can be made axiom-free and machine-checked: causal worlds as presheaves, interventions as classified subobjects, and causal reasoning as Kripke-Joyal forcing in the internal logic. It claims and verifies three non-transcriptive results. The subobject classifier names the target of an intervention but not the operation: intervention and observation classify the same subobject, and on a confounder the interventional law differs from the conditional law. The modal unit of a Lawvere-Tierney topology is derivable from naturality and j⊤=⊤, not a missing fourth axiom. Finally, pairwise-consistent local causal data over three contexts can admit no global model, a contextuality obstruction detected by a degree-one holonomy class; a sympathetic reader cares because the framework's central claims stop being asserted and become checkable, and because modular causal discovery needs a global consistency check that pairwise agreement cannot provide.

Core claim

The central claim, on the paper's own terms, is that the presheaf topos over the category of contexts carries a verified account of causal intervention: the sieve-valued subobject classifier Ω classifies the value-fixing subobject 'X = x0' with a characteristic map, but that same map also classifies the same subobject when the value is merely observed. So Ω fixes only the target of a do-operation; the operation itself is kernel surgery, and the paper machine-checks that on a pure confounder the interventional law differs from the conditional law. It also establishes that inflationarity S ≤ jS is a theorem for a topology on the classifier, not an additional axiom, and that a compatible family

What carries the argument

The load-bearing object is the subobject classifier Ω of a presheaf topos, realized as the presheaf of sieves that names sub-presheaves by characteristic maps; the paper defines the characteristic map χ for 'X = x0' and proves the classification theorem χ(b)=⊤ iff b=x0, along with the general universal property of Ω. The modal layer uses a Lawvere-Tierney topology j:Ω→Ω as a closure operator on truth values, and shows that its naturality together with j⊤=⊤ yields inflationarity. The obstruction is carried by a combinatorial cohomological criterion: the holonomy of a 1-cochain around a closed walk, which is trivial for coboundaries and nontrivial for the Specker triangle's pairwise anti-corre

Load-bearing premise

The load-bearing premise is that the companion paper's probability monad and do-calculus are sound: the present development takes them 'as given,' does not reproduce them, and does not pin them by commit, so a bug in those kernels would silently propagate into every machine-checked theorem about intervention and modality.

What would settle it

Exhibit a compatible family of local causal models over two measurement contexts that agrees on the overlap but has no global section; the paper's argument that two contexts always collate would then be wrong, and its three-context obstruction would not be minimal.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • The central claims of topos causal models become axiom-free machine-checked facts in the presheaf setting, rather than stated conjectures.
  • A topose-internal intervention must fix a natural global element, not merely a context-indexed family of values; otherwise the construction fails to be a classifiable subobject.
  • The do-operator differs from conditioning on a confounder, so the subobject-classifier picture cannot replace kernel-level surgery; both levels are needed.
  • On the subobject classifier, inflationarity requires no fourth topology axiom; formalisations that model topologies on a bare Heyting algebra would silently lose this property.
  • Modular assembly of local causal models from pairwise agreement alone cannot certify a global model; a global-consistency check is necessary.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the companion paper's probability monad or do-calculus is later found to contain an unsound step, the machine-checked theorems presented here inherit the error; pinning the dependency by a commit hash and re-checking both developments together would close that gap.
  • The cohomological criterion suggests a computational certificate for global inconsistency: check whether a proposed local-fit cochain has zero holonomy as a necessary condition for a global model; the triangle-versus-four-cycle contrast shows the criterion discriminates.
  • The directed asymmetric account's inability to formalise the do-operator points to a concrete target: a machine-checked directed-univalent universe would let intervention itself become a directed arrow, joining the undirected verified core.
  • The paper stops at invariance, not full transportability; if the full graphical transportability criterion is eventually formalised, effects that take different values across domains would break the identification with j-stability.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 6 minor

Summary. The paper reports a Cubical Agda formalisation of the 1-topos (presheaf) core of Mahadevan's topos causal models (TCM). It claims to machine-check, under Agda's --safe flag and with no axioms, the sieve classifier with its universal property, the classification of the value-fixing subobject 'X = x0', Kripke-Joyal forcing clauses, pullback collation of mechanisms, the distinction between do(X:=x0) and conditioning on a confounder, the derivability of inflationarity for Lawvere-Tierney topologies from naturality and j-top = top, and a Specker-triangle contextuality obstruction with a holonomy criterion. It also sketches a directed rzk fragment. The formalisation is explicitly built on the companion [Sar26] probability monad and Pearl do-calculus, which are taken as given; type-level sheafification, the full H^1 quotient, and the complete Lawvere-Tierney axioms for the intervention site are stated to be outside the formalised scope.

Significance. If the artifact is as described, this is a substantial and useful formalisation: it provides machine-checked versions of several standard topos-theoretic facts in a causal setting, and it is unusually explicit about what is and is not verified. The proofs that are presented in detail (classification theorem, inflationarity derivation, pullback universal property, holonomy criterion) are internally consistent and standard. The three beyond-transcription contributions — the delimitation of the classifier's role, the derivation of the modal unit, and the contextuality obstruction — are interesting. However, the headline verification claim cannot be independently confirmed from the manuscript alone: the central theorems inherit their correctness from the unpinned companion and repository, and at least one advertised theorem (transport soundness) is not stated precisely. These are fixable in revision.

major comments (3)
  1. [§2, §10] The central machine-checked claim is not self-contained. Section 2 explicitly takes the companion paper's probability monad and do-calculus 'as given', and Section 10 says the development is 'over' that companion layer; the artifact is a bare GitHub URL with no commit hash, no Agda/library versions, and no CI log. The theorems DoSeeDistinct, do-prior, do-classified, modal-rule1-3, and the contextuality results all depend on the companion's FDist monad laws, partial division, and Pearl-rule theorems. If any of those contain a definitional or logical error, every central theorem inherits it. The 'axiom-free' claim is thus only as strong as that unverified dependency. Please pin the artifact with a commit hash and versions, and either include the companion layer or give a precise interface/statement of the assumptions taken from it.
  2. [§7] The modal-stability contribution is weaker than the abstract suggests, and the paper itself says so. Section 7 ('What this does and does not show') states that modal-rulei would typecheck with the causal content deleted, because each rule's conclusion is a proved equality of distributions, hence has internal truth value top, and j-top = top is a topology axiom. The non-vacuous examples are degenerate or incomplete: ContingentCI/ModalCI sit on the discrete two-regime category, where Omega is Boolean and not-not is the identity, so every truth value is j-closed; InterventionSite is computed only at obs, with the coverage not formalised as a Grothendieck topology, the closure not a natural map Omega => Omega, and the Lawvere-Tierney axioms not checked. Please separate the fully verified part (derivability of inflationarity) from the vacuous stability theorems and the still-open non-degenera
  3. [§9] The transport-soundness theorem is not stated precisely. The text says 'We prove that for any topology in which the environment is j-dense — the identity lies in the closure of its sieve — a j-stable counterfactual that holds in the environment holds globally', but no formal statement is given: 'j-dense', 'holds in the environment', and 'holds globally' are not defined as precise type-theoretic statements, and the proof is only sketched via the density remark. The failure case and the completeness direction are admitted not to be machine-checked. This section needs a precise lemma statement (with the relevant module name) or the claims should be downgraded to 'sketched, not machine-checked'.
minor comments (6)
  1. [§6] The existential quantifier clause is stated as local pointwise existence, which is correct for presheaf toposes but differs from the cover-based clause one sees for sheaf toposes. A remark to this effect would avoid confusion.
  2. [§8] The sentence 'H^1 ∼= Z2 follows, though we do not formalise the quotient itself' is easy to misread as a machine-checked result. Please mark it clearly as an informal consequence, outside the scope of the formalisation.
  3. [§8] The example is called 'Specker's triangle', but the machine-checked object is the 3-cycle of perfect anti-correlations. Please clarify the relation to the usual quantum Specker triangle, or qualify the name.
  4. [§11] The rzk development assumes extension extensionality; the paper should state explicitly that the 'axiom-free' claim applies only to the Cubical Agda component, not to the directed fragment.
  5. [§7] In the record LawvereTierney, the derived monotonicity of j from meet-preservation is not mentioned in the text. A one-sentence explanation would help the reader see why the reflector presentation works.
  6. [References] The companion [Sar26] is central to the paper; please include its publication status or a stable version identifier beyond the arXiv number.

Circularity Check

0 steps flagged

No circular derivation chain: the paper's theorems are proved from explicit definitions, and its reliance on the companion [Sar26] is an external dependency rather than a circular reduction.

full rationale

I walked the claimed derivation chain. Section 3's classification theorem is a direct consequence of defining chi_c(b) as the sieve of arrows along which b restricts to x0; it is a verification of the subobject-classifier universal property, not a prediction derived from a fitted quantity. Section 4's DoSeeDistinct is an explicit computation inside the companion monad (interventional marginal p vs conditional marginal 1); it is an example/consistency check, and the paper does not claim to derive the companion's monad laws from it. Section 7's inflationarity theorem is proved from the record's jnat and j-top fields; naturality is part of the definition of a topology on Omega, so the proof is not circular. The paper itself concedes the modal-stability statements are top-vacuous (the proof depends only on the conclusion's truth value being top, not on the rule that produced it), which weakens their advertised content but is not a circular reduction. The contextuality obstruction is a finite case analysis for Specker's triangle, explicitly attributed to Abramsky-Brandenburger and Abramsky-Mansfield-Barbosa; the holonomy criterion is a standard coboundary/holonomy argument, with the H^1 iso Z2 quotient explicitly not formalised. The main caveat is not circularity: the formalisation takes the same-author companion [Sar26] as given for the probability monad and do-calculus, and the artifact is unpinned. That is a reproducibility/dependency risk, not a definitional or self-citation circularity, because the companion is an input layer claimed to be machine-checked rather than the conclusion being derived.

Axiom & Free-Parameter Ledger

0 free parameters · 6 axioms · 0 invented entities

No fitted parameters or invented entities: the numerical examples are constructed (e.g., p = 1/2), and the only new 'obstruction' is a standard cohomological criterion applied to a known example. The central mathematical work assumes trusted foundations, the companion monad, and the source framework's definitions.

axioms (6)
  • standard math Cubical Agda / cubical type theory and the Agda standard library are sound and correctly implemented
    The whole development is built inside this trusted proof assistant; no independent check is supplied.
  • domain assumption Companion probability monad and Pearl do-calculus formalisation [Sar26] are correct and available
    Section 2: 'We take all of this as given'; modules DoSeeDistinct, do-prior and do-classified compute inside that monad.
  • domain assumption Mahadevan's definitions of topos causal models, sieves, and the j-do-calculus are the intended target and are internally consistent
    Sections 2-3 restate Mahadevan's Def. 8/11/10; if the source's intervention notion differs, the formalisation may not address it.
  • standard math Mac Lane-Moerdijk Kripke-Joyal clauses are the reference semantics
    Section 6 verifies clauses from Mac Lane-Moerdijk VI.6.
  • domain assumption Abramsky-Brandenburger compatibility and global-section formalism applies to classical causal models
    Section 8 maps causal local models to empirical models; if causal models impose extra structure, the obstruction may not transfer.
  • domain assumption Extension extensionality in the rzk directed companion
    Section 11: the directed development assumes 'the library's extension extensionality'; it is not part of the --safe Agda core.

reviewed 2026-08-04 · how reviews work

0 comments
Cite this review

Pith. "Pith review of A cubical formalisation of topos causal models: intervention, forcing, and a contextuality obstruction." pith.science (2026). https://pith.science/paper/624W7VO3

@misc{pith2026260715629,
  author       = {Pith},
  title        = {Pith review of: A cubical formalisation of topos causal models: intervention, forcing, and a contextuality obstruction},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/624W7VO3}},
  note         = {Machine review of arXiv:2607.15629}
}
Share X Bluesky LinkedIn Reddit HN
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.

Review history (2 revisions) →

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

13 extracted references · 5 linked inside Pith

  1. [8]

    Intuitionistic j-do-calculus in topos causal models.arXiv preprint arXiv:2510.17944v2,

    [Mah25a] Sridhar Mahadevan. Intuitionistic j-do-calculus in topos causal models.arXiv preprint arXiv:2510.17944v2,

    Pith/arXiv arXiv

  2. [12]

    [VMA19] Andrea Vezzosi, Anders M¨ ortberg, and Andreas Abel

    Lean 4 mathematical library. [VMA19] Andrea Vezzosi, Anders M¨ ortberg, and Andreas Abel. Cubical Agda: A dependently typed programming language with univalence and higher inductive types. InProceedings of the ACM on Programming Languages (ICFP), volume 3, pages 87:1–87:29, 2019.doi:10.1145/3341691. [WL20] Matthew Z. Weaver and Daniel R. Licata. A constru...

    arXiv 2019

  3. [13]

    [ZM23] Max Zeuner and Anders M¨ ortberg

    URL:https://arxiv.org/abs/2606.03719. [ZM23] Max Zeuner and Anders M¨ ortberg. A univalent formalization of constructive affine schemes. In28th International Conference on Types for Proofs and Programs (TYPES 2022), volume 269 ofLeibniz International Proceedings in Informatics (LIPIcs), pages 14:1–14:24. Schloss Dagstuhl—Leibniz-Zentrum f¨ ur Informatik, ...

    Pith/arXiv arXiv 2022

  4. [2009]

    Lawvere-tierney sheafification in homotopy type theory

    [QT16] Kevin Quirin and Nicolas Tabareau. Lawvere-tierney sheafification in homotopy type theory. Journal of Formalized Reasoning, 9(2):131–161, 2016.doi:10.6092/issn.1972-5787/6232. [RS17] Emily Riehl and Michael Shulman. A type theory for synthetic ∞-categories.Higher Structures, 1(1):147–224,

    doi:10.6092/issn.1972-5787/6232 2016

  5. [2011]

    The cohomology of non-locality and contextuality

    [AMB12] Samson Abramsky, Shane Mansfield, and Rui Soares Barbosa. The cohomology of non-locality and contextuality. InProceedings 8th International Workshop on Quantum Physics and Logic (QPL 2011), volume 95 ofEPTCS, pages 1–14,

    2011

  6. [2012]

    A general algorithm for deciding transportability of experi- mental results.Journal of Causal Inference, 1(1):107–134, 2013.doi:10.1515/jci-2012-0004

    [BP13] Elias Bareinboim and Judea Pearl. A general algorithm for deciding transportability of experi- mental results.Journal of Causal Inference, 1(1):107–134, 2013.doi:10.1515/jci-2012-0004. [BP16] Elias Bareinboim and Judea Pearl. Causal inference and the data-fusion problem.Proceedings of the National Academy of Sciences, 113(27):7345–7352, 2016.doi:10...

    doi:10.1515/jci-2012-0004 2013

  7. [2017]

    Conference version: TYPES 2015, LIPIcs 69, 5:1–5:34,

    2015

  8. [2019]

    [dAFH09] Ricardo Queiroz de Araujo Fernandes and Edward Hermann Haeusler

    doi:10.1017/S0960129518000488. [dAFH09] Ricardo Queiroz de Araujo Fernandes and Edward Hermann Haeusler. A topos-theoretic approach to counterfactual logic.Electronic Notes in Theoretical Computer Science, 256:33–47,

    doi:10.1017/s0960129518000488

  9. [2020]

    doi:10.1016/j.aim.2020. 107239. [GP23] Stefano Gogioso and Nicola Pinzani. The topology of causality.arXiv preprint arXiv:2303.07148,

    Pith/arXiv arXiv 2020

  10. [2023]

    Directed univalence in simplicial homotopy type theory.arXiv preprint arXiv:2407.09146,

    [GWB24] Daniel Gratzer, Jonathan Weinberger, and Ulrik Buchholtz. Directed univalence in simplicial homotopy type theory.arXiv preprint arXiv:2407.09146,

    arXiv

  11. [2024]

    Causal inference by string diagram surgery

    [JKZ19] Bart Jacobs, Aleks Kissinger, and Fabio Zanasi. Causal inference by string diagram surgery. In Foundations of Software Science and Computation Structures (FoSSaCS 2019), volume 11425 of Lecture Notes in Computer Science. Springer, 2019.doi:10.1007/978-3-030-17127-8_18. [LBG24] Zhengyu Li, Curtis Bright, and Vijay Ganesh. A SAT solver and computer ...

    doi:10.1007/978-3-030-17127-8_18 2019

  12. [2025]

    [Mah25b] Sridhar Mahadevan

    Version 2, 25 July 2026; all references here are to that version. [Mah25b] Sridhar Mahadevan. Topos causal models, 2025.arXiv:2508.08295. [Mah25c] Sridhar Mahadevan. Universal causal inference in a topos. InAdvances in Neural Information Processing Systems 38 (NeurIPS 2025),

    Pith/arXiv arXiv 2026

  13. [2026]

    URL: https://arxiv.org/abs/2606

    Companion paper. URL: https://arxiv.org/abs/2606. 20351,arXiv:2606.20351. [The24] The mathlib Community. Mathlib.Algebra.Star.CHSH: Tsirelson’s inequality,

    Pith/arXiv arXiv

This paper was first reviewed by deepseek-v4-flash on August 4, 2026.