{X Y : pType} `{IsHSpace Y} (f : X <~>* Y) : IsHSpace X. Proof. snrapply Build_IsHSpace. - exact (fun a b => f^-1 (f a * f b)). - intro b. rhs_V nrapply (eissect f b). apply ap. lhs nrapply (ap (.* f b) (point_eq f)). apply left_identity. - intro a. rhs_V nrapply (eissect f a). apply ap. lhs nrapply (ap (f a *.) (point_eq f)). apply right_identity. Defined.
Require Import Basics Types Pointed WildCat.Core. Require Import Truncations.Core Truncations.Connectedness.