feat(hott): remove multiple_instances attribute

hott/algebra/category/category.hlean

@@ -34,8 +34,6 @@ namespace category
   -- without it, we would have to explicitly use category.to_precategory
   attribute category.to_precategory [coercion]
 
-  attribute category [multiple_instances]
-
   abbreviation iso_of_path_equiv := @category.iso_of_path_equiv
   attribute category.iso_of_path_equiv [instance]
 

hott/algebra/category/functor/attributes.hlean

@@ -54,8 +54,8 @@ namespace category
   end
 
   theorem reflect_inverse (F : C ⇒ D) [H : fully_faithful F] {c c' : C} (f : c ⟶ c')
-    [H : is_iso f] : (to_fun_hom F)⁻¹ᶠ (F f)⁻¹ = f⁻¹ :=
-  inverse_eq_inverse (idp : to_hom (@(iso.mk f) (reflect_is_iso F f)) = f)
+    [H' : is_iso f] : (to_fun_hom F)⁻¹ᶠ (F f)⁻¹ = f⁻¹ :=
+  @inverse_eq_inverse _ _ _ _ _ _ (reflect_is_iso F f) H' idp
 
   definition hom_equiv_F_hom_F [constructor] (F : C ⇒ D)
     [H : fully_faithful F] (c c' : C) : (c ⟶ c') ≃ (F c ⟶ F c') :=

hott/algebra/category/iso.hlean

@@ -22,7 +22,6 @@ namespace iso
 
   attribute is_iso.inverse [reducible]
 
-  attribute is_iso [multiple_instances]
   open split_mono split_epi is_iso
   abbreviation retraction_of [unfold 6] := @split_mono.retraction_of
   abbreviation retraction_comp [unfold 6] := @split_mono.retraction_comp
@@ -79,7 +78,7 @@ namespace iso
   is_iso.mk _ ((retraction_eq_section f) ▸ (retraction_comp f)) (comp_section f)
 
   theorem inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' :=
-  inverse_eq_left !left_inverse
+  @inverse_eq_left _ _ _ _ _ _ H !left_inverse
 
   theorem inverse_involutive (f : a ⟶ b) [H : is_iso f] [H : is_iso (f⁻¹)]
     : (f⁻¹)⁻¹ = f :=

hott/algebra/category/precategory.hlean

@@ -30,7 +30,6 @@ namespace category
     (id_id : Π (a : ob), comp !ID !ID = ID a)
     (is_set_hom : Π(a b : ob), is_set (hom a b))
 
-  -- attribute precategory [multiple-instances] --this is not used anywhere
   attribute precategory.is_set_hom [instance]
 
   infixr ∘ := precategory.comp