proposition: Lemma RoofEqclassCompToRoofComp {x y z : C} (R1 : Roof x y) (R2 : Roof y z) : @compose loc_precategory x y z (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2) = (RoofEqclassFromRoof (roof_comp R1 R2)).
proof: Proof. apply RoofEqclassEqRoof. apply (pr2 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))). - apply RoofEqclassFromRoofIn. - apply RoofEqclassFromRoofIn. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors