Definition RoofTopToCoroof {x y : ob C} {R1 R2 : Roof x y} (T : RoofTop R1 R2) : ∑ CR : Coroof x y, (RoofMor1 R1 · CoroofMor1 CR = RoofMor2 R1 · CoroofMor2 CR) × (RoofMor1 R2 · CoroofMor1 CR = RoofMor2 R2 · CoroofMor2 CR). Proof. set (sqr1 := isLocClassSqr1 iLC _ _ _ (RoofMor1 R1) (RoofMor1Is R1) (RoofMor2 R1)). set (sqr2 := isLocClassSqr1 iLC _ _ _ (RoofMor1 R2) (RoofMor1Is R2) (RoofMor2 R2)). set (sqr3 := isLocClassSqr1 iLC _ _ _ (LocSqr1Mor2 sqr1) (LocSqr1Mor2Is sqr1) (LocSqr1Mor2 sqr2)). set (mor1 := RoofTopMor1 T · RoofMor1 R1 · LocSqr1Mor1 sqr1 · LocSqr1Mor1 sqr3). set (mor2 := RoofTopMor1 T · RoofMor1 R1 · LocSqr1Mor1 sqr2 · LocSqr1Mor2 sqr3). assert (H : RoofTopMor1 T · RoofMor1 R1 · (LocSqr1Mor1 sqr1 · LocSqr1Mor1 sqr3) = RoofTopMor1 T · RoofMor1 R1 · (LocSqr1Mor1 sqr2 · LocSqr1Mor2 sqr3)). { set (tmp1 := LocSqr1Comm sqr1). set (tmp2 := LocSqr1Comm sqr2). set (tmp3 := LocSqr1Comm sqr3). rewrite assoc. rewrite <- (assoc _ (RoofMor1 R1)). rewrite tmp1. rewrite assoc. rewrite <- assoc. rewrite tmp3. rewrite assoc. rewrite (RoofTopEq2 T). rewrite <- (assoc _ (RoofMor2 R2)). rewrite <- tmp2. rewrite assoc. rewrite (RoofTopEq1 T). rewrite assoc. apply idpath. } set (PreS := isLocClassPre iLC _ _ _ (RoofTopMor1 T · RoofMor1 R1) (RoofTopMor1Is T) (LocSqr1Mor1 sqr1 · LocSqr1Mor1 sqr3) (LocSqr1Mor1 sqr2 · LocSqr1Mor2 sqr3) H). use tpair. - use make_Coroof. + exact PreS. + exact (LocSqr1Mor1 sqr1 · LocSqr1Mor1 sqr3 · PreSwitchMor PreS). + exact (LocSqr1Mor2 sqr2 · LocSqr1Mor2 sqr3 · PreSwitchMor PreS). + use (isLocClassComp iLC). * use (isLocClassComp iLC). -- exact (LocSqr1Mor2Is sqr2). -- exact (LocSqr1Mor2Is sqr3). * exact (PreSwitchMorIs PreS). - cbn. split. + rewrite <- (LocSqr1Comm sqr3). rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. apply cancel_postcomposition. apply cancel_postcomposition. apply (LocSqr1Comm sqr1). + rewrite (PreSwitchEq PreS). rewrite assoc. rewrite assoc. rewrite assoc. rewrite assoc. apply cancel_postcomposition. apply cancel_postcomposition. apply (LocSqr1Comm sqr2). Defined.
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))).