proposition: Lemma rlp_isos : rlp (morphism_class_isos C) = morphism_class_univ C.
proof: Proof. apply morphism_class_subset_antisymm. - intros x y g H. unfold morphism_class_univ. exact tt. - rewrite <- llp_univ. exact (rlp_llp_self _). Qed.
imports: UniMath.MoreFoundations.All UniMath.MoreFoundations.Tactics UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Pullbacks UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Products UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Opp UniMath.CategoryTheory.Chains.Chains UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.ModelCategories.Retract UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Lifting