proposition: Lemma check4 X Y (w:X≅Y) : Equivalence_toSourceHomotopy (weq_to_Equivalence (Equivalence_to_weq w)) = Equivalence_toSourceHomotopy w.
proof: Proof. try reflexivity. revert w. intros [f [g [p [q h]]]]. unfold Equivalence_toSourceHomotopy; simpl. apply funextsec; intros x. try reflexivity. Abort. Definition weq_to_Equivalence' X Y : X ≃ Y -> Equivalence X Y. intros [f r]. unfold isweq in r. set (g := λ y, hfiberpr1 f y (pr1 (r y))). set (p := λ y, pr2 (pr1 (r y))). simpl in p. set (L := λ x, pr2 (r (f x)) (make_hfiber f x (idpath (f x)))). set (q := λ x, maponpaths pr1 (L x)). set (q' := λ x, !q x). exact (makeEquivalence X Y f g p q' (λ x, ! transportf_fun_idpath x (pr1 (pr1 (r (f x)))) (q x) (idpath (f x)) @ (fiber_paths (L x)))). Defined.
imports: UniMath.Foundations.All UniMath.MoreFoundations.Notations UniMath.MoreFoundations.Tactics