proposition: Lemma lp_of_retracts {C : category} {a b x y a' b' x' y' : C} {f : x --> y} {f' : x' --> y'} {g : a --> b} {g' : a' --> b'} (rf : retract f' f) (rg : retract g' g) : (lp f' g') -> (lp f g).
proof: Proof. intros Hlp h k Hcomm. destruct rf as [ia [ra [ib [rb [ha [hb [hif hrf]]]]]]]. destruct rg as [ix [rx [iy [ry [hx [hy [hig hrg]]]]]]]. use Hlp. - exact (ra · h · ix). - exact (rb · k · iy). - rewrite <- assoc, hig, assoc, <- (assoc _ h g), Hcomm, assoc, hrf, assoc, assoc. reflexivity. - intro Hl. destruct Hl as [l [H1 H2]]. apply hinhpr. exists (ib · l · rx). split. * rewrite assoc, assoc, <- hif, <- (assoc _ f' l), H1, assoc, assoc. now rewrite ha, id_left, <- assoc, hx, id_right. * rewrite <- assoc, hrg, assoc, <- (assoc _ l g'), H2, assoc, assoc. now rewrite hb, id_left, <- assoc, hy, id_right. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Limits.Opp UniMath.ModelCategories.Retract UniMath.ModelCategories.MorphismClass UniMath.CategoryTheory.DisplayedCats.Examples.Arrow