2026-07-21T11:10:39Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:6000 2024-03-06T10:37:27Z ddc:004 open_access

Category Theory in Coq 8.5 Timany, Amin Jacobs, Bart Category Theory Coq 8.5 Universe Polymorphism Homotopy Type Theory We report on our experience implementing category theory in Coq 8.5. Our work formalizes most of basic category theory, including concepts not covered by existing formalizations, in a library that is fit to be used as a general-purpose category-theoretical foundation. Our development particularly takes advantage of two features new to Coq 8.5: primitive projections for records and universe polymorphism. Primitive projections allow for well-behaved dualities while universe polymorphism provides a relative notion of largeness and smallness. The latter is one of the main contributions of this paper. It pushes the limits of the new universe polymorphism and constraint inference algorithm of Coq 8.5. In this paper we present in detail smallness and largeness in categories and the foundation they are built on top of. We furthermore explain how we have used the universe polymorphism of Coq 8.5 to represent smallness and largeness arguments by simply ignoring them and entrusting them to the universe inference algorithm of Coq 8.5. We also briefly discuss our experience throughout this implementation, discuss concepts formalized in this development and give a comparison with a few other developments of similar extent. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Amin Timany and Bart Jacobs 2016 Is Part Of LIPIcs, Volume 52, 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2016.30 urn:nbn:de:0030-drops-60003 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2016.30 eng https://creativecommons.org/licenses/by/3.0/legalcode