Category Theory in Coq 8.5

Amin Timany and Bart Jacobs: Category Theory in Coq 8.5. In Coq Workshop 2015, June 2015.
arXiv [slides] .pdf
Unpublished Workshop Paper
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.

The bibtex source for this publication:
@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}
 }