proposition: Lemma llp_anti {R R' : morphism_class C} (h : R ⊆ R') : llp R' ⊆ llp R.
proof: Proof. unfold "⊆" in *. intros ? ? f H. intros ? ? g K. apply (H _ _ g). apply (h _ _ g). exact K. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Opp UniMath.ModelCategories.Retract UniMath.ModelCategories.MorphismClass UniMath.CategoryTheory.DisplayedCats.Examples.Arrow