diff --git a/hott/algebra/groupoid.hlean b/hott/algebra/groupoid.hlean
index eb4260d23e..daa492366d 100644
--- a/hott/algebra/groupoid.hlean
+++ b/hott/algebra/groupoid.hlean
@@ -18,7 +18,7 @@ namespace category
    (all_iso : Π ⦃a b : ob⦄ (f : hom a b), @is_iso ob parent a b f)
 
   abbreviation all_iso := @groupoid.all_iso
-  attribute groupoid.all_iso [instance]
+  attribute groupoid.all_iso [instance] [priority 100000]
 
   definition groupoid.mk' [reducible] (ob : Type) (C : precategory ob)
     (H : Π (a b : ob) (f : a ⟶ b), is_iso f) : groupoid ob :=
diff --git a/hott/algebra/precategory/iso.hlean b/hott/algebra/precategory/iso.hlean
index fb9fde881f..dbfa64e926 100644
--- a/hott/algebra/precategory/iso.hlean
+++ b/hott/algebra/precategory/iso.hlean
@@ -35,7 +35,7 @@ namespace iso
   definition right_inverse [reducible] := @is_iso.right_inverse
   postfix `⁻¹` := inverse
   --a second notation for the inverse, which is not overloaded
-  postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse
+  postfix [parsing-only] `⁻¹ʰ`:std.prec.max_plus := inverse -- input using \-1h
 
   variables {ob : Type} [C : precategory ob]
   variables {a b c : ob} {g : b ⟶ c} {f : a ⟶ b} {h : b ⟶ a}
@@ -82,7 +82,8 @@ namespace iso
   definition inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' :=
   inverse_eq_left !left_inverse
 
-  definition inverse_involutive (f : a ⟶ b) [H : is_iso f] : (f⁻¹)⁻¹ = f :=
+  definition inverse_involutive (f : a ⟶ b) [H : is_iso f] [H : is_iso (f⁻¹)]
+    : (f⁻¹)⁻¹ = f :=
   inverse_eq_right !left_inverse
 
   definition retraction_id (a : ob) : retraction_of (ID a) = id :=