michael/Spectral
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

tiny

Browse source 
tiny
This commit is contained in:
Steve Awodey 2015-12-10 15:41:24 -05:00
parent c1d1a5e509
commit f4a8a679c6
1 changed files with 5 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
group_theory/basic.hlean
View file

@ -21,6 +21,9 @@ namespace group
definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one definition pointed_Group [instance] (G : Group) : pointed G := pointed.mk one
definition Pointed_of_Group (G : Group) : Type* := pointed.mk' G definition Pointed_of_Group (G : Group) : Type* := pointed.mk' G
-- print Type*
-- print Pointed
definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group := definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group :=
Group.mk G _ Group.mk G _
@ -69,6 +72,8 @@ namespace group
definition homomorphism_id [constructor] (G : Group) : G → G := definition homomorphism_id [constructor] (G : Group) : G → G :=
homomorphism.mk id (λg h, idp) homomorphism.mk id (λg h, idp)
-- TODO: maybe define this in more generality for pointed types? -- TODO: maybe define this in more generality for pointed types?
definition kernel [constructor] (φ : G₁ →g G₂) (g : G₁) : hprop := trunctype.mk (φ g = 1) _ definition kernel [constructor] (φ : G₁ →g G₂) (g : G₁) : hprop := trunctype.mk (φ g = 1) _