proposition: Lemma lp_isos_univ {x y a b : C} (f : x --> y) (g : a --> b) : (morphism_class_isos C _ _ f) -> lp f g.
proof: Proof. intro H. set (fiso := make_iso _ H). change (lp fiso g). intros h k s. apply hinhpr. exists (h ∘ (inv_from_iso fiso)). split. * rewrite assoc, iso_inv_after_iso, id_left. reflexivity. * rewrite <- assoc, s, assoc. rewrite iso_after_iso_inv, id_left. reflexivity. 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