README

This is an implementation of category theory in Coq.

Coq version and compilation

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

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

Name		Name	Last commit message	Last commit date
Latest commit History 160 Commits
Adjunction		Adjunction
Algebras		Algebras
Archetypal		Archetypal
Basic_Cons		Basic_Cons
Cat		Cat
Category		Category
Coq_Cats		Coq_Cats
Demo		Demo
Essentials		Essentials
Ext_Cons		Ext_Cons
Functor		Functor
KanExt		KanExt
Limits		Limits
Monad		Monad
NatTrans		NatTrans
PreSheaf		PreSheaf
Topos		Topos
Yoneda		Yoneda
.gitignore		.gitignore
README.md		README.md
_CoqProject		_CoqProject
configure.sh		configure.sh