proposition: Lemma llp_univ : llp (morphism_class_univ C) = morphism_class_isos C.
proof: Proof. apply morphism_class_subset_antisymm; intros x y f H. - specialize ((H _ _ f) tt). use (H (identity _) (identity _)). { rewrite id_left, id_right. reflexivity. } intro hl. destruct hl as [l [hfl hlf]]. unfold morphism_class_isos. assert (is_z_isomorphism f) as f_z_iso. { exists l. split; assumption. } apply is_iso_from_is_z_iso. exact f_z_iso. - intros a b g _. exact (lp_isos_univ f g H). 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