Single-set cubical categories and their formalisation with a proof assistant (extended version)
Fuente:
arXiv
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866909242090323968 |
|---|---|
| author | Malbos, Philippe Massacrier, Tanguy Struth, Georg |
| author_facet | Malbos, Philippe Massacrier, Tanguy Struth, Georg |
| contents | We introduce a single-set axiomatisation of cubical $ω$-categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the category of single-set cubical $ω$-categories, and their variants with connections and inverses, and the corresponding cubical $ω$-categories. We also report on the formalisation of cubical $ω$-categories with the Isabelle/HOL proof assistant, which has been instrumental in developing the single-set axiomatisation. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2401_10553 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Single-set cubical categories and their formalisation with a proof assistant (extended version) Malbos, Philippe Massacrier, Tanguy Struth, Georg Logic in Computer Science Category Theory 18N30, 68V15, 03B35, 68Q42 We introduce a single-set axiomatisation of cubical $ω$-categories, including connections and inverses. We justify these axioms by establishing a series of equivalences between the category of single-set cubical $ω$-categories, and their variants with connections and inverses, and the corresponding cubical $ω$-categories. We also report on the formalisation of cubical $ω$-categories with the Isabelle/HOL proof assistant, which has been instrumental in developing the single-set axiomatisation. |
| title | Single-set cubical categories and their formalisation with a proof assistant (extended version) |
| topic | Logic in Computer Science Category Theory 18N30, 68V15, 03B35, 68Q42 |
| url | https://arxiv.org/abs/2401.10553 |