A formalization of category theory in the Coq proof assistant.
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
Adjunction Correct _CoqProject Sep 27, 2017
Algebras
Archetypal
Basic_Cons
Cat
Category
Coq_Cats Correct _CoqProject Sep 27, 2017
Demo
Essentials
Ext_Cons
Functor
KanExt
Limits
NatTrans
PreSheaf
Topos Correct _CoqProject Sep 27, 2017
Yoneda Correct _CoqProject Sep 27, 2017
.gitignore Make the development compatible with Coq8.7beta1 Sep 27, 2017
README.md
_CoqProject Correct _CoqProject Sep 27, 2017
configure.sh

README.md

README

This is an implementation of category theory in Coq.

Coq version and compilation

  • This development uses features new to Coq8.6
  • It has been tested on Debian with Coq 8.6
  • To compile simply type
    • ./configure to produce the Makefile [1] and then
    • make to compile

[1] you will need to have coq_makefile to be on the path