Pith. sign in

REVIEW 3 major objections 5 minor 6 references

A Graphical Interface for Category Theory Proofs in Coq

T0 review · 3 major / 5 minor · reviewed 2026-08-15 · deepseek-v4-flash

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

Pith's one-line read A Coq plugin turns category-theory proof goals into interactive commutative diagrams and lets users advance proofs by manipulating those diagrams.

desk verdict A coherent tool paper: the pushout-based lemma matching is genuinely new, but the soundness question is real and the paper would be stronger with one explicit statement of how Coq's kernel bounds the damage. read the letter →

arxiv 2505.13473 v1 pith:63TZHC7K submitted 2025-05-09 cs.LO cs.PL

Luc Chabassier (ENS Paris-Saclay) This is my paper · ORCID
classification cs.LOcs.PL
keywords categorytheoryproofassistantcommutativediagramsCoqplugingraphicalpushoutlemmaapplicationdiagrammaticreasoning
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

The paper is trying to establish that categorical proofs can be read, edited, and advanced through a graphical interface living inside a general-purpose proof assistant, rather than in a separate diagram tool with its own logic. The plugin builds a commutative diagram directly from a Coq proof state, normalizes it, and exposes operations such as splitting, merging, decomposing, and lemma application that change both the diagram and the proof. Lemma application works by representing the lemma as a graph pattern, letting the user match its nodes and edges to the goal diagram, and gluing the two graphs along that match; the glued diagram becomes the new proof state. If this works as described, students could practice diagrammatic reasoning on concrete proofs, and the same proof scripts could be replayed or ported across proof assistants.

What carries the argument

The central object is the graph extracted from a Coq proof state, together with the pattern graph extracted from a first-order lemma about categories. The operation that carries lemma application is the pushout of a partial matching: the interface unifies the Coq terms on matched objects as the user selects them, then takes the union of the lemma graph and the goal graph and merges the matched objects, producing the new proof state by gluing the two diagrams together.

What would settle it

Record the full Coq proof term the plugin produces for a nontrivial category-theory proof and check it with Coq's kernel; a single accepted proof whose generated term fails type-checking, or a lemma application that creates a goal not derivable from the matched hypotheses, would refute the claim.

Watch

Extended reading notes

Core claim

The paper claims that a Coq plugin can read a proof goal whose conclusion is an equality between morphisms, extract a graph whose nodes are objects, whose edges are morphisms, and whose faces are equalities, and then let the user manipulate that graph, splitting and merging edges, decomposing faces, and applying lemmas, where each manipulation refines the underlying Coq proof state. In particular, applying a lemma is done by matching its extracted graph pattern against the goal graph and computing the pushout of the two graphs modulo the matching; the result becomes the new goal graph, and any remaining proof obligations are returned to Coq as new goals.

Load-bearing premise

The load-bearing premise is that gluing the lemma's diagram to the goal's diagram, after unifying the matched terms, yields exactly the proof obligations of a correct Coq refinement.

Editorial extensions

If this is right

  • A user can complete a categorical proof, including instantiating existential variables, without leaving the diagram, because merging matched objects unifies the underlying Coq terms.
  • The textual script language makes every graphical interaction replayable: the same file re-runs the proof without reopening the interface when it succeeds.
  • The uniform lemma-application mechanism covers backward reasoning, forward reasoning, exact application, and cut, all through the same pushout operation.
  • Because the plugin talks to the interface through a small protocol, the same interface could be reused by other proof assistants with a modest porting effort.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the pushout operation is sound, the same mechanism could generalize from categories to any theory whose proof states admit a graph-like structure, turning lemma application into a generic diagrammatic rewriting step.
  • The plugin's soundness is ultimately a claim about the correspondence between graph unification and Coq's dependent type checker; a testable extension is to instrument every plugin step to emit the generated Coq refinement and verify it with the kernel.
  • For teaching, the web version suggests a further step: an exercise author could choose which lemmas are visible, turning the diagram editor into a puzzle environment where students build proofs by matching shapes.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

3 major / 5 minor

Summary. The paper presents a Coq plugin that renders a proof goal as a commutative diagram when the goal is an equality between morphisms in a category, using the UniMath library. The user can manipulate the diagram through operations such as splitting, merging, decomposing, composing, and normalizing edges, and can apply lemmas by matching a graph pattern extracted from the lemma statement, unifying terms via Coq, and then computing a pushout of the two graphs. The paper also describes a replayable textual script language for proof interactions and a split architecture in which a Rust interface communicates with a Coq plugin through a custom protocol, with a web version reported as in progress. The central claim is that interactive diagrammatic proof is feasible inside a generic proof assistant, with the graph operations producing valid Coq refinements.

Significance. If the implementation is correct, the tool is a useful educational artifact and a concrete step toward context-specific proof assistants layered over generic ones. The paper gives a worked example, explains the graph model and the main operations, and honestly discusses several limitations, including the restriction to a first-order fragment and the inability to apply lemmas under a term. The strengths are the concrete demonstration, the public repository, and the replayable script language. However, the paper does not supply a soundness theorem, a test suite, or a user study, so the significance is currently that of a feasibility demonstration rather than a verified or empirically evaluated system.

major comments (3)
  1. [§4.3] The central correctness claim of the paper is that the pushout-based lemma application produces a valid new proof state, but no soundness argument is given. The text states that 'the pushout of the matching is computed and the result is the new proof state,' yet it does not state a correspondence theorem between graph nodes, edges, and faces and Coq terms, nor does it prove that the pushout is logically equivalent to Coq's apply or refine. Since Section 4.4 explicitly restricts the supported fragment and admits that lemmas cannot be applied under a term, the graph representation is not a complete account of the Coq context, so soundness is not self-evident. A silent divergence from Coq's unification or refinement semantics in a corner case (for example, with existential quantifiers or partial matches) would make the tool unsound in a way that defeats its purpose. Please provide a precise statement of the correspondence, or at least a substantial automated test suite covering partial matches, existential lemmas, and nested terms; without this, the main claim that the user can progress proofs safely remains unverified.
  2. [§3] The proof-progressing operations described in Section 3, especially 'Merging' and 'Solving,' are specified only informally. For example, the solver 'attempts to construct an equality proof from the other equalities present, using the structure of the graph,' but the paper does not say what Coq term or tactic is generated when the solver succeeds. The same applies to 'Decomposition,' which 'refines the equality to reduce it to proof obligations for all the atomic planar regions.' Because these operations change the Coq proof state, the reader cannot judge whether they are guaranteed to produce well-typed refinements. Please specify the underlying proof-term construction or tactic for each operation that modifies the Coq state, or state which of them are intended only as heuristics whose outputs are checked by Coq before being accepted.
  3. [§5.1] The scope of the tool is narrower than the title and abstract suggest. The architecture description in Section 5.1, step ➋, says the plugin constructs the graph 'if it is an equality between morphisms,' and the concrete example in Section 2.1 is an equality goal. The abstract, however, announces 'a graphical interface for category theory proofs' without this qualification. This discrepancy should be corrected, either by narrowing the stated contribution to equality goals in the first-order fragment or by clearly stating the supported class of goals in the abstract and introduction; otherwise the central claim is broader than what is demonstrated.
minor comments (5)
  1. [§1] There is a typo in the last paragraph of the introduction: 'We well begin' should be 'We will begin.'
  2. [§2.2] The scripting language example in Figure 4 contains the command 'succeed,' but the paper never explains its meaning or when it is generated. A brief description of each command in the script language would help readers understand the replay mechanism.
  3. [§4.2] The treatment of existential quantifiers in lemmas would benefit from a precise Coq term. The paper says 'an existential quantifier is a dependent pair' and that references can be substituted by 'the first projection of the lemma,' but the standard Coq ex type lives in Prop and does not have a first projection in the same sense as sigT. Please specify the exact Coq representation used (for example, sigT or a UniMath-specific dependent sum) so that this step can be checked.
  4. [§5.2] The web version is described as motivating a substantial asynchronous rewrite, but the paper states that it cannot yet provide a link and that the asynchronous version is still in progress. Marking this section more explicitly as future work would make the status of the web version clearer.
  5. [Appendix A] The appendix lists the original screenshots but does not explicitly state which screenshots correspond to Figures 2 and 3. Adding a short mapping would make the appendix more useful to readers who want to compare the synthetic figures with the actual interface.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity: the paper is a tool implementation report with no fitted parameters, no predictions derived from fitted inputs, and no load-bearing self-citation chain.

full rationale

The paper reports a Coq plugin that extracts a commutative-diagram graph from a proof state, lets the user manipulate it, and reconstructs Coq refinements from those manipulations. Its central claims are existence and design claims about the tool, not derived quantities or empirical predictions. There are no fitted constants, no data subsets used to predict closely related quantities, and no uniqueness theorem imported from the authors' prior work. The only citations are to other tools and background references (Actema, Lean widgets, Lafont's diagram editor, string diagrams, topos theory unification), and none of these is invoked as a load-bearing justification for a derived result. The skeptical concern that the pushout-based lemma application in Section 4.3 is not accompanied by a formal soundness proof against Coq's refine is a correctness-risk concern about unverified behavior, not a circularity: the paper does not define its pushout operation in terms of the proof states it is supposed to produce, nor does it fit the operation to a dataset and then call the fit a prediction. The design is self-contained as an implementation description, so the appropriate circularity score is 0.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

For a tool paper, the ledger is mostly empty of fitted parameters and invented entities. The central claim depends on domain assumptions about the correctness of the graph extraction and pushout operations, and on the UniMath library's faithfulness. The tool introduces no new mathematical objects.

assumptions (3)
  • domain assumption The UniMath library correctly implements precategory axioms, including identity and composition, as used to build graphs from Coq goals.
    Section 2.1 states the plugin works only with the UniMath library; the graph extraction assumes these categorical structures are faithful.
  • domain assumption Graph extraction and pushout computation preserve the logical content of the Coq proof state.
    Sections 3 and 4.3 claim merging and pushout operations 'progress the Coq proof' and 'result in the new proof state,' but no soundness proof is given.
  • ad hoc to paper The restriction of supported lemmas to first-order formulas over categorical types is sufficient for the intended teaching use cases.
    Section 4.1 chooses this restriction to limit engineering work, and the paper acknowledges natural transformations and other structures are not yet supported.

how reviews work

0 comments
Cite this review

Pith. "Pith review of A Graphical Interface for Category Theory Proofs in Coq." pith.science (2026). https://pith.science/paper/63TZHC7K

@misc{pith2026250513473,
  author       = {Pith},
  title        = {Pith review of: A Graphical Interface for Category Theory Proofs in Coq},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/63TZHC7K}},
  note         = {Machine review of arXiv:2505.13473}
}
read the original abstract

The importance of category theory in recent developments in both mathematics and in computer science cannot be overstated. However, its abstract nature makes it difficult to understand at first. Graphical languages have been developed to help manage this abstraction, but they have not been used in proof assistants, most of which are text-based. We believe that a graphical interface for categorical proofs integrated in a generic proof assistant would allow students to familiarize themselves with diagrammatic reasoning on concrete proofs that they are already familiar with. We present an implementation of a Coq plugin that enables both visualization and interactions with Coq proofs in a graphical manner.

Figures

Figures reproduced from arXiv: 2505.13473 by the authors.

Figure 1
Figure 1. A Coq goal happened in parallel to ours, and most engineering decisions are different, but we believe at some point our two tools should converge into one. Integrating graphical reasoning in proof assistants is not a novel idea, and previous experiments include Actema [5] and Lean widgets [1]. Lean widgets actually include a specific widget to visualize the current proof state as a commutative diagram, but is limite… view at source ↗
Figure 2
Figure 2. The plugin interface This Coq script rewrites all associativities to one side, and then removes the compositions with identities on the left and on the right. However, we do not need to do this because our plugin has its own normalization procedure which is applied at the start. More precisely, when started, the plugin looks into the proof goal to identify the objects and morphisms, and construct a graph from it. So… view at source ↗
Figure 3
Figure 3. The lemma application window The interface exposes some operations to transform the graph and progress the proof, such as splitting an edge along compositions, splitting an equality along its planar decomposition, an automatic procedure for faces. . . These operations will be detailed in section Section 3. One can progress quite a lot using only these, but to conclude this proof using Hf is necessary to deal with f.… view at source ↗
Figures from the paper (5 more)
Figure 4
Figure 4. Figure 4: An example of the plugin scripting language [PITH_FULL_IMAGE:figures/full_fig_p005_4.png]
Figure 5
Figure 5. Figure 5: A prematch given by the user, with the deduced unifier of the matched terms on the right. [PITH_FULL_IMAGE:figures/full_fig_p009_5.png]
Figure 6
Figure 6. Figure 6: Result of the application [PITH_FULL_IMAGE:figures/full_fig_p009_6.png]
Figure 7
Figure 7. Figure 7: The architecture of the plugin with the interface [PITH_FULL_IMAGE:figures/full_fig_p011_7.png]
Figure 8
Figure 8. Figure 8: Architecture of the web version. We believed that all that was needed was to change the connection method of the interface to use web sockets. However, we used a synchronous communication channel, and in the browser it is only possible to use asynchronous communication…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

6 extracted references · 5 canonical work pages

  1. [1]

    doi:10.17863/CAM.81869

    Edward Ayers (2021): A Tool for Producing Verified, Explainable Proofs. doi:10.17863/CAM.81869. Avail- able at https://www.repository.cam.ac.uk/handle/1810/334452. Publisher: Apollo - University of Cambridge Repository

    work page doi:10.17863/cam.81869 2021

  2. [2]

    Baez & Mike Stay (2010): Physics, Topology, Logic and Computation: A Rosetta Stone

    John C. Baez & Mike Stay (2010): Physics, Topology, Logic and Computation: A Rosetta Stone . arXiv:0903.0340 [quant-ph] 813, pp. 95–172, doi:10.1007/978-3-642-12821-9_2. Available at http:// arxiv.org/abs/0903.0340. ArXiv: 0903.0340

    arXiv 2010

  3. [3]

    In: Leibniz International Proceedings in Informatics , 52, pp

    Krzysztof Bar, Aleks Kissinger & Jamie Vicary (2016): Globular: an online proof assistant for higher-dimensional rewriting. In: Leibniz International Proceedings in Informatics , 52, pp. 34:1–34:11, doi:10.23638/LMCS-14(1:8)2018

    work page doi:10.23638/lmcs-14(1:8)2018 2016

  4. [4]

    The unification of Mathematics via Topos Theory

    Olivia Caramello (2010): The unification of Mathematics via Topos Theory , doi:10.48550/arXiv.1006.3930. Available at http://arxiv.org/abs/1006.3930. ArXiv:1006.3930 [math]

    work page Pith review arXiv doi:10.48550/arxiv.1006.3930 2010

  5. [5]

    In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs , ACM, Philadelphia PA USA, pp

    Pablo Donato, Pierre-Yves Strub & Benjamin Werner (2022): A drag-and-drop proof tactic. In: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs , ACM, Philadelphia PA USA, pp. 197–209, doi:10.1145/3497775.3503692. Available at https://dl.acm.org/doi/10.1145/ 3497775.3503692

    work page arXiv 2022

  6. [6]

    Available at https://hal

    Ambroise Lafont (2024): A diagram editor to mechanise categorical proofs . Available at https://hal. science/hal-04407118. L. Chabassier 41 A Screenshots Since the graphical framework we used only has a black theme, and we did not take the time to create another lighter theme, we replaced the screenshots in the main body of the paper by figures made in- d...

    work page 2024

Pith tools

Reviewed August 15, 2026 · model on record in the stance chip above.