Библиотека категорий для Agda?
Существуют ли "рекомендуемые" библиотеки, которые обеспечивают удобную формализацию базовой теории категорий в Agda? Стандартная библиотека Agda, кажется, предоставляет очень мало в этом отношении.
Я ищу что-то с низким барьером для входа, подобно тому, как кто-то использует алгебраические структуры, такие как Semigroup определено в стандартной библиотеке.
Например, в моем текущем проекте есть несколько понятий морфизма, и перегрузка синтаксиса для композиции и идентичности становится неудобной. Естественно было бы ввести подходящий тип записи и использовать механизм "аргументов экземпляра" Агды для эмуляции Morphism тип класс. Но, без сомнения, это должно быть колесо, которое было изобретено много раз. (Хорошо, есть структура под названием Morphism в стандартной библиотеке, которая, возможно, может быть адаптирована для этой цели, так что это не обязательно лучший пример, но вы поняли.)
Мне известна эта библиотека, которая выглядит всеобъемлющей, но, кажется, не особенно активна.
2 ответа
Это старый вопрос, но он по-прежнему получает ответы в Google и других поисковых запросах, поэтому: библиотека де-факто теперь называется agda-categories.
Я использую библиотеку категорий, как упомянуто выше, и, хотя я использую только ее базовые функции, пока что все в порядке.