This PR adds a definition of abstract categories extending category.v.
Due to shortcomings in the constraint solver for universes in Coq,
this could only be done only for the impredicative version of monae.
Some compatibility changes are needed and made in imonae_lib to make it resemble more to analysis.boolp.
This PR adds a definition of abstract categories extending category.v. Due to shortcomings in the constraint solver for universes in Coq, this could only be done only for the impredicative version of monae.
Some compatibility changes are needed and made in imonae_lib to make it resemble more to analysis.boolp.