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

TL;DR

idris-ct is a practical Idris library that formalizes categorical concepts using dependent types, enabling verified and correct implementations for both theoretical exploration and industrial software development.

Contribution

It introduces a verified Idris library for category theory that bridges academic concepts with practical software engineering applications.

Findings

Provides formally verified categorical definitions in Idris

Enables implementation of category theory concepts in real-world software

Bridges the gap between theoretical category theory and practical programming

Abstract

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.