proposition: Lemma roof_comp_iscontr_eqclass {x y z : ob C} (R1 : RoofEqclass x y) (R2 : RoofEqclass y z) (R1' : Roof x y) (R1'' : RoofEqclassIn R1 R1') (R2' : Roof y z) (R2'' : RoofEqclassIn R2 R2') : pr1 (pr1 (roof_comp_iscontr x y z R1 R2)) = RoofEqclassFromRoof (roof_comp R1' R2').
proof: Proof. set (tmp := pr2 (pr1 (roof_comp_iscontr x y z R1 R2)) R1' R1'' R2' R2''). use RoofEqclassEq. - intros R3 HR3. use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof (roof_comp R1' R2')))). + exact (roof_comp R1' R2'). + use (eqax2 (RoofEqclassIs (pr1 (pr1 (roof_comp_iscontr x y z R1 R2))))). * exact tmp. * exact HR3. + apply RoofEqclassFromRoofIn. - intros R3 HR3. use (eqax1 (RoofEqclassIs (pr1 (pr1 (roof_comp_iscontr x y z R1 R2))))). + exact (roof_comp R1' R2'). + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof (roof_comp R1' R2')))). * apply RoofEqclassFromRoofIn. * exact HR3. + apply tmp. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors