From 8d8e633be656cc4e2be8ae0f39713657e5c99f3c Mon Sep 17 00:00:00 2001
From: "Jarl G. Taxeraas Flaten" <jtaxers@uwo.ca>
Date: Sun, 3 Sep 2023 09:52:27 +0200
Subject: [PATCH] fix instance cycle in Homotopy.HSpace.Core

---
 theories/Homotopy/HSpace/Core.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/Homotopy/HSpace/Core.v b/theories/Homotopy/HSpace/Core.v
index 62d521ea0e2..de7a9461c08 100644
--- 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.