A formalization of category theory in the Coq proof assistant.
Coq
100
160 commits
updated Nov 4, 2024
README
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.shto produce the Makefile [1] and thenmaketo compile
[1] you will need to have coq_makefile to be on the path
adjunctions
categories
category-theory
coq
coq-formalization
kan-extensions
library
proof-assistant
topos
Contributors
amintimany
160 commits
Similar repos
Languages
Coq
100.0%
A formalization of category theory in the Coq proof assistant.
Coq
100
160 commits
updated Nov 4, 2024
README
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.shto produce the Makefile [1] and thenmaketo compile
[1] you will need to have coq_makefile to be on the path
adjunctions
categories
category-theory
coq
coq-formalization
kan-extensions
library
proof-assistant
topos
Similar repos
Contributors
amintimany
160 commits
Languages
Coq
100.0%