From f4a8a679c60b23efc671ab5366902a4724317697 Mon Sep 17 00:00:00 2001 From: Steve Awodey Date: Thu, 10 Dec 2015 15:41:24 -0500 Subject: [PATCH] tiny tiny --- group_theory/basic.hlean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/group_theory/basic.hlean b/group_theory/basic.hlean index 1419ba1..9da1d98 100644 --- a/group_theory/basic.hlean +++ b/group_theory/basic.hlean @@ -21,6 +21,9 @@ namespace group definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one definition Pointed_of_Group (G : Group) : Type* := pointed.mk' G + -- print Type* + -- print Pointed + definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group := Group.mk G _ @@ -69,6 +72,8 @@ namespace group definition homomorphism_id [constructor] (G : Group) : G → G := homomorphism.mk id (λg h, idp) + + -- TODO: maybe define this in more generality for pointed types? definition kernel [constructor] (φ : G₁ →g G₂) (g : G₁) : hprop := trunctype.mk (φ g = 1) _