`{Funext} {A B : pType} `{IsHSpace A} {f g : B ->* A} (K : f == g) : f ==* g. Proof. snrapply (phomotopy_from_homotopy _ _ K). - intro a. exact (fmap loops (pmap_hspace_left_op a o* (pequiv_hspace_left_op pt)^-1*)). - lazy beta. transitivity (fmap (b:=A) loops pmap_idmap). 2: rapply (fmap_id loops). rapply (fmap2 loops). nrapply peisretr. Defined.
Require Import Basics Types Pointed WildCat.Core. Require Import Truncations.Core Truncations.Connectedness.