From e2b31a9b331f1bcb113502eaa3c6e0d74ba86b6c Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 2 Mar 2016 16:50:20 -0500
Subject: [PATCH] feat(hott): remove multiple_instances attribute

---
 hott/algebra/category/category.hlean           | 2 --
 hott/algebra/category/functor/attributes.hlean | 4 ++--
 hott/algebra/category/iso.hlean                | 3 +--
 hott/algebra/category/precategory.hlean        | 1 -
 4 files changed, 3 insertions(+), 7 deletions(-)

diff --git a/hott/algebra/category/category.hlean b/hott/algebra/category/category.hlean
index dc0a85f8d4..c40dfb4da3 100644
--- a/hott/algebra/category/category.hlean
+++ b/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]
 
diff --git a/hott/algebra/category/functor/attributes.hlean b/hott/algebra/category/functor/attributes.hlean
index a67b03cbc2..a97ba8b275 100644
--- a/hott/algebra/category/functor/attributes.hlean
+++ b/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') :=
diff --git a/hott/algebra/category/iso.hlean b/hott/algebra/category/iso.hlean
index eb998ec1bf..338a787e76 100644
--- a/hott/algebra/category/iso.hlean
+++ b/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 :=
diff --git a/hott/algebra/category/precategory.hlean b/hott/algebra/category/precategory.hlean
index 19137afde4..007375a08d 100644
--- a/hott/algebra/category/precategory.hlean
+++ b/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