proposition: Lemma lifting_data_Jg_iff_maps : right_lifting_data J f <-> ∑ (γ : ρ1 --> f), Λ1 · γ = identity _.
proof: Proof. apply (logeq_trans lifting_data_Jg_iff_lifting_coprod_lp). apply (logeq_trans lifting_coprod_lp_iff_lifting_coprod_lp_red). split; intro H. - destruct H as [l [lcomm1 lcomm2]]. use tpair. * use mors_to_arrow_mor. + exact l. + exact (identity _). + abstract ( etrans; [exact lcomm2|]; apply pathsinv0; apply id_right ). * use arrow_mor_eq. + exact lcomm1. + apply id_left. - destruct H as [γ γcomm]. exists (arrow_mor00 γ). set (γcomm1 := arrow_mor00_eq γcomm). set (γcomm2 := arrow_mor11_eq γcomm). split. * exact γcomm1. * etrans. exact (arrow_mor_comm γ). etrans. apply cancel_precomposition. etrans. exact (pathsinv0 (id_left _)). exact γcomm2. apply id_right. 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