Build_pEquiv' {A B : pType} (f : A <~> B) (p : f (point A) = point B) : A <~>* B := Build_pEquiv _ _ (Build_pMap _ _ f p) _.
Require Import Basics. Require Import Types. Require Import WildCat. Require Import Pointed.Core.