proposition: Lemma FunctorToLocalization_comp {x y z : ob C} (f : x --> y) (g : y --> z) : RoofEqclassFromRoof (MorToRoof (f · g)) = pr1 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof (MorToRoof f)) (RoofEqclassFromRoof (MorToRoof g)))).
proof: Proof. set (tmpp := roof_comp_iscontr_in x y z (MorToRoof f) (MorToRoof g)). set (eqclass := pr1 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof (MorToRoof f)) (RoofEqclassFromRoof (MorToRoof g))))). fold eqclass in tmpp. set (cont := pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof (MorToRoof f)) (RoofEqclassFromRoof (MorToRoof g)))). set (cont' := pr2 cont). cbn in cont, cont'. use RoofEqclassEq. - intros R HR. unfold RoofEqclassIn in tmpp. use (eqax1 (RoofEqclassIs eqclass)). + exact (roof_comp (MorToRoof f) (MorToRoof g)). + use eqreltrans. * exact (MorToRoof (f · g)). * apply eqrelsymm. apply MorphismCompEqrel. * set (HR' := RoofEqclassFromRoofIn (MorToRoof (f · g))). use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof (MorToRoof (f · g))))). -- exact HR'. -- exact HR. + exact tmpp. - intros R HR. use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof (MorToRoof (f · g))))). + exact (MorToRoof (f · g)). + use eqreltrans. * exact (roof_comp (MorToRoof f) (MorToRoof g)). * apply MorphismCompEqrel. * use (eqax2 (RoofEqclassIs eqclass)). -- exact tmpp. -- exact HR. + 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