Definition InvRoofFromMorInSom {x y : C} (s : y --> x) (S : SOM y x s) : Roof x y. Proof. use make_Roof. - exact y. - exact s. - exact (identity y). - exact S. 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))).