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