TL;DR
This paper discusses implementing category theory in Coq 8.5, highlighting the use of new features like primitive projections and universe polymorphism to enhance formalization.
Contribution
It introduces a formalization of category theory in Coq 8.5 utilizing new language features for improved expressiveness.
Findings
Successful implementation of category theory in Coq 8.5
Utilization of primitive projections and universe polymorphism
Repository available at provided URL
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
