fact: Definition oppositePrecategoryWithBinOps (M : precategoryWithBinOps) : precategoryWithBinOps := make_precategoryWithBinOps (op_category M) (λ A B f g, @to_binop M (rm_opp_ob B) (rm_opp_ob A) (rm_opp_mor f) (rm_opp_mor g)).
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.Algebra.BinaryOperations UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.TransportMorphisms UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.opp_precat