Cubical Categories

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.

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

BSD License

Topics

Mathematics/Category theory

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

Session CubicalCategories

Depends on

Catoids, Categories, Groupoids