proposition: Lemma isaprop_is_wfs {C : category} (L R : morphism_class C) : isaprop (is_wfs L R).
proof: Proof. apply isapropdirprod. - unfold isaprop. exact (isasetmorphism_class _ _). - apply isapropdirprod. * exact (isasetmorphism_class _ _). * do 3 (apply impred_isaprop; intro). apply propproperty. 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