fix instance cycle in Homotopy.HSpace.Core

HoTT · Sep 3, 2023 · 8d8e633 · 8d8e633
1 parent 6c2c3f6
commit 8d8e633
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/Homotopy/HSpace/Core.v b/theories/Homotopy/HSpace/Core.v
@@ -90,7 +90,7 @@ Definition homogeneous_pt_id_beta `{Funext} {A : pType} `{IsHomogeneous A}
   := ltac:(apply path_pequiv, peisretr).
 
 (** This modified structure makes any homogeneous type into a (left-invertible) H-space. *)
-Global Instance ishspace_homogeneous {A : pType} `{IsHomogeneous A}
+Definition ishspace_homogeneous {A : pType} `{IsHomogeneous A}
   : IsHSpace A.
 Proof.
   snrapply Build_IsHSpace.