fact: Definition morphism_class_isos (C : category) : (morphism_class C) := λ X Y f, make_hProp (is_iso f) (isaprop_is_iso _ _ _).
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.ModelCategories.Retract