fact: Definition weq_cancel_right {C : category} (W : weak_equivalences C) := is_weq_cancel_right (weq_is_weq W).
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.ModelCategories.MorphismClass