WildCat/ZeroGroupoid: fix typo, graph -> 0gpd

HoTT · Sep 3, 2023 · d7ec40b · d7ec40b
1 parent 977214c
commit d7ec40b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/WildCat/ZeroGroupoid.v b/theories/WildCat/ZeroGroupoid.v
@@ -54,7 +54,7 @@ Proof.
   exact (forall x : G, f x $== g x).
 Defined.
 
-Global Instance is1cat_graph : Is1Cat ZeroGpd.
+Global Instance is1cat_0gpd : Is1Cat ZeroGpd.
 Proof.
   snrapply Build_Is1Cat.
   - intros G H.