Abstract
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.
License
Topics
Related publications
- Malbos, P., Massacrier, T., & Struth, G. (2024). Single-set cubical categories and their formalisation with a proof assistant (extended version) (Version 3). arXiv. https://doi.org/10.48550/ARXIV.2401.10553