idris-ct: A Library to do Category Theory in Idris

Fabrizio Genovese
(Statebox Team)
Alex Gryzlov
(Statebox Team)
Jelle Herold
(Statebox Team)
Andre Knispel
(Statebox Team)
Marco Perone
(Statebox Team)
Erik Post
(Statebox Team)
André Videla
(Statebox Team)

We introduce idris-ct, a Idris library providing verified type definitions of categorical concepts.idris-ct strives to be a bridge between academy and industry, catering both to category theorists who want to implement and try their ideas in a practical environment and to businesses and engineers who care about formalization with category theory: It is inspired by similar libraries developed for theorem proving but remains very practical, being aimed at software production in business. Nevertheless, the use of dependent types allows for a formally correct implementation of categorical concepts, so that guarantees can be made on software properties.

In John Baez and Bob Coecke: Proceedings Applied Category Theory 2019 (ACT 2019), University of Oxford, UK, 15-19 July 2019, Electronic Proceedings in Theoretical Computer Science 323, pp. 246–254.
Published: 15th September 2020.

ArXived at: https://dx.doi.org/10.4204/EPTCS.323.16 bibtex PDF

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org