diff --git a/contrib/SetoidRewrite.v b/contrib/SetoidRewrite.v
index 83a5352efc6..61e3c2bff87 100644
--- a/contrib/SetoidRewrite.v
+++ b/contrib/SetoidRewrite.v
@@ -121,7 +121,7 @@ Defined.
 
 #[export] Instance gpd_hom_is_proper1 {A : Type} `{Is0Gpd A}
  : CMorphisms.Proper
-     (Hom ==> Hom ==> CRelationClasses.arrow) Hom.
+     (Hom (A:=A)==> Hom ==> CRelationClasses.arrow) Hom.
 Proof.
   intros x y eq_xy a b eq_ab f.
   refine (transitivity _ eq_ab).
diff --git a/theories/Algebra/AbGroups/AbHom.v b/theories/Algebra/AbGroups/AbHom.v
index 4e969b7a558..972cc24eca0 100644
--- a/theories/Algebra/AbGroups/AbHom.v
+++ b/theories/Algebra/AbGroups/AbHom.v
@@ -40,10 +40,10 @@ Defined.
 (** ** Coequalizers *)
 
 (** Using the cokernel and addition and negation for the homs of abelian groups, we can define the coequalizer of two group homomorphisms as the cokernel of their difference. *)
-Definition ab_coeq {A B : AbGroup} (f g : GroupHomomorphism A B)
+Definition ab_coeq {A B : AbGroup} (f g : Hom A B)
   := ab_cokernel ((-f) + g).
 
-Definition ab_coeq_in {A B} {f g : A $-> B} : B $-> ab_coeq f g.
+Definition ab_coeq_in {A B : AbGroup} {f g : A $-> B} : B $-> ab_coeq f g.
 Proof.
   snrapply grp_quotient_map.
 Defined.
@@ -97,7 +97,7 @@ Proof.
   exact p.
 Defined.
 
-Definition functor_ab_coeq {A B} {f g : A $-> B} {A' B'} {f' g' : A' $-> B'}
+Definition functor_ab_coeq {A B : AbGroup} {f g : A $-> B} {A' B'} {f' g' : A' $-> B'}
   (a : A $-> A') (b : B $-> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
   : ab_coeq f g $-> ab_coeq f' g'.
 Proof.
@@ -109,7 +109,7 @@ Proof.
   nrapply ab_coeq_glue.
 Defined.
 
-Definition functor2_ab_coeq {A B} {f g : A $-> B} {A' B'} {f' g' : A' $-> B'}
+Definition functor2_ab_coeq {A B : AbGroup} {f g : A $-> B} {A' B'} {f' g' : A' $-> B'}
   {a a' : A $-> A'} {b b' : B $-> B'}
   (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
   (p' : f' $o a' $== b' $o f) (q' : g' $o a' $== b' $o g)
@@ -121,7 +121,7 @@ Proof.
   exact (ap ab_coeq_in (s x)).
 Defined.
 
-Definition functor_ab_coeq_compose {A B} {f g : A $-> B}
+Definition functor_ab_coeq_compose {A B : AbGroup} {f g : A $-> B}
   {A' B'} {f' g' : A' $-> B'} 
   (a : A $-> A') (b : B $-> B') (p : f' $o a $== b $o f) (q : g' $o a $== b $o g)
   {A'' B''} {f'' g'' : A'' $-> B''}
@@ -206,10 +206,7 @@ Proof.
 Defined.
 
 Global Instance is0bifunctor_ab_hom `{Funext}
-  : Is0Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
-Proof.
-  rapply Build_Is0Bifunctor''.
-Defined.
+  : Is0Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup) := Build_Is0Bifunctor'' _.
 
 Global Instance is1bifunctor_ab_hom `{Funext}
   : Is1Bifunctor (ab_hom : Group^op -> AbGroup -> AbGroup).
diff --git a/theories/Algebra/AbSES/BaerSum.v b/theories/Algebra/AbSES/BaerSum.v
index e804c762aca..c110706fa64 100644
--- a/theories/Algebra/AbSES/BaerSum.v
+++ b/theories/Algebra/AbSES/BaerSum.v
@@ -52,10 +52,7 @@ Proof.
 Defined.
 
 Global Instance is0bifunctor_abses' `{Univalence}
-  : Is0Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
-Proof.
-  rapply Build_Is0Bifunctor''.
-Defined.
+  : Is0Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type) := Build_Is0Bifunctor'' _.
 
 Global Instance is1bifunctor_abses' `{Univalence}
   : Is1Bifunctor (AbSES' : AbGroup^op -> AbGroup -> Type).
@@ -230,10 +227,7 @@ Proof.
 Defined.
 
 Global Instance is0bifunctor_abses `{Univalence}
-  : Is0Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
-Proof.
-  rapply Build_Is0Bifunctor''.
-Defined.
+  : Is0Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType) := Build_Is0Bifunctor'' _.
 
 Global Instance is1bifunctor_abses `{Univalence}
   : Is1Bifunctor (AbSES : AbGroup^op -> AbGroup -> pType).
diff --git a/theories/Algebra/AbSES/Core.v b/theories/Algebra/AbSES/Core.v
index 1e232084c2b..f16945c633c 100644
--- a/theories/Algebra/AbSES/Core.v
+++ b/theories/Algebra/AbSES/Core.v
@@ -147,7 +147,7 @@ Definition path_abses_iso `{Univalence} {B A : AbGroup@{u}}
 
 (** A special case of the "short 5-lemma" where the two outer maps are (definitionally) identities. *)
 Lemma short_five_lemma {B A : AbGroup@{u}}
-  {E F : AbSES B A} (phi : GroupHomomorphism E F)
+  {E F : AbSES B A} (phi : Hom (A:=Group) E F)
   (p0 : phi $o inclusion E == inclusion F) (p1 : projection E == projection F $o phi)
   : IsEquiv phi.
 Proof.
@@ -185,7 +185,7 @@ Defined.
 
 (** Below we prove that homomorphisms respecting [projection] and [inclusion] correspond to paths in [AbSES B A]. We refer to such homomorphisms simply as path data in [AbSES B A]. *)
 Definition abses_path_data {B A : AbGroup@{u}} (E F : AbSES B A)
-  := {phi : GroupHomomorphism E F
+  := {phi : Hom (A:=Group) E F
             & (phi $o inclusion _ == inclusion _)
               * (projection _ == projection _ $o phi)}.
 
diff --git a/theories/Algebra/AbSES/Ext.v b/theories/Algebra/AbSES/Ext.v
index 4193d16a0e6..63ce0a1465e 100644
--- a/theories/Algebra/AbSES/Ext.v
+++ b/theories/Algebra/AbSES/Ext.v
@@ -119,10 +119,7 @@ Proof.
 Defined.
 
 Global Instance is0bifunctor_abext `{Univalence}
-  : Is0Bifunctor (A:=AbGroup^op) ab_ext.
-Proof.
-  rapply Build_Is0Bifunctor''.
-Defined.
+  : Is0Bifunctor (A:=AbGroup^op) ab_ext := Build_Is0Bifunctor'' _.
 
 Global Instance is1bifunctor_abext `{Univalence}
   : Is1Bifunctor (A:=AbGroup^op) ab_ext.
diff --git a/theories/Algebra/Categorical/MonoidObject.v b/theories/Algebra/Categorical/MonoidObject.v
index 06d29d6a12f..f7a9080e761 100644
--- a/theories/Algebra/Categorical/MonoidObject.v
+++ b/theories/Algebra/Categorical/MonoidObject.v
@@ -205,7 +205,7 @@ Defined.
 Section MonoidEnriched.
   Context {A : Type} `{HasEquivs A} `{!HasBinaryProducts A}
     (unit : A) `{!IsTerminal unit} {x y : A}
-    `{!HasMorExt A} `{forall x y, IsHSet (x $-> y)}.
+    `{!HasMorExt A} `{forall x y : A, IsHSet (x $-> y)}.
 
   Section Monoid.
     Context `{!IsMonoidObject _ _ y}.
diff --git a/theories/Algebra/Groups/Group.v b/theories/Algebra/Groups/Group.v
index 452fd9e87ae..6658db297ac 100644
--- a/theories/Algebra/Groups/Group.v
+++ b/theories/Algebra/Groups/Group.v
@@ -771,6 +771,9 @@ Defined.
 Global Instance isgraph_group : IsGraph Group
   := Build_IsGraph Group GroupHomomorphism.
 
+Definition isHom_GroupIsomorphism (G H : Group) : GroupIsomorphism G H -> Hom G H := idmap.
+Coercion isHom_GroupIsomorphism  : GroupIsomorphism >-> Hom.
+
 Global Instance is01cat_group : Is01Cat Group :=
   Build_Is01Cat Group _ (@grp_homo_id) (@grp_homo_compose).
 
diff --git a/theories/Algebra/Rings/Module.v b/theories/Algebra/Rings/Module.v
index 13a6c88849b..68ffe6f61be 100644
--- a/theories/Algebra/Rings/Module.v
+++ b/theories/Algebra/Rings/Module.v
@@ -419,7 +419,7 @@ Global Instance isgraph_leftmodule {R : Ring} : IsGraph (LeftModule R)
   := Build_IsGraph _ LeftModuleHomomorphism.
 
 Global Instance is01cat_leftmodule {R : Ring} : Is01Cat (LeftModule R)
-  := Build_Is01Cat _ _ lm_homo_id (@lm_homo_compose R).
+  := Build_Is01Cat (LeftModule R) _ lm_homo_id (@lm_homo_compose R).
 
 Global Instance is2graph_leftmodule {R : Ring} : Is2Graph (LeftModule R)
   := fun M N => isgraph_induced (@lm_homo_map R M N).
diff --git a/theories/Algebra/Rings/Ring.v b/theories/Algebra/Rings/Ring.v
index d1746a20d0e..7989d6e37c3 100644
--- a/theories/Algebra/Rings/Ring.v
+++ b/theories/Algebra/Rings/Ring.v
@@ -261,7 +261,7 @@ Global Instance isgraph_ring : IsGraph Ring
   := Build_IsGraph _ RingHomomorphism.
 
 Global Instance is01cat_ring : Is01Cat Ring
-  := Build_Is01Cat _ _ rng_homo_id (@rng_homo_compose).
+  := Build_Is01Cat Ring _ rng_homo_id (@rng_homo_compose).
 
 Global Instance is2graph_ring : Is2Graph Ring
   := fun A B => isgraph_induced (@rng_homo_map A B : _ -> (group_type _ $-> _)).
diff --git a/theories/Algebra/ooGroup.v b/theories/Algebra/ooGroup.v
index 6192c216a78..ced4b9dd4f2 100644
--- a/theories/Algebra/ooGroup.v
+++ b/theories/Algebra/ooGroup.v
@@ -270,7 +270,7 @@ End Subgroups.
 Global Instance isgraph_oogroup : IsGraph ooGroup
   := Build_IsGraph _ ooGroupHom.
 Global Instance is01cat_oogroup : Is01Cat ooGroup
-  := Build_Is01Cat _ _ grouphom_idmap (@grouphom_compose).
+  := Build_Is01Cat ooGroup _ grouphom_idmap (@grouphom_compose).
 Global Instance is2graph_oogroup : Is2Graph ooGroup
   := is2graph_induced classifying_space.
 Global Instance is1cat_oogroup : Is1Cat ooGroup
diff --git a/theories/WildCat/Core.v b/theories/WildCat/Core.v
index 0b4f65d99a5..762849d6c06 100644
--- a/theories/WildCat/Core.v
+++ b/theories/WildCat/Core.v
@@ -9,6 +9,8 @@ Class IsGraph (A : Type) :=
   Hom : A -> A -> Type
 }.
 
+Hint Mode IsGraph ! : typeclass_instances.
+
 Notation "a $-> b" := (Hom a b).
 
 Definition graph_hfiber {B C : Type} `{IsGraph C} (F : B -> C) (c : C)
@@ -46,7 +48,7 @@ Global Instance reflexive_GpdHom {A} `{Is0Gpd A}
   := fun a => Id a.
 
 Global Instance reflexive_Hom {A} `{Is01Cat A}
-  : Reflexive Hom
+  : Reflexive Hom (A:=A)
   := fun a => Id a.
 
 Definition gpd_comp {A} `{Is0Gpd A} {a b c : A}
@@ -55,21 +57,21 @@ Definition gpd_comp {A} `{Is0Gpd A} {a b c : A}
 Infix "$@" := gpd_comp.
 
 Global Instance transitive_GpdHom {A} `{Is0Gpd A}
-  : Transitive GpdHom
+  : Transitive GpdHom (A:=A)
   := fun a b c f g => f $@ g.
 
 Global Instance transitive_Hom {A} `{Is01Cat A}
-  : Transitive Hom
+  : Transitive Hom (A:=A)
   := fun a b c f g => g $o f.
 
 Notation "p ^$" := (gpd_rev p).
 
 Global Instance symmetric_GpdHom {A} `{Is0Gpd A}
-  : Symmetric GpdHom
+  : Symmetric GpdHom (A:=A)
   := fun a b f => f^$.
 
 Global Instance symmetric_GpdHom' {A} `{Is0Gpd A}
-  : Symmetric Hom
+  : Symmetric Hom (A:=A)
   := fun a b f => f^$.
 
 Definition Hom_path {A : Type} `{Is01Cat A} {a b : A} (p : a = b) : (a $-> b).
@@ -296,7 +298,7 @@ Class Faithful {A B : Type} (F : A -> B) `{Is1Functor A B F} :=
 
 Section IdentityFunctor.
 
-  Global Instance is0functor_idmap {A : Type} `{IsGraph A} : Is0Functor idmap.
+  Global Instance is0functor_idmap {A : Type} `{IsGraph A} : Is0Functor (A:=A) idmap.
   Proof.
     by apply Build_Is0Functor.
   Defined.
diff --git a/theories/WildCat/Paths.v b/theories/WildCat/Paths.v
index 882c5a3fb95..fa03510b3ab 100644
--- a/theories/WildCat/Paths.v
+++ b/theories/WildCat/Paths.v
@@ -24,7 +24,7 @@ Local Existing Instances isgraph_paths is2graph_paths is3graph_paths | 10.
 
 (** Any type has composition and identity morphisms given by path concatenation and reflexivity. *)
 Global Instance is01cat_paths (A : Type) : Is01Cat A
-  := {| Id := @idpath _ ; cat_comp := fun _ _ _ x y => concat y x |}.
+  := { Id := @idpath _ ; cat_comp := fun _ _ _ x y => concat y x }.
 
 (** Any type has a 0-groupoid structure with inverse morphisms given by path inversion. *)
 Global Instance is0gpd_paths (A : Type) : Is0Gpd A