Lemma roof_post_comp {x y z : ob C} (R1 : Roof x y) (R2 R3 : Roof y z) (e : (make_eqrel (RoofHrel y z) (RoofEqrel y z)) R2 R3) : (make_eqrel (RoofHrel x z) (RoofEqrel x z)) (roof_comp R1 R2) (roof_comp R1 R3). Proof. use (squash_to_prop e). apply propproperty. intros T. clear e. set (T' := RoofTopToCoroof T). induction T' as [CR eq]. intros P X. apply X. clear X P. set (R4 := roof_comp R1 R2). set (R5 := roof_comp R1 R3). unfold roof_comp in R4. unfold roof_comp in R5. set (sqr4 := isLocClassSqr2 iLC R2 R1 y (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R1)). set (sqr5 := isLocClassSqr2 iLC R3 R1 y (RoofMor1 R3) (RoofMor1Is R3) (RoofMor2 R1)). fold sqr4 in R4. fold sqr5 in R5. set (sqr6 := isLocClassSqr2 iLC R5 R4 R1 (LocSqr2Mor2 sqr5) (LocSqr2Mor2Is sqr5) (LocSqr2Mor2 sqr4)). assert (H : LocSqr2Mor1 sqr6 · LocSqr2Mor1 sqr5 · RoofMor2 R3 · CoroofMor2 CR = LocSqr2Mor2 sqr6 · LocSqr2Mor1 sqr4 · RoofMor2 R2 · CoroofMor2 CR). { rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- assoc. rewrite <- (dirprod_pr1 eq). rewrite <- (dirprod_pr2 eq). rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. rewrite <- (assoc _ (LocSqr2Mor1 sqr4)). rewrite (LocSqr2Comm sqr4). rewrite <- (assoc _ (LocSqr2Mor1 sqr5)). rewrite (LocSqr2Comm sqr5). rewrite assoc. rewrite assoc. apply cancel_postcomposition. apply cancel_postcomposition. apply (LocSqr2Comm sqr6). } set (PostS := isLocClassPost iLC _ _ _ (LocSqr2Mor1 sqr6 · LocSqr2Mor1 sqr5 · RoofMor2 R3) (LocSqr2Mor2 sqr6 · LocSqr2Mor1 sqr4 · RoofMor2 R2) (CoroofMor2 CR) (CoroofMor2Is CR) H). use make_RoofTop. - exact PostS. - exact (PostSwitchMor PostS · LocSqr2Mor2 sqr6). - exact (PostSwitchMor PostS · LocSqr2Mor1 sqr6). - use (isLocClassComp iLC). + use (isLocClassComp iLC). * exact (PostSwitchMorIs PostS). * exact (LocSqr2Mor2Is sqr6). + exact (RoofMor1Is R4). - cbn. rewrite assoc. rewrite assoc. apply cancel_postcomposition. set (tmp := ! (LocSqr2Comm sqr6)). apply (maponpaths (λ f : _, PostSwitchMor PostS · f)) in tmp. rewrite assoc in tmp. rewrite assoc in tmp. apply tmp. - cbn. apply pathsinv0. rewrite assoc. rewrite assoc. set (tmp := PostSwitchEq PostS). rewrite assoc in tmp. rewrite assoc in tmp. rewrite assoc in tmp. rewrite assoc in tmp. apply 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))).