Cubical Categories

Georg Struth 📧 and Tanguy Massacrier

January 24, 2024

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

Related publications

  • Malbos, P., Massacrier, T., & Struth, G. (2024). Single-set cubical categories and their formalisation with a proof assistant (Version 2). arXiv. https://doi.org/10.48550/ARXIV.2401.10553

Session CubicalCategories

Depends on

Auto-related entries

Cite

× 
@article{CubicalCategories-AFP,
  author  = {Georg Struth and Tanguy Massacrier},
  title   = {Cubical Categories},
  journal = {Archive of Formal Proofs},
  month   = {January},
  year    = {2024},
  note    = {\url{https://isa-afp.org/entries/CubicalCategories.html},
             Formal proof development},
  ISSN    = {2150-914x},
}
Download

Download

× Download latest