equiv_path_pequiv' `{Funext} {A B : pType} (f g : A <~>* B) : (f = g :> (A ->* B)) <~> (f = g :> (A <~>* B)). Proof. refine ((equiv_ap' (issig_pequiv A B)^-1%equiv f g)^-1%equiv oE _); cbn. match goal with |- _ <~> ?F = ?G => exact (equiv_path_sigma_hprop F G) end. Defined.
Require Import Basics Types. Require Import Homotopy.IdentitySystems. Require Import WildCat. Require Import Truncations.Core. Require Import ReflectiveSubuniverse. Require Import Extensions.