Utilities and reasoning principles for monads in Coq
The development is organized as the follows.
Basics/— files relevant to category theory, heterogenous relations, and other basic definitionsStructure/— definitions of monadsEqmR/— definition of eqmREqmRInstances/— instances of eqmRAlgebras/— algebraic properties of eqmR
The following are necessary dependencies for the code base.
- rocq 9.0
The project can be built by running make in the top directory.
make