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