A diagram editor to mechanize categorical proofs
summary
A diagram editor runs as a web app or Electron desktop app and hooks into Coq via VS Code + coq-lsp integration, showing diagrammatic goals as graphics and letting users create labeled proof nodes that become Coq tactics. It generates Coq proof scripts by asserting subdiagram commutations and inserting tactic steps or admits, uses a small custom notation/tactic layer, and currently targets the UniMath library for 1‑category proofs only, with validation performed by Coq and feedback shown in VS Code.
AI-written summary · about
chapters (12)
- 0:00Diagram editor intro
- 2:14Quiver comparison & features
- 3:17Mechanization architecture
- 5:48Automating categorical proofs
- 8:16Demo: distributive law
- 13:21Validating proofs with Coq
- 15:33Interactive proof workflow
- 17:32Generating proof scripts
- 19:21Closing remarks
- 19:43Q&A: proof complexity
- 20:25Q&A: VS Code integration
- 21:10Q&A: library compatibility
related talks
26mIntegrating graphical proofs in Coq
21mPractical compositional diagramming
01h 10mMedium-scale automation for proof assistants
04mLT Erich Studer
07mWeaving Schematics and Code: Interactive Visual Editing for Hardware Description Languages
21mLive Verification in an Interactive Proof Assistant
34mDiagram as Code - Decoding Architectural Diagrams
24mCode Generation via Meta-programming in Dependently Typed Proof Assistants