Back port developpment from https://github.com/hivert/Adjoint/

[hivert]

In https://github.com/hivert/Adjoint/blob/main/theories/category.v I adapted and expanded the category.v to work in an axiom free setting with the goal of dealing with MathComp algebraic categories. There are a few things you might want to be backported. Here is a tentative list.

• fixes the notation for hom sets {hom a -> b} instead of {hom a, b}
• isomorphism theory for invertible morphisms (maybe it is not so useful with extensionality axioms).
• category equivalence (I ended up not using it but composition of adjunction since I actually needed adjoint equivalence).
• transfert of an adjunction through a natural isomorphism G ~ G' -> F -| G -> F -| G'

Please comment.