proposition: Lemma retract_argument {L' : morphism_class C} (w : wfs C) (H : wfs_fact_ax L' (wfs_R w)) : ∏ {x y} (f : x --> y), (wfs_L w _ _) f -> ∃ {x' y'} (f' : x' --> y') (r : retract f' f), (L' _ _) f'.
proof: Proof. intros x y f hf. specialize (H _ _ f) as eHf. simpl in eHf. use (hinhuniv _ eHf). intro Hf. destruct Hf as [z [g [h [hg [hh hgh]]]]]. use (wfs'lp w hf hh g (identity _)). { rewrite hgh, id_right. reflexivity. } intro hl. destruct hl as [l [hl1 hl2]]. assert (r : retract g f). { use (make_retract (identity _) (identity _) l h). use make_is_retract. - now rewrite id_left. - assumption. - rewrite id_left. now symmetry. - rewrite id_left. now symmetry. } apply hinhpr. exists x, z, g, r. exact hg. 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