proposition: Lemma RoofEqrel (x y : ob C) : iseqrel (RoofHrel x y).
proof: Proof. use iseqrelconstr. - intros R1 R2 R3 T1' T2'. use (squash_to_prop T1'). apply isapropishinh. intros T1. clear T1'. use (squash_to_prop T2'). apply isapropishinh. intros T2. clear T2'. set (tmp := isLocClassSqr2 iLC T2 T1 x (RoofTopMor1 T2 · RoofMor1 R2) (RoofTopMor1Is T2) (RoofTopMor2 T1 · RoofMor1 R2)). induction tmp as [D1 D2]. induction D1 as [w m]. induction m as [m1 m2]. induction D2 as [D1 D2]. cbn in D1, D2. repeat rewrite assoc in D2. set (tmp := isLocClassPost iLC w R2 x (m1 · RoofTopMor1 T2) (m2 · RoofTopMor2 T1) (RoofMor1 R2) (RoofMor1Is R2) D2). induction tmp as [t p]. intros P X. apply X. clear X P. use make_RoofTop. + exact (pr1 t). + exact ((pr2 t) · m2 · RoofTopMor1 T1). + exact ((pr2 t) · m1 · RoofTopMor2 T2). + repeat rewrite <- assoc. use (isLocClassComp iLC). * exact (dirprod_pr1 p). * use (isLocClassComp iLC). -- exact D1. -- exact (RoofTopMor1Is T1). + induction p as [p1 p2]. repeat rewrite assoc in p2. set (tmp := RoofTopEq1 T2). repeat rewrite <- assoc. rewrite <- tmp. clear tmp. repeat rewrite assoc. repeat rewrite <- (assoc (pr2 t)). rewrite D2. repeat rewrite <- assoc. apply cancel_precomposition. apply cancel_precomposition. exact (RoofTopEq1 T1). + induction p as [p1 p2]. repeat rewrite assoc in p2. set (tmp := RoofTopEq2 T2). repeat rewrite <- assoc. rewrite <- tmp. clear tmp. repeat rewrite assoc. rewrite p2. repeat rewrite <- assoc. apply cancel_precomposition. apply cancel_precomposition. exact (RoofTopEq2 T1). - intros R1. intros P X. apply X. clear X P. use make_RoofTop. + exact R1. + exact (identity R1). + exact (identity R1). + rewrite id_left. exact (RoofMor1Is R1). + apply idpath. + apply idpath. - intros R1 R2 T'. use (squash_to_prop T'). apply isapropishinh. intros T. clear T'. intros P X. apply X. clear X P. use make_RoofTop. + exact T. + exact (RoofTopMor2 T). + exact (RoofTopMor1 T). + rewrite <- (RoofTopEq1 T). exact (RoofTopMor1Is T). + exact (! (RoofTopEq1 T)). + exact (! (RoofTopEq2 T)). Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors