proposition: Lemma morphism_class_opp_opp {C : category} (S : morphism_class C) : morphism_class_opp (morphism_class_opp S) = S.
proof: Proof. trivial. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.ModelCategories.Retract