From 0742e50270e62ef6d8d5a52b90325bf8560bbbab Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Thu, 18 Jan 2024 09:53:50 -0500
Subject: [PATCH 1/2] Remove some Global Instances

---
 theories/Modalities/Descent.v | 6 +++---
 theories/Modalities/Lex.v     | 2 +-
 theories/Types/Unit.v         | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/Modalities/Descent.v b/theories/Modalities/Descent.v
index f129294e4c3..72749d4bd3a 100644
--- a/theories/Modalities/Descent.v
+++ b/theories/Modalities/Descent.v
@@ -64,8 +64,8 @@ Section LeftExactness.
 Universe i.
 Context (O' O : ReflectiveSubuniverse@{i}) `{O << O', O <<< O'}.
 
-(** Proposition 2.30 of CORS and Theorem 3.1(xii) of RSS: any [O']-equivalence is [O]-connected.  The special case when [f = to O' A] requires only [O << O'], but the general case seems to require [O <<< O']. *)
-Global Instance conn_map_OO_inverts
+(** Proposition 2.30 of CORS and Theorem 3.1(xii) of RSS: any [O']-equivalence is [O]-connected.  The special case when [f = to O' A] requires only [O << O'], but the general case seems to require [O <<< O']. It is convenient to have this as an instance in this file, but we don't make it global, as it requires that Coq guess [O']. *)
+Local Instance conn_map_OO_inverts
        {A B : Type} (f : A -> B) `{O_inverts O' f}
   : IsConnMap O f.
 Proof.
@@ -261,7 +261,7 @@ Definition OO_isconnected_hfiber
   := OO_conn_map_isconnected f x.
 
 (** Theorem 3.1(iv) of RSS: an [O]-modal map between [O']-connected types is an equivalence. *)
-Global Instance OO_isequiv_mapino_isconnected
+Definition OO_isequiv_mapino_isconnected
        {Y X : Type} `{IsConnected O' Y, IsConnected O' X} (f : Y -> X) `{MapIn O _ _ f}
   : IsEquiv f.
 Proof.
diff --git a/theories/Modalities/Lex.v b/theories/Modalities/Lex.v
index ce79479cd72..cb761887e1a 100644
--- a/theories/Modalities/Lex.v
+++ b/theories/Modalities/Lex.v
@@ -34,7 +34,7 @@ Section LexModality.
     := OO_conn_map_isconnected O O f.
 
   (** RSS Theorem 3.1 (iv) *)
-  Global Instance isequiv_mapino_isconnected
+  Definition isequiv_mapino_isconnected
          {Y X : Type} `{IsConnected O Y, IsConnected O X}
          (f : Y -> X) `{MapIn O _ _ f}
     : IsEquiv f
diff --git a/theories/Types/Unit.v b/theories/Types/Unit.v
index 739db0772e7..3ab36cc309c 100644
--- a/theories/Types/Unit.v
+++ b/theories/Types/Unit.v
@@ -111,8 +111,8 @@ Global Instance contr_unit : Contr Unit | 0 := Build_Contr _ tt (fun t : Unit =>
 Definition equiv_contr_unit `{Contr A} : A <~> Unit
   := equiv_contr_contr.
 
-(* Conversely, a type equivalent to [Unit] is contractible. *)
-Global Instance contr_equiv_unit (A : Type) (f : A <~> Unit) : Contr A | 10000
+(* Conversely, a type equivalent to [Unit] is contractible. We don't make this an instance because Coq would have to guess the equivalence.  And when it has a map in mind, it would try to use [isequiv_contr_contr], which would cause a cycle. *)
+Definition contr_equiv_unit (A : Type) (f : A <~> Unit) : Contr A
   := contr_equiv' Unit f^-1%equiv.
 
 (** The constant map to [Unit].  We define this so we can get rid of an unneeded universe variable that Coq generates when [const tt] is used in a context that doesn't have [Universe Minimization ToSet] as this file does. If we ever set that globally, then we could get rid of this and remove some imports of this file. *)

From eb521ed132ce6078f7659ed4da585874668fa521 Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Thu, 18 Jan 2024 11:19:51 -0500
Subject: [PATCH 2/2] Supply some implicit variables

---
 theories/HIT/V.v                            | 2 +-
 theories/Homotopy/EMSpace.v                 | 2 +-
 theories/Modalities/ReflectiveSubuniverse.v | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/HIT/V.v b/theories/HIT/V.v
index ae2e9fd274b..7825706e6a6 100644
--- a/theories/HIT/V.v
+++ b/theories/HIT/V.v
@@ -395,7 +395,7 @@ Proof.
     apply setext'; split.
     + intro a. apply tr; exists (eu a). exact (ap10 factor a).
     + intro a'. generalize (epi_eu a').
-      intros ?; refine (Trunc_functor (-1) _ (center _)).
+      intro IC; refine (Trunc_functor (-1) _ (@center _ IC)).
       intros [a p]. exists a. transitivity (mu (eu a)).
       * exact (ap10 factor a).
       * exact (ap mu p).
diff --git a/theories/Homotopy/EMSpace.v b/theories/Homotopy/EMSpace.v
index 8e59a4090c8..8d383827956 100644
--- a/theories/Homotopy/EMSpace.v
+++ b/theories/Homotopy/EMSpace.v
@@ -235,7 +235,7 @@ Section EilenbergMacLane.
     nrapply O_inverts_conn_map.
     nrapply (isconnmap_pred_add n.-2).
     rewrite 2 trunc_index_add_succ.
-    rapply conn_map_loop_susp_unit.
+    apply (conn_map_loop_susp_unit n X).
   Defined.
 
   Lemma pequiv_loops_em_em (G : AbGroup) (n : nat)
diff --git a/theories/Modalities/ReflectiveSubuniverse.v b/theories/Modalities/ReflectiveSubuniverse.v
index ca73853d54c..8ba564a627f 100644
--- a/theories/Modalities/ReflectiveSubuniverse.v
+++ b/theories/Modalities/ReflectiveSubuniverse.v
@@ -1636,7 +1636,7 @@ Section ConnectedMaps.
   : forall b:B, P b.
   Proof.
     intros b.
-    refine (pr1 (isconnected_elim O _ _)).
+    refine (pr1 (isconnected_elim O (A:=hfiber f b) _ _)).
     intros [a p].
     exact (transport P p (d a)).
   Defined.