proposition: Lemma RoofEqclassCompInvRToId {x y : ob C} (f1 : Roof x y) : @compose loc_precategory _ _ _ (RoofEqclassFromRoof (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))) (RoofEqclassFromRoof (MorToRoof (RoofMor1 f1))) = (RoofEqclassFromRoof (IdRoof x)).
proof: Proof. set (R1 := (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))). set (R2 := (MorToRoof (RoofMor1 f1))). set (tmp := pr2 (pr1 (roof_comp_iscontr x f1 x (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))). cbn in tmp. use pathscomp0. - exact (RoofEqclassFromRoof (roof_comp R1 R2)). - use RoofEqclassEqRoof. apply tmp. + apply RoofEqclassFromRoofIn. + apply RoofEqclassFromRoofIn. - apply RoofEqClassEq1. intros P X. apply X. clear X P. clear tmp. unfold roof_comp. set (sqr := (isLocClassSqr2 iLC R2 R1 f1 (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R1))). use make_RoofTop. + exact sqr. + cbn. exact (identity sqr). + exact (LocSqr2Mor2 sqr · (RoofMor1 f1)). + use (isLocClassComp iLC). * exact (isLocClassIs iLC _). * exact (RoofMor1Is _). + rewrite id_left. cbn. rewrite id_right. apply idpath. + rewrite id_left. rewrite id_right. cbn. set (tmp := LocSqr2Comm sqr). cbn in tmp. rewrite id_right in tmp. rewrite id_right in tmp. rewrite tmp. 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