Category Theory in Coq 8.5

In Coq Workshop 2015 Unpublished Workshop Presentation
Amin Timany and Bart Jacobs. Category Theory in Coq 8.5. In Coq Workshop 2015, June 2015.
  • Links: arXiv [slides] .pdf
  • Keywords: Category Theory, Coq 8.5, Universe Polymorphism, Homotopy Type Theory
Abstract

We report on our experience implementing category theory in Coq 8.5. The repository of this development can be found at this https URL. This implementation most notably makes use of features, primitive projections for records and universe polymorphism that are new to Coq 8.5.

BibTeX
@inproceedings{KULeuven-515021,
 author = {Timany, Amin and Jacobs, Bart},
 title = {Category Theory in Coq 8.5},
 booktitle = {Coq Workshop},
 year = {2015},
 month = {June}, 
 url = {https://arxiv.org/abs/1505.06430}
 }