proposition: Lemma wfs_isos_univ : is_wfs (morphism_class_isos C) (morphism_class_univ C).
proof: Proof. use make_is_wfs; try symmetry. - exact llp_univ. - exact rlp_isos. - intros x y f. apply hinhpr. exists x, (identity x), f. repeat split. * exact (identity_is_iso C x). * rewrite 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