### 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 (Version 2). arXiv. https://doi.org/10.48550/ARXIV.2401.10553

### Session CubicalCategories

- ICatoids
- CubicalCategories
- CubicalCategoriesConnections
- CubicalOmegaZeroCategoriesConnections

### Depends on

- Catoids, Categories, Groupoids

### Auto-related entries

- Higher Globular Catoids and Quantales
- Go Code Generation for Isabelle
- Zermelo Fraenkel Set Theory in Higher-Order Logic
- Quaternions
- Type Constructor Classes and Monad Transformers

## Cite

×

CubicalCategories-AFP

    @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