`{Funext} {A B : pType} `{IsHSpace A} {f g : B ->* A} (K : pointed_fun f = pointed_fun g) : f = g. Proof. apply path_pforall, hspace_phomotopy_from_homotopy. apply (path_arrow _ _)^-1. exact K. Defined.
Require Import Basics Types Pointed WildCat.Core. Require Import Truncations.Core Truncations.Connectedness.