Apply suggestions from code review

Added explanatory comments, some stylistic changes (Hom A B -> A $-> B)

Co-authored-by: Dan Christensen <[email protected]>

theories/Algebra/AbGroups/AbHom.v

@@ -40,7 +40,7 @@ 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 : Hom A B)
+Definition ab_coeq {A B : AbGroup} (f g : A $-> B)
   := ab_cokernel ((-f) + g).
 
 Definition ab_coeq_in {A B : AbGroup} {f g : A $-> B} : B $-> ab_coeq f g.

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 : Hom (A:=Group) E F)
+  {E F : AbSES B A} (phi : Hom (A:=AbGroup) 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 : Hom (A:=Group) E F
+  := {phi : Hom (A:=AbGroup) E F
             & (phi $o inclusion _ == inclusion _)
               * (projection _ == projection _ $o phi)}.
 

theories/Algebra/Groups/Group.v

@@ -771,6 +771,7 @@ Defined.
 Global Instance isgraph_group : IsGraph Group
   := Build_IsGraph Group GroupHomomorphism.
 
+(** We add this coercion to make it easier to use a group isomorphism where Coq expects a category morphism. *)
 Definition isHom_GroupIsomorphism (G H : Group) : GroupIsomorphism G H -> Hom G H := idmap.
 Coercion isHom_GroupIsomorphism  : GroupIsomorphism >-> Hom.
 

theories/WildCat/Core.v

@@ -9,6 +9,7 @@ Class IsGraph (A : Type) :=
   Hom : A -> A -> Type
 }.
 
+(** This tells Coq to not perform typeclass search on a goal of the form `IsGraph A` when the head of `A` is an evar, avoiding what is often a search involving all possible graph structures on all types.  With this hint in place, we need to occasionally annotate our terms to explicitly give the underlying type. *) 
 Hint Mode IsGraph ! : typeclass_instances.
 
 Notation "a $-> b" := (Hom a b).