package rocq-categories
A library for category theory
Install
Dune Dependency
Authors
Maintainers
Sources
v1.0.tar.gz
sha512=21508cdafe3860e2ed5869c276f5bb326ffd9691d9e0f027f5c74fa1cefbbc37f8d951fd2df76af2fd62bbf004c8de2ee39ee03884647c3ee3a73971e43721a0
Description
Library about category theory, with hom-setoids. Hierarchy of structures implemented with Hierarchy Builder. Inference of MacLane morphisms and decision procedure for monoidal categories.
Tags
keyword:category theory keyword:monoidal categories keyword:MacLane's coherence theorem keyword:string diagrams keyword:setoid logpath:Categories date:2026-05-07Published: 18 May 2026
Dependencies (3)
- rocq-partial-orders
- rocq-stdlib
-
rocq-core
>= "9.1"
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page