define abstract category, impredicatively

[t6s]

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.

[affeldt-aist]

Should the changes in imonae_lib.v be also reported in monae_lib.v?
(It is easier for maintenance to these two files as similar as possible.)

[t6s]

The only essential change in imonae_lib.v is the addition of funeqP, and it is not necessary for monae_lib.v since it is provided by boolp.v https://github.com/math-comp/analysis/blob/155492be64984449ebcdd79191ebdf5983fed60c/classical/boolp.v#L147

Do you suggest redefining it in monae_lib.v?

[affeldt-aist]

Do you suggest redefining it in monae_lib.v?

No, this wouldn't be a good idea in that case, but could left a comment, for I am sure that I will ask again in a few months ;-)

[t6s]

Porting Arguments lines to monae_lib.v seems to be harmless.

[affeldt-aist]

Maybe you want to double-check this PR while you rebase,
because Florent has been contributed a few changes to category.v (that have been merged in master),
they are perhaps worth backporting in icategory.v.

[t6s]

It think this PR should be anyway turned into a draft.
(or perhaps abandoned since the original goal to define functor categories has not been achieved even by impredicativity.)