proposition: Lemma loc_id_left_in {x y : loc_precategory_data} (f : loc_precategory_data⟦x, y⟧) (R1 : Roof x y) (H1 : RoofEqclassIn f R1) : pr1 (identity x · f) (roof_comp (IdRoof x) R1).
proof: Proof. apply (pr2 (pr1 (roof_comp_iscontr x x y (IdRoofEqclass x) f))). - apply RoofEqclassFromRoofIn. - apply H1. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors