proposition: Lemma IdRoofEqrel_left {x y : ob C} (R1 : Roof x y) : (make_eqrel (RoofHrel x y) (RoofEqrel x y)) R1 (roof_comp (IdRoof x) R1).
proof: Proof. set (comp := roof_comp (IdRoof x) R1). unfold roof_comp in comp. set (sqr := isLocClassSqr2 iLC R1 (IdRoof x) x (RoofMor1 R1) (RoofMor1Is R1) (RoofMor2 (IdRoof x))). fold sqr in comp. apply eqrelsymm. intros P X. apply X. clear X P. use make_RoofTop. - exact comp. - exact (identity comp). - exact (LocSqr2Mor1 sqr). - use (isLocClassComp iLC). + apply (isLocClassIs iLC). + apply (RoofMor1Is comp). - rewrite id_left. cbn. apply (! (LocSqr2Comm sqr)). - cbn. rewrite id_left. apply idpath. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors