Document Open Access Logo

Automating Boundary Filling in Cubical Agda

Authors Maximilian Doré , Evan Cavallo , Anders Mörtberg

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2024.22.pdf
  • Filesize: 0.85 MB
  • 18 pages

Document Identifiers

Author Details

Maximilian Doré
  • Department of Computer Science, University of Oxford, United Kingdom
Evan Cavallo
  • Department of Computer Science and Engineering, University of Gothenburg, Sweden
Anders Mörtberg
  • Department of Mathematics, Stockholm University, Sweden

Funding

  • Doré, Maximilian: The author was supported by COST Action EuroProofNet, supported by COST (European Cooperation in Science and Technology, www.cost.eu).
  • Cavallo, Evan: The author was supported by the Knut and Alice Wallenberg Foundation through the Foundation’s program for mathematics.
  • Mörtberg, Anders: The author was supported by the Swedish Research Council (Vetenskapsrådet) under Grant No. 2019-04545.

Acknowledgements

We are grateful to Axel Ljungström for discussions about the solver and to him and Tom Jack for cubical versions of Eckmann-Hilton and syllepsis for us to test it with.

Cite AsGet BibTex

Maximilian Doré, Evan Cavallo, and Anders Mörtberg. Automating Boundary Filling in Cubical Agda. In 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 299, pp. 22:1-22:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/LIPIcs.FSCD.2024.22

Abstract

When working in a proof assistant, automation is key to discharging routine proof goals such as equations between algebraic expressions. Homotopy Type Theory allows the user to reason about higher structures, such as topological spaces, using higher inductive types (HITs) and univalence. Cubical Agda is an extension of Agda with computational support for HITs and univalence. A difficulty when working in Cubical Agda is dealing with the complex combinatorics of higher structures, an infinite-dimensional generalisation of equational reasoning. To solve these higher-dimensional equations consists in constructing cubes with specified boundaries. We develop a simplified cubical language in which we isolate and study two automation problems: contortion solving, where we attempt to "contort" a cube to fit a given boundary, and the more general Kan solving, where we search for solutions that involve pasting multiple cubes together. Both problems are difficult in the general case - Kan solving is even undecidable - so we focus on heuristics that perform well on practical examples. We provide a solver for the contortion problem using a reformulation of contortions in terms of poset maps, while we solve Kan problems using constraint satisfaction programming. We have implemented our algorithms in an experimental Haskell solver that can be used to automatically solve goals presented by Cubical Agda. We illustrate this with a case study establishing the Eckmann-Hilton theorem using our solver, as well as various benchmarks - providing the ground for further study of proof automation in cubical type theories.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Theory of computation → Type theory
  • Computing methodologies → Theorem proving algorithms
  • Theory of computation → Constraint and logic programming
  • Theory of computation → Automated reasoning
Keywords
  • Cubical Agda
  • Automated Reasoning
  • Constraint Satisfaction Programming

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Carlo Angiuli, Guillaume Brunerie, Thierry Coquand, Robert Harper, Kuen-Bang Hou (Favonia), and Daniel R. Licata. Syntax and models of Cartesian cubical type theory. Mathematical Structures in Computer Science, 31(4):424-468, 2021. URL: https://doi.org/10.1017/S0960129521000347.
  2. Carlo Angiuli, Kuen-Bang Hou (Favonia), and Robert Harper. Cartesian cubical computational type theory: Constructive reasoning with paths and equalities. In 27th EACSL Annual Conference on Computer Science Logic, CSL 2018, September 4-7, 2018, Birmingham, UK, pages 6:1-6:17, 2018. URL: https://doi.org/10.4230/LIPIcs.CSL.2018.6.
  3. Dimitri Ara, Albert Burroni, Yves Guiraud, Philippe Malbos, François Métayer, and Samuel Mimram. Polygraphs: From rewriting to higher categories. Submitted, 2023. URL: https://arxiv.org/abs/2312.00429.
  4. Steve Awodey. Cartesian cubical model categories, 2023. URL: https://arxiv.org/abs/2305.00893.
  5. Ronald Brown and Philip J. Higgins. On the algebra of cubes. Journal of Pure and Applied Algebra, 21(3):233-260, 1981. URL: https://doi.org/10.1016/0022-4049(81)90018-9.
  6. Guillaume Brunerie. On the homotopy groups of spheres in homotopy type theory. PhD thesis, Université de Nice Sophia Antipolis, 2016. Google Scholar
  7. Guillaume Brunerie. Computer-generated proofs for the monoidal structure of the smash product. Homotopy Type Theory Electronic Seminar Talks, November 2018. URL: https://www.uwo.ca/math/faculty/kapulkin/seminars/hottest.html.
  8. J. Daniel Christensen and Luis Scoccola. The Hurewicz theorem in Homotopy Type Theory. Algebraic & Geometric Topology, 23:2107-2140, 2023. Google Scholar
  9. Cyril Cohen, Thierry Coquand, Simon Huber, and Anders Mörtberg. Cubical Type Theory: A Constructive Interpretation of the Univalence Axiom. In Tarmo Uustalu, editor, 21st International Conference on Types for Proofs and Programs (TYPES 2015), volume 69 of LIPIcs, pages 5:1-5:34. Schloss Dagstuhl, 2018. URL: https://doi.org/10.4230/LIPIcs.TYPES.2015.5.
  10. Thierry Coquand, Simon Huber, and Anders Mörtberg. On Higher Inductive Types in Cubical Type Theory. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 255-264. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209197.
  11. Christoph Dorn. Associative n-categories. PhD thesis, University of Oxford, 2018. Google Scholar
  12. Beno Eckmann and Peter J. Hilton. Group-like structures in general categories I: multiplications and comultiplications. Mathematische Annalen, 145:227-255, 1962. Google Scholar
  13. Eric Finster and Samuel Mimram. A type-theoretical definition of weak ω-categories. In 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12, 2017. URL: https://doi.org/10.1109/LICS.2017.8005124.
  14. Eric Finster, David Reutter, Jamie Vicary, and Alex Rice. A type theory for strictly unital ∞-categories. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12, 2022. URL: https://doi.org/10.1145/3531130.3533363.
  15. Lennart Van Hirtum, Patrick De Causmaecker, Jens Goemaere, Tobias Kenter, Heinrich Riebler, Michael Lass, and Christian Plessl. A computation of D(9) using FPGA Supercomputing, 2023. URL: https://arxiv.org/abs/2304.03039.
  16. Kuen-Bang Hou (Favonia), Eric Finster, Daniel R. Licata, and Peter LeFanu Lumsdaine. A Mechanization of the Blakers-Massey Connectivity Theorem in Homotopy Type Theory. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '16, pages 565-574. Association for Computing Machinery, 2016. URL: https://doi.org/10.1145/2933575.2934545.
  17. Kuen-Bang Hou (Favonia) and Michael Shulman. The Seifert-van Kampen Theorem in Homotopy Type Theory. In Jean-Marc Talbot and Laurent Regnier, editors, 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22:1-22:16, Dagstuhl, Germany, 2016. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.22.
  18. Peter Tennant Johnstone. Stone Spaces, volume 3 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, 1986. Google Scholar
  19. Christian Jäkel. A computation of the ninth Dedekind Number, 2023. URL: https://arxiv.org/abs/2304.00895.
  20. Daniel M. Kan. Abstract homotopy. I. Proceedings of the National Academy of Sciences of the United States of America, 41(12):1092-1096, 1955. Google Scholar
  21. Jean-Louis Laurière. A language and a program for stating and solving combinatorial problems. Artificial Intelligence, 10(1):29-127, 1978. URL: https://doi.org/10.1016/0004-3702(78)90029-2.
  22. Per Martin-Löf. An intuitionistic theory of types: Predicative part. In H.E. Rose and J.C. Shepherdson, editors, Logic Colloquium '73, volume 80 of Studies in Logic and the Foundations of Mathematics, pages 73-118. Elsevier, 1975. URL: https://doi.org/10.1016/S0049-237X(08)71945-1.
  23. Anders Mörtberg and Loïc Pujet. Cubical Synthetic Homotopy Theory. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2020, pages 158-171, New York, NY, USA, 2020. Association for Computing Machinery. URL: https://doi.org/10.1145/3372885.3373825.
  24. Ian Orton and Andrew M. Pitts. Axioms for Modelling Cubical Type Theory in a Topos. Logical Methods in Computer Science, Volume 14, Issue 4, December 2018. URL: https://doi.org/10.23638/LMCS-14(4:23)2018.
  25. David Overton. Constraint Programming in Haskell. Melbourne Haskell Users Group, 2015. URL: https://de.slideshare.net/davidoverton/constraint-programming-in-haskell.
  26. Emily Riehl and Michael Shulman. A type theory for synthetic ∞-categories. Higher Structures, 1(1):116-193, 2017. Google Scholar
  27. Matthew Z. Weaver Robert Rose and Dan R. Licata. Deciding entailment for cofibration languages. At the second international conference on Homotopy Type Theory, 2023. URL: https://hott.github.io/HoTT-2023/slides/rose.pdf.
  28. Kristina Sojakova and G. A. Kavvos. Syllepsis in Homotopy Type Theory. In Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Association for Computing Machinery, 2022. URL: https://doi.org/10.1145/3531130.3533347.
  29. Cédric Ho Thanh, Pierre-Louis Curien, and Samuel Mimram. A sequent calculus for opetopes. In Proceedings of the 34th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 1-12, 2019. URL: https://doi.org/10.1109/LICS.2019.8785667.
  30. The 1Lab Development Team. The 1Lab, 2023. URL: https://1lab.dev.
  31. The Agda Community. Cubical Agda Library, October 2023. URL: https://github.com/agda/cubical.
  32. The RedPRL Development Team. The redtt proof assistant, 2018. URL: https://github.com/RedPRL/redtt/.
  33. The RedPRL Development Team. The cooltt proof assistant, 2021. URL: https://github.com/RedPRL/cooltt/.
  34. Edward Tsang. Foundations of Constraint Satisfaction. Academic Press, 1993. URL: https://doi.org/10.1016/C2013-0-07627-X.
  35. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. Google Scholar
  36. Floris van Doorn. On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory. PhD thesis, Carnegie Mellon University, May 2018. URL: https://arxiv.org/abs/1808.10690.
  37. Andrea Vezzosi, Anders Mörtberg, and Andreas Abel. Cubical Agda: a Dependently Typed Programming Language With Univalence and Higher Inductive Types. Proceedings of the ACM on Programming Languages, 3(ICFP):1-29, 2019. URL: https://doi.org/10.1145/3341691.
  38. Vladimir Voevodsky. The equivalence axiom and univalent models of type theory, February 2010. Notes from a talk at Carnegie Mellon University, available at URL: http://www.math.ias.edu/vladimir/files/CMU_talk.pdf.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact