Cubical Categories

Georg Struth 📧 and Tanguy Massacrier

January 24, 2024


This AFP entry formalises cubical omega-categories and cubical omega-categories with connections in the style of single-set categories. Cubical categories, and the cubical sets on which they are based, have their origins and main applications in algebraic topology. Applications in computer science include homotopy type theory, higher-dimensional automata in concurrency theory and higher-dimensional rewriting. The single-set axiomatisation, introduced in these components and a companion paper, allows a formalisation based on Isabelle's type classes.


BSD License


Related publications

  • Malbos, P., Massacrier, T., & Struth, G. (2024). Single-set cubical categories and their formalisation with a proof assistant (Version 2). arXiv.

Session CubicalCategories