Category Theory in Coq 8.5
classification
💻 cs.LO
keywords
categorytheoryamintimanybitbucketcategoriesdevelopmentexperiencefeatures
read the original abstract
We report on our experience implementing category theory in Coq 8.5. The repository of this development can be found at https://bitbucket.org/amintimany/categories/. This implementation most notably makes use of features, primitive projections for records and universe polymorphism that are new to Coq 8.5.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.