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. 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.
Require Import UniMath.Foundations.PartD. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.Sets. Require Import UniMath.CategoryTheory.Core.Categories. Require Import UniMath.CategoryTheory.Core.Isos. Require Import UniMath.CategoryTheory.Core.Functors. Definition RoofEqclassFromRoof {x y : ob C} (R : Roof x y) : RoofEqclass x y. Definition RoofEqclassFromRoofIn {x y : ob C} (R : Roof x y) : RoofEqclassIn (RoofEqclassFromRoof R) R. (R : Roof x y) (HR : RoofEqclassIn RE R) : RE = RoofEqclassFromRoof R. use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R))). + apply RoofEqclassFromRoofIn. + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof R))). * apply RoofEqclassFromRoofIn. (H1 : RoofEqclassIn (RoofEqclassFromRoof R1) R2) RoofEqclassIn (RoofEqclassFromRoof R1) R3. exact (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R1)) R2 R3 H2 H1). RoofEqclassIn (pr1 (pr1 (roof_comp_iscontr _ _ _ (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))) use (pr2 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))). - apply RoofEqclassFromRoofIn. - apply RoofEqclassFromRoofIn. exact (RoofEqclassFromRoof (make_Roof x x x (identity x) (identity x) (isLocClassIs iLC x))). - apply RoofEqclassFromRoofIn. - apply RoofEqclassFromRoofIn. * apply RoofEqclassFromRoofIn. - apply RoofEqclassFromRoofIn. * apply RoofEqclassFromRoofIn. RoofEqclassFromRoof (MorToRoof (f · g)) = pr1 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof (MorToRoof f)) (RoofEqclassFromRoof (MorToRoof g)))). set (eqclass := pr1 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof (MorToRoof f)) (RoofEqclassFromRoof (MorToRoof g))))). set (cont := pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof (MorToRoof f)) (RoofEqclassFromRoof (MorToRoof g)))). * set (HR' := RoofEqclassFromRoofIn (MorToRoof (f · g))). use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof (MorToRoof (f · g))))). use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof (MorToRoof (f · g))))). + apply RoofEqclassFromRoofIn. + intros x y f. exact (RoofEqclassFromRoof (MorToRoof f)). pr1 (pr1 (roof_comp_iscontr x y z R1 R2)) = RoofEqclassFromRoof (roof_comp R1' R2'). use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof (roof_comp R1' R2')))). + apply RoofEqclassFromRoofIn. + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof (roof_comp R1' R2')))). * apply RoofEqclassFromRoofIn. Definition InvRoofFromMorInSom {x y : C} (s : y --> x) (S : SOM y x s) : Roof x y. (make_eqrel _ (RoofEqrel x y)) R (roof_comp (InvRoofFromMorInSom (RoofMor1 R) (RoofMor1Is R)) (InvRoofFromMorInSom (RoofMor1 R) (RoofMor1Is R)) R (RoofMor2 (InvRoofFromMorInSom (RoofMor1 R) (RoofMor1Is R)))). @compose loc_precategory x y z (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2) = (RoofEqclassFromRoof (roof_comp R1 R2)). apply (pr2 (pr1 (roof_comp_iscontr x y z (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))). - apply RoofEqclassFromRoofIn. - apply RoofEqclassFromRoofIn. (RoofEqclassFromRoof R1) = (RoofEqclassFromRoof R2). use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R2))). + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof R1))). * exact (RoofEqclassFromRoofIn R1). + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof R2))). * exact (RoofEqclassFromRoofIn R2). use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R1))). + use (eqax2 (RoofEqclassIs (RoofEqclassFromRoof R2))). * exact (RoofEqclassFromRoofIn R2). + use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R1))). * exact (RoofEqclassFromRoofIn R1). (RoofEqclassFromRoof (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))) (RoofEqclassFromRoof (MorToRoof (RoofMor1 f1))) = (RoofEqclassFromRoof (IdRoof x)). set (R1 := (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))). set (tmp := pr2 (pr1 (roof_comp_iscontr x f1 x (RoofEqclassFromRoof R1) (RoofEqclassFromRoof R2)))). - exact (RoofEqclassFromRoof (roof_comp R1 R2)). + apply RoofEqclassFromRoofIn. + apply RoofEqclassFromRoofIn. RoofEqclassFromRoof R = RoofEqclassFromRoof (roof_comp (InvRoofFromMorInSom (RoofMor1 R) (RoofMor1Is R)) (MorToRoof (RoofMor2 R))). use (eqax1 (RoofEqclassIs (RoofEqclassFromRoof R))). - apply RoofEqclassFromRoofIn. apply RoofEqclassFromRoofIn. D hsD F H' x z (RoofEqclassFromRoof (roof_comp R1' R2')))) (roof_comp R1' R2') (RoofEqclassFromRoofIn (roof_comp R1' R2'))). use (pathscomp0 (MorMap_iscontr_eq D hsD F H' a b (RoofEqclassFromRoof (MorToRoof f)) (MorToRoof f) (RoofEqclassFromRoofIn _))). H' a b (RoofEqclassFromRoof f1))) f1 (RoofEqclassFromRoofIn f1)))). rewrite <- (RoofEqclassCompToRoofComp (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1)) (RoofEqclassFromRoof (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))) (RoofEqclassFromRoof (MorToRoof (RoofMor2 f1))))). (RoofEqclassFromRoof (InvRoofFromMorInSom (RoofMor1 f1) (RoofMor1Is f1))) (RoofEqclassFromRoof (MorToRoof (RoofMor1 f1)))). - exact (RoofEqclassFromRoof (InvRoofFromMorInSom f s)). + set (sqr := isLocClassSqr2 iLC (InvRoofFromMorInSom f s) (MorToRoof f) y (RoofMor1 (InvRoofFromMorInSom f s)) (RoofMor1Is (InvRoofFromMorInSom f s)) + set (sqr := isLocClassSqr2 iLC (MorToRoof f) (InvRoofFromMorInSom f s) x (RoofMor2 (InvRoofFromMorInSom f s))).