License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2016.30
URN: urn:nbn:de:0030-drops-60003
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2016/6000/
Go to the corresponding LIPIcs Volume Portal

Timany, Amin ; Jacobs, Bart

Category Theory in Coq 8.5

pdf-format:
LIPIcs-FSCD-2016-30.pdf (0.5 MB)

Abstract

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.

BibTeX - Entry

@InProceedings{timany_et_al:LIPIcs:2016:6000,
  author =	{Amin Timany and Bart Jacobs},
  title =	{{Category Theory in Coq 8.5}},
  booktitle =	{1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)},
  pages =	{30:1--30:18},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-010-1},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{52},
  editor =	{Delia Kesner and Brigitte Pientka},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2016/6000},
  URN =		{urn:nbn:de:0030-drops-60003},
  doi =		{10.4230/LIPIcs.FSCD.2016.30},
  annote =	{Keywords: Category Theory, Coq 8.5, Universe Polymorphism, Homotopy Type Theory}
}

Keywords: Category Theory, Coq 8.5, Universe Polymorphism, Homotopy Type Theory
Collection: 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016)
Issue Date: 2016
Date of publication: 17.06.2016

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI