fact: Definition morphism_class_rm_opp {C : category} (S : morphism_class (op_cat C)) : (morphism_class C) := λ X Y f, (S _ _) (rm_opp_mor f).
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.ModelCategories.Retract