From d3cba4b95d6ed308be9cee8a02593284f158964b Mon Sep 17 00:00:00 2001
From: Egbert Rijke <e.m.rijke@gmail.com>
Date: Thu, 1 Dec 2016 15:43:05 -0500
Subject: [PATCH] simplifty the trivial subgroup

---
 algebra/subgroup.hlean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/algebra/subgroup.hlean b/algebra/subgroup.hlean
index 08a1a32..c5d1598 100644
--- a/algebra/subgroup.hlean
+++ b/algebra/subgroup.hlean
@@ -34,11 +34,8 @@ namespace group
     { intros g p, esimp at *, rewrite p, exact one_inv }
   end
 
-  definition is_trivial_subgroup (G : Group) (R : subgroup_rel G) : Prop :=
-  trunctype.mk (Π g : G, R g ↔ trivial_subgroup G g)
-  begin
-    apply pi.is_trunc_pi, intro g, apply is_trunc_prod
-  end
+  definition is_trivial_subgroup (G : Group) (R : subgroup_rel G) : Type :=
+  (Π g : G, R g → g = 1)
 
   definition full_subgroup.{u} (G : Group.{u}) : subgroup_rel.{u 0} G :=
   begin