From aeec8cae851d533b77801700b009fbda8fc26309 Mon Sep 17 00:00:00 2001 From: Ulrik Buchholtz Date: Thu, 8 Sep 2016 15:02:28 -0400 Subject: [PATCH] full_subgroup --- algebra/group_basics.hlean | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/algebra/group_basics.hlean b/algebra/group_basics.hlean index 9b6bcc2..5014ccd 100644 --- a/algebra/group_basics.hlean +++ b/algebra/group_basics.hlean @@ -34,13 +34,13 @@ namespace group definition is_trivial_subgroup (G : Group) (R : subgroup_rel G) : Prop := sorry /- Π g, R g = trivial_subgroup g -/ - definition full_subgroup.{u} (G : Group.{u}) : subgroup_rel.{u u} G := + definition full_subgroup.{u} (G : Group.{u}) : subgroup_rel.{u 0} G := begin fapply subgroup_rel.mk, - { intro g, fapply trunctype.mk, exact g = g, exact _}, -- instead of the unit type, we take g = g, because the unit type is in Type₀ and not in Type.{u} - { esimp }, - { intros g h p q, esimp }, - { intros g p, esimp } + { intro g, fapply trunctype.mk, exact unit, exact _}, -- instead of the unit type, we take g = g, because the unit type is in Type₀ and not in Type.{u} + { esimp, constructor }, + { intros g h p q, esimp, constructor }, + { intros g p, esimp, constructor } end definition is_full_subgroup (G : Group) (R : subgroup_rel G) : Prop := sorry /- Π g, R g -/