{X : pType} : IsHSpace (loops X). Proof. snrapply Build_IsHSpace. - exact concat. - exact concat_1p. - exact concat_p1. Defined.
Require Import Basics Types Pointed WildCat.Core. Require Import Truncations.Core Truncations.Connectedness.