diff --git a/hott/algebra/groupoid.hlean b/hott/algebra/groupoid.hlean
index daa492366d..591c9b7b41 100644
--- a/hott/algebra/groupoid.hlean
+++ b/hott/algebra/groupoid.hlean
@@ -109,7 +109,7 @@ namespace category
   Precategory.mk (Groupoid.carrier C) C
 
   definition groupoid.Mk [reducible] := Groupoid.mk
-  definition category.MK [reducible] (C : Precategory) (H : Π (a b : C) (f : a ⟶ b), is_iso f)
+  definition groupoid.MK [reducible] (C : Precategory) (H : Π (a b : C) (f : a ⟶ b), is_iso f)
     : Groupoid :=
   Groupoid.mk C (groupoid.mk' C C H)