proposition: Lemma llp_iff_lift_with_R {C : category} (w : wfs C) {x y : C} (f : x --> y) (H : ∑ z (g : x --> z) (h : z --> y), (wfs_L w _ _) g × (wfs_R w _ _) h × h ∘ g = f) : lp (pr12 H) f <-> (wfs_R w _ _) f.
proof: Proof. destruct H as [z [g [h [Lg [Rh Hgh]]]]]. split. - intro hf. unfold wfs_R. rewrite (wfs_rlp w). intros a b g' hg'. intros top bottom comm_total. use (hf (identity _) h). { rewrite id_left. apply pathsinv0. exact (Hgh). } intro h'. destruct h' as [lift_lff [comm_lff1 comm_lff2]]. assert (lp g' h) as lp_grf. { set (rf_r := Rh). unfold wfs_R in rf_r. rewrite (wfs_rlp w) in rf_r. exact (rf_r _ _ g' hg'). } use (lp_grf (g ∘ top) bottom). { rewrite <- assoc. rewrite (Hgh). exact comm_total. } intro H. destruct H as [lift_grf [comm_grf1 comm_grf2]]. apply hinhpr. exists (lift_lff ∘ lift_grf). split. * etrans. apply assoc. etrans. apply cancel_postcomposition. exact comm_grf1. etrans. apply assoc'. etrans. apply cancel_precomposition. exact comm_lff1. apply id_right. * etrans. apply assoc'. etrans. apply cancel_precomposition. exact comm_lff2. exact comm_grf2. - intro hf. intros h' k Hk. unfold wfs_R in hf. rewrite wfs_rlp in hf. use hf. exact (Lg). 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