Email Gateway (Mar 04 2024 at 15:13): Email Gateway (Mar 04 2024 at 15:13):From: Tobias Nipkow <nipkow@in.tum.de>
Cubical Categories
Georg Struth and Tanguy Massacrier
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.
https://www.isa-afp.org/entries/CubicalCategories.html
Enjoy!
Last updated: Jan 04 2025 at 20:18 UTC