{A : pType} `{IsHomogeneous A} : IsHSpace A. Proof. snrapply Build_IsHSpace. - exact (fun a b => homogeneous_pt_id a b). - intro a; cbn. apply eisretr. - intro a. exact (point_eq (homogeneous_pt_id a)). Defined.
Require Import Basics Types Pointed WildCat.Core. Require Import Truncations.Core Truncations.Connectedness.