From 7bfd897f9d80ea95ad940865ca856abd40004d92 Mon Sep 17 00:00:00 2001
From: Jakob von Raumer <javra@web.de>
Date: Mon, 8 Dec 2014 20:16:02 -0500
Subject: [PATCH] feat(library/hott) add groupoid definition

---
 library/hott/algebra/groupoid.lean | 32 ++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)
 create mode 100644 library/hott/algebra/groupoid.lean

diff --git a/library/hott/algebra/groupoid.lean b/library/hott/algebra/groupoid.lean
new file mode 100644
index 0000000000..a3b81a1c3d
--- /dev/null
+++ b/library/hott/algebra/groupoid.lean
@@ -0,0 +1,32 @@
+-- Copyright (c) 2014 Jakob von Raumer. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Author: Jakob von Raumer
+-- Ported from Coq HoTT
+import .precategory.basic .precategory.morphism
+
+open path function prod sigma truncation morphism nat precategory
+
+structure foo (A : Type) := (bsp : A)
+
+structure groupoid [class] (ob : Type) extends precategory ob :=
+  (all_iso : Π ⦃a b : ob⦄ (f : hom a b),
+    @is_iso ob (precategory.mk hom _ _ _ assoc id_left id_right) a b f)
+
+namespace groupoid
+
+set_option pp.universes true
+universe variable l
+definition path_precategory (A : Type.{l})
+    (H : is_trunc 1 A) : precategory.{l l} A :=
+begin
+  fapply precategory.mk,
+    intros (a, b), exact (a ≈ b),
+    intros, apply succ_is_trunc, exact H,
+    intros (a, b, c, p, q), exact (@concat A a b c q p),
+    intro a, apply idp,
+    intros, apply concat_pp_p,
+    intros, apply concat_p1,
+    intros, apply concat_1p,
+end
+
+end groupoid