{A B : Type} {P : A -> A -> Type} (e : B <~> A) (Prefl : forall b, P (e b) (e b)) (cp : forall b1, Contr {b2 : B & P (e b1) (e b2)}) : forall a0 a1 : A, P a0 a1 <~> a0 = a1. Proof. apply (equiv_path_along_equiv e). intro a0. srapply equiv_path_from_contr. apply Prefl. Defined.
Require Import Basics. Require Import Types.Sigma Types.Equiv Types.Paths. Require Import HoTT.Tactics.