proposition: Lemma MorphismCompEqrel {x y z : ob C} (f : x --> y) (g : y --> z) : (make_eqrel _ (RoofEqrel x z)) (MorToRoof (f · g)) (roof_comp (MorToRoof f) (MorToRoof g)).
proof: Proof. set (Rf := MorToRoof f). set (Rg := MorToRoof g). set (Rfg := MorToRoof (f · g)). unfold roof_comp. set (sqr1 := isLocClassSqr2 iLC Rg Rf y (RoofMor1 Rg) (RoofMor1Is Rg) (RoofMor2 Rf)). set (CR := RoofToCoroof (MorToRoof g)). set (sqrop := isLocClassSqr1 iLC y y z (identity y) (isLocClassIs iLC y) g). assert (H : LocSqr2Mor1 sqr1 · RoofMor2 Rg · CoroofMor2 CR = LocSqr2Mor2 sqr1 · f · g · CoroofMor2 CR). { cbn. fold sqrop. rewrite <- assoc. rewrite <- (LocSqr1Comm sqrop). rewrite id_left. rewrite <- assoc. rewrite <- (LocSqr1Comm sqrop). rewrite id_left. apply cancel_postcomposition. set (tmp := LocSqr2Comm sqr1). cbn in tmp. rewrite id_right in tmp. exact tmp. } set (PostS := isLocClassPost iLC _ _ _ (LocSqr2Mor1 sqr1 · RoofMor2 Rg) (LocSqr2Mor2 sqr1 · f · g) (CoroofMor2 CR) (CoroofMor2Is CR) H). intros P X. apply X. clear X P. use make_RoofTop. - exact PostS. - exact (PostSwitchMor PostS · (LocSqr2Mor2 sqr1)). - exact (PostSwitchMor PostS). - use (isLocClassComp iLC). + use (isLocClassComp iLC). * exact (PostSwitchMorIs PostS). * exact (LocSqr2Mor2Is sqr1). + exact (RoofMor1Is Rfg). - cbn. rewrite assoc. apply idpath. - cbn. set (tmp := PostSwitchEq PostS). cbn in tmp. rewrite assoc in tmp. rewrite assoc in tmp. rewrite assoc in tmp. rewrite assoc. rewrite assoc. exact (! (tmp)). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors