{A} `{IsEquiv _ _ (fun (a:A) => (a,a))} : IsHProp A. Proof. apply hprop_allpath; intros x y. set (d := fun (a:A) => (a,a)) in *. transitivity (fst (d (d^-1 (x,y)))). - exact (ap fst (eisretr d (x,y))^). - transitivity (snd (d (d^-1 (x,y)))). + unfold d; reflexivity. + exact (ap snd (eisretr d (x,y))). Defined.
Require Import HoTT.Basics HoTT.Types.