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'
In https://github.com/hivert/Adjoint/blob/main/theories/category.v I adapted and expanded the
category.vto 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.{hom a -> b}instead of{hom a, b}[ ] transfert of an adjunction through a natural isomorphism
G ~ G' -> F -| G -> F -| G'Please comment.