proposition: Theorem equiv_pointify_map `{Funext} (A : Type) (X : pType) : (pointify A ->* X) <~> (A -> X).
proof: Proof. snrapply equiv_adjointify. 1: exact (fun f => f o inl). { intros f. snrapply Build_pMap. { intros [a|]. 1: exact (f a). exact pt. } reflexivity. } 1: intro x; reflexivity. intros f. cbv. pointed_reduce. rapply equiv_path_pforall. snrapply Build_pHomotopy. 1: by intros [a|[]]. reflexivity. Defined.
imports: Basics Types PathAny WildCat Truncations.Core ReflectiveSubuniverse Extensions