proposition: Lemma wfs_L_retract (w : wfs C) {x y x' y' : C} {f : x --> y} {f' : x' --> y'} (r : retract f f') (hf : (wfs_L w _ _) f) : (wfs_L w _ _) f'.
proof: Proof. destruct r as [ia [ra [ib [rb [ha [hb [hi hr]]]]]]]. unfold wfs_L. rewrite (wfs_llp w). intros a b g hg h k s. use (wfs'lp w hf hg (h ∘ ra) (k ∘ rb) _). { rewrite <- assoc, s, assoc, assoc, hr. reflexivity. } intro hl. destruct hl as [l [hlh hlk]]. apply hinhpr. exists (l ∘ ib). split. * rewrite assoc, <- hi, <- assoc, hlh, assoc, ha, id_left. reflexivity. * rewrite <- assoc, hlk, assoc, hb, 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