From 7083f2fccdbc5e379f8606bf3137cafd00bcb7a3 Mon Sep 17 00:00:00 2001 From: Jakob von Raumer Date: Fri, 13 Mar 2015 18:33:53 -0400 Subject: [PATCH] fix(hott/algebra) correct the name of a groupoid constructor --- hott/algebra/groupoid.hlean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/hott/algebra/groupoid.hlean b/hott/algebra/groupoid.hlean index daa492366..591c9b7b4 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)