proposition: Lemma lifting_data_impl_lifting_coprod_lp : right_lifting_data J f -> elp (morcls_lp_coprod) f.
proof: Proof. intro rldJf. intros h k S. set (hj := λ (j : morcls_lp J f), (CoproductIn _ j) · h). set (kj := λ (j : morcls_lp J f), (CoproductIn _ j) · k). assert (∏ (j : morcls_lp J f), ∑ lj, ((pr1 (morcls_lp_map j)) · lj = hj j) × (lj · f = kj j)) as jlift. { intro j. use (rldJf (pr1 (morcls_lp_map j)) (pr2 (morcls_lp_map j))). etrans. apply assoc'. etrans. apply cancel_precomposition. exact S. etrans. apply assoc. apply pathsinv0. etrans. apply assoc. apply pathsinv0. etrans. apply cancel_postcomposition. exact (CoproductOfArrows'In _ _ _ _ _ j). reflexivity. } set (jlifts := foralltototal _ _ jlift). destruct jlifts as [lj hlj]. set (hl := isCoproduct_Coproduct _ _ (morcls_lp_cod_coprod) _ lj). destruct hl as [[l hl] uniqueness]. exists l. split; rewrite CoproductArrowEta, (CoproductArrowEta _ _ _ _ _ l). - etrans. apply (precompWithCoproductArrow). apply CoproductArrowUnique. intro j. etrans. apply (CoproductInCommutes (morcls_lp_dom_coprod)). destruct (hlj j) as [hljcomm _]. apply pathsinv0. etrans. exact (pathsinv0 hljcomm). etrans. apply cancel_precomposition. exact (pathsinv0 (hl j)). reflexivity. - apply CoproductArrowUnique. intro j. etrans. apply assoc. etrans. apply cancel_postcomposition. apply (CoproductInCommutes (morcls_lp_cod_coprod)). destruct (hlj j) as [_ kljcomm]. apply pathsinv0. etrans. exact (pathsinv0 kljcomm). etrans. apply cancel_postcomposition. exact (pathsinv0 (hl j)). reflexivity. Qed.
imports: UniMath.MoreFoundations.All UniMath.CategoryTheory.Core.Prelude UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.opp_precat UniMath.CategoryTheory.Core.Functors UniMath.CategoryTheory.Core.NaturalTransformations UniMath.CategoryTheory.PrecategoryBinProduct UniMath.CategoryTheory.Monads.Monads UniMath.CategoryTheory.Monads.MonadAlgebras UniMath.CategoryTheory.catiso UniMath.CategoryTheory.Limits.BinCoproducts UniMath.CategoryTheory.Limits.Graphs.Colimits UniMath.CategoryTheory.Limits.Graphs.Coequalizers UniMath.CategoryTheory.Limits.Coproducts UniMath.CategoryTheory.Limits.Pushouts UniMath.CategoryTheory.Equivalences.Core UniMath.CategoryTheory.DisplayedCats.Core UniMath.CategoryTheory.DisplayedCats.SIP UniMath.CategoryTheory.DisplayedCats.Total UniMath.CategoryTheory.DisplayedCats.Functors UniMath.CategoryTheory.DisplayedCats.Constructions UniMath.CategoryTheory.DisplayedCats.Equivalences UniMath.CategoryTheory.DisplayedCats.Examples.Opposite UniMath.CategoryTheory.DisplayedCats.Examples.Arrow UniMath.CategoryTheory.DisplayedCats.Examples.Three UniMath.ModelCategories.MorphismClass UniMath.ModelCategories.Retract UniMath.ModelCategories.Lifting UniMath.ModelCategories.NWFS UniMath.ModelCategories.NWFSisWFS UniMath.ModelCategories.Helpers