Remove some Global Instances

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).

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)

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.

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

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.

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. *)