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

fix(algebra): change the reducibility of some defintions

Browse source
This commit is contained in:
Floris van Doorn 2016-09-18 00:14:19 -04:00
parent 11c08c51e6
commit e2734080c6
2 changed files with 23 additions and 24 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

38
hott/algebra/bundled.hlean
View file

@ -37,20 +37,18 @@ abbreviation signature := interval
structure Group (i : signature) :=
(carrier : Type) (struct : group carrier)
definition MulGroup [reducible] : Type := Group interval.zero
definition AddGroup [reducible] : Type := Group interval.one
definition MulGroup : Type := Group interval.zero
definition AddGroup : Type := Group interval.one
attribute Group.carrier [coercion]
definition MulGroup.mk [constructor] (G : Type) (H : group G) : MulGroup := Group.mk _ G _
definition AddGroup.mk [constructor] (G : Type) (H : add_group G) : AddGroup :=
definition MulGroup.mk [constructor] [reducible] (G : Type) (H : group G) : MulGroup :=
Group.mk _ G _
definition AddGroup.mk [constructor] [reducible] (G : Type) (H : add_group G) : AddGroup :=
Group.mk _ G add_group.to_group
section
local attribute group.to_add_group Group.struct [instance]
definition MulGroup.struct (G : MulGroup) : group G := _
definition AddGroup.struct (G : AddGroup) : add_group G := _
end
definition MulGroup.struct [reducible] (G : MulGroup) : group G := Group.struct G
definition AddGroup.struct [reducible] (G : AddGroup) : add_group G :=
@group.to_add_group _ (Group.struct G)
attribute MulGroup.struct AddGroup.struct [instance] [priority 2000]
attribute Group.struct [instance] [priority 800]
@ -58,27 +56,23 @@ attribute Group.struct [instance] [priority 800]
structure CommGroup (i : signature) :=
(carrier : Type) (struct : comm_group carrier)
definition MulCommGroup [reducible] : Type := CommGroup interval.zero
definition AddCommGroup [reducible] : Type := CommGroup interval.one
definition MulCommGroup : Type := CommGroup interval.zero
definition AddCommGroup : Type := CommGroup interval.one
attribute CommGroup.carrier [coercion]
definition MulCommGroup.mk [constructor] (G : Type) (H : comm_group G) : MulCommGroup :=
definition MulCommGroup.mk [constructor] [reducible] (G : Type) (H : comm_group G) : MulCommGroup :=
CommGroup.mk _ G _
definition AddCommGroup.mk [constructor] (G : Type) (H : add_comm_group G) : AddCommGroup :=
definition AddCommGroup.mk [constructor] [reducible] (G : Type) (H : add_comm_group G) :
AddCommGroup :=
CommGroup.mk _ G add_comm_group.to_comm_group
section
local attribute comm_group.to_add_comm_group CommGroup.struct [instance]
definition MulCommGroup.struct (G : MulCommGroup) : comm_group G := _
definition AddCommGroup.struct (G : AddCommGroup) : add_comm_group G := _
end
definition MulCommGroup.struct [reducible] (G : MulCommGroup) : comm_group G := CommGroup.struct G
definition AddCommGroup.struct [reducible] (G : AddCommGroup) : add_comm_group G :=
@comm_group.to_add_comm_group _ (CommGroup.struct G)
attribute MulCommGroup.struct AddCommGroup.struct [instance] [priority 2000]
attribute CommGroup.struct [instance] [priority 800]
-- structure AddSemigroup :=
-- (carrier : Type) (struct : add_semigroup carrier)

9
hott/types/int/hott.hlean
View file

@ -14,12 +14,17 @@ namespace int
section
open algebra
definition group_integers [constructor] : AddGroup :=
/-
we make these structures reducible, so that n * m in gℤ and agℤ can be interpreted as
multiplication on ℤ. For this it's needed that the carriers of gℤ and agℤ reduce to ℤ unfolding
only reducible definitions.
-/
definition group_integers [reducible] [constructor] : AddGroup :=
AddGroup.mk ℤ _
notation `gℤ` := group_integers
definition CommGroup_int [constructor] : AddCommGroup :=
definition CommGroup_int [reducible] [constructor] : AddCommGroup :=
AddCommGroup.mk ℤ _
notation `agℤ` := CommGroup_int