proposition: Lemma roof_comp_iscontr (x y z : ob C) (e1 : RoofEqclass x y) (e2 : RoofEqclass y z) : iscontr (∑ e3 : RoofEqclass x z, ∏ (f : Roof x y) (s1 : (RoofEqclassIn e1) f) (g : Roof y z) (s2 : (RoofEqclassIn e2) g), (RoofEqclassIn e3) (roof_comp f g)).
proof: Proof. induction e1 as [e1 e1eq]. induction e2 as [e2 e2eq]. use (squash_to_prop (dirprod_pr1 e1eq)). apply isapropiscontr. intros R1. induction R1 as [R1 R1']. use (squash_to_prop (dirprod_pr1 e2eq)). apply isapropiscontr. intros R2. induction R2 as [R2 R2']. use tpair. - use tpair. + use make_RoofEqclass. * exact (λ RR : (Roof x z), (make_eqrel _ (RoofEqrel x z)) RR (roof_comp R1 R2)). * use iseqclassconstr. -- intros P X. apply X. clear X P. use tpair. ++ exact (roof_comp R1 R2). ++ use eqrelrefl. -- intros R3 R4 H1 H2. cbn beta in H2. cbn beta. use (squash_to_prop H1). apply propproperty. intros T1. use (squash_to_prop H2). apply propproperty. intros T2. apply eqrelsymm in H1. use eqreltrans. ++ exact R3. ++ exact H1. ++ exact H2. -- intros R3 R4 H1 H2. cbn beta in H1, H2. apply eqrelsymm in H2. use eqreltrans. ++ exact (roof_comp R1 R2). ++ exact H1. ++ exact H2. + cbn. intros R3 R3' R4 R4'. set (tmp1 := eqax2 e1eq R1 R3 R1' R3'). set (tmp2 := eqax2 e2eq R2 R4 R2' R4'). set (tmp_pre := roof_pre_comp R1 R3 tmp1 R4). set (tmp_post := roof_post_comp R1 R2 R4 tmp2). assert (X : (make_eqrel (RoofHrel x z) (RoofEqrel x z)) (roof_comp R3 R4) (roof_comp R1 R2)). { apply eqrelsymm. use eqreltrans. - exact (roof_comp R1 R4). - exact tmp_post. - exact tmp_pre. } exact X. - intros t. use total2_paths_f. + use RoofEqclassEq. * intros R HR. cbn. set (tmp1 := eqax2 (pr2 (pr1 t))). apply tmp1. -- exact HR. -- apply (pr2 t). ++ cbn. exact R1'. ++ cbn. exact R2'. * intros R HR. cbn in HR. set (tmp1 := eqax1 (pr2 (pr1 t))). apply (tmp1 (roof_comp R1 R2)). -- apply eqrelsymm. apply HR. -- apply (pr2 t). ++ cbn. exact R1'. ++ cbn. exact R2'. + apply proofirrelevance. apply impred_isaprop. intros t0. apply impred_isaprop. intros t1. apply impred_isaprop. intros t2. apply impred_isaprop. intros t3. apply impred_isaprop. intros t4. apply impred_isaprop. intros t5. apply propproperty. Qed.
imports: UniMath.Foundations.PartD UniMath.Foundations.Propositions UniMath.Foundations.Sets UniMath.CategoryTheory.Core.Categories UniMath.CategoryTheory.Core.Isos UniMath.CategoryTheory.Core.Functors