Remove three Local Instances that are already Global Instances

HoTT · Jan 1, 2024 · ab2543e · ab2543e
1 parent e6a719d
commit ab2543e
Show file tree

Hide file tree

Showing 2 changed files with 0 additions and 6 deletions.
diff --git a/theories/Algebra/Groups/ShortExactSequence.v b/theories/Algebra/Groups/ShortExactSequence.v
@@ -38,9 +38,6 @@ Proof.
   exact (grp_homo_unit f).
 Defined.
 
-Local Existing Instance ishprop_phomotopy_hset.
-Local Existing Instance ishprop_isexact_hset.
-
 (** A complex 0 -> A -> B of groups is purely exact if and only if the map A -> B is an embedding. *)
 Lemma iff_grp_isexact_isembedding `{Funext} {A B : Group} (f : A $-> B)
   : IsExact purely (@grp_homo_const grp_trivial A) f <-> IsEmbedding f.

diff --git a/theories/Homotopy/ExactSequence.v b/theories/Homotopy/ExactSequence.v
@@ -127,14 +127,11 @@ Proof.
     exact (concat_p1 _ @ concat_1p _).
 Defined.
 
-Local Existing Instance ishprop_phomotopy_hset.
-
 (** If Y is a set, then IsComplex is an HProp. *)
 Global Instance ishprop_iscomplex_hset `{Univalence} {F X Y : pType} `{IsHSet Y}
   (i : F ->* X) (f : X ->* Y)
   : IsHProp (IsComplex i f) := {}.
 
-
 (** ** Very short exact sequences and fiber sequences *)
 
 (** A complex is [n]-exact if the induced map [cxfib] is [n]-connected.  *)