fix spacing and add comment about universes

Signed-off-by: Ali Caglayan <[email protected]>
HoTT · Jan 21, 2025 · b2c7d9f · b2c7d9f
1 parent a412b5c
commit b2c7d9f
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/theories/Algebra/Groups/QuotientGroup.v b/theories/Algebra/Groups/QuotientGroup.v
@@ -116,6 +116,7 @@ Section Cosets.
 
   Definition LeftCoset := G / in_cosetL H.
 
+  (** TODO: Way too many universes, needs fixing *)
   (** The set of left cosets of a finite subgroup of a finite group is finite. *)
   Global Instance finite_leftcoset `{Univalence, Finite G, Finite H}
     : Finite LeftCoset.
@@ -128,7 +129,7 @@ Section Cosets.
   Defined.
 
   (** The index of a subgroup is the number of possible cosets of the subgroup. *) 
-  Definition subgroup_index `{Univalence, Finite G,  Finite H} : nat
+  Definition subgroup_index `{Univalence, Finite G, Finite H} : nat
     := fcard LeftCoset.
 
   Definition RightCoset := G / in_cosetR H.