feat(hott/algebra/bundled): add a parameter to Group to specify whether it's an additive or multiplicative group

hott/algebra/bundled.hlean

@@ -5,7 +5,7 @@ Authors: Jeremy Avigad
 
 Bundled structures
 -/
-import algebra.group
+import algebra.group homotopy.interval
 open algebra
 
 namespace algebra
@@ -33,51 +33,85 @@ structure CommMonoid :=
 attribute CommMonoid.carrier [coercion]
 attribute CommMonoid.struct [instance]
 
-structure Group :=
+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
 attribute Group.carrier [coercion]
-attribute Group.struct [instance]
 
-structure CommGroup :=
+definition MulGroup.mk [constructor] (G : Type) (H : group G) : MulGroup := Group.mk _ G _
+definition AddGroup.mk [constructor] (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
+
+attribute MulGroup.struct AddGroup.struct [instance] [priority 2000]
+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
 attribute CommGroup.carrier [coercion]
-attribute CommGroup.struct [instance]
 
-structure AddSemigroup :=
+definition MulCommGroup.mk [constructor] (G : Type) (H : comm_group G) : MulCommGroup :=
-(carrier : Type) (struct : add_semigroup carrier)
+CommGroup.mk _ G _
+definition AddCommGroup.mk [constructor] (G : Type) (H : add_comm_group G) : AddCommGroup :=
+CommGroup.mk _ G add_comm_group.to_comm_group
 
-attribute AddSemigroup.carrier [coercion]
+section
-attribute AddSemigroup.struct [instance]
+local attribute comm_group.to_add_comm_group CommGroup.struct [instance]
 
-structure AddCommSemigroup :=
+definition MulCommGroup.struct (G : MulCommGroup) : comm_group G := _
-(carrier : Type) (struct : add_comm_semigroup carrier)
+definition AddCommGroup.struct (G : AddCommGroup) : add_comm_group G := _
+end
 
-attribute AddCommSemigroup.carrier [coercion]
+attribute MulCommGroup.struct AddCommGroup.struct [instance] [priority 2000]
-attribute AddCommSemigroup.struct [instance]
+attribute CommGroup.struct [instance] [priority 800]
 
-structure AddMonoid :=
-(carrier : Type) (struct : add_monoid carrier)
 
-attribute AddMonoid.carrier [coercion]
-attribute AddMonoid.struct [instance]
 
-structure AddCommMonoid :=
+-- structure AddSemigroup :=
-(carrier : Type) (struct : add_comm_monoid carrier)
+-- (carrier : Type) (struct : add_semigroup carrier)
 
-attribute AddCommMonoid.carrier [coercion]
+-- attribute AddSemigroup.carrier [coercion]
-attribute AddCommMonoid.struct [instance]
+-- attribute AddSemigroup.struct [instance]
 
-structure AddGroup :=
+-- structure AddCommSemigroup :=
-(carrier : Type) (struct : add_group carrier)
+-- (carrier : Type) (struct : add_comm_semigroup carrier)
 
-attribute AddGroup.carrier [coercion]
+-- attribute AddCommSemigroup.carrier [coercion]
-attribute AddGroup.struct [instance]
+-- attribute AddCommSemigroup.struct [instance]
 
-structure AddCommGroup :=
+-- structure AddMonoid :=
-(carrier : Type) (struct : add_comm_group carrier)
+-- (carrier : Type) (struct : add_monoid carrier)
 
-attribute AddCommGroup.carrier [coercion]
+-- attribute AddMonoid.carrier [coercion]
-attribute AddCommGroup.struct [instance]
+-- attribute AddMonoid.struct [instance]
+
+-- structure AddCommMonoid :=
+-- (carrier : Type) (struct : add_comm_monoid carrier)
+
+-- attribute AddCommMonoid.carrier [coercion]
+-- attribute AddCommMonoid.struct [instance]
+
+-- structure AddGroup :=
+-- (carrier : Type) (struct : add_group carrier)
+
+-- attribute AddGroup.carrier [coercion]
+-- attribute AddGroup.struct [instance]
+
+-- structure AddCommGroup :=
+-- (carrier : Type) (struct : add_comm_group carrier)
+
+-- attribute AddCommGroup.carrier [coercion]
+-- attribute AddCommGroup.struct [instance]
 end algebra

hott/algebra/category/functor/attributes.hlean

@@ -21,6 +21,9 @@ namespace category
   definition split_essentially_surjective [class] (F : C ⇒ D) := Π(d : D), Σ(c : C), F c ≅ d
   definition essentially_surjective [class] (F : C ⇒ D) := Π(d : D), ∃(c : C), F c ≅ d
 
+  definition is_weak_equivalence [class] (F : C ⇒ D) :=
+  fully_faithful F × essentially_surjective F
+
   definition is_equiv_of_fully_faithful [instance] (F : C ⇒ D)
     [H : fully_faithful F] (c c' : C) : is_equiv (@(to_fun_hom F) c c') :=
   !H

hott/algebra/category/functor/equivalence.hlean

@@ -18,9 +18,6 @@ namespace category
     (is_iso_unit : is_iso η)
     (is_iso_counit : is_iso ε)
 
-  definition is_weak_equivalence [class] (F : C ⇒ D) :=
-  fully_faithful F × essentially_surjective F
-
   abbreviation inverse := @is_equivalence.G
   postfix ⁻¹ := inverse
   --a second notation for the inverse, which is not overloaded (there is no unicode superscript F)

hott/algebra/category/groupoid.hlean

@@ -79,7 +79,7 @@ namespace category
   definition Groupoid.eta [unfold 1] (C : Groupoid) : Groupoid.mk C C = C :=
   Groupoid.rec (λob c, idp) C
 
-  definition Groupoid_of_Group [constructor] (G : Group) : Groupoid :=
+  definition Groupoid_of_Group [constructor] {i : signature} (G : Group i) : Groupoid :=
   Groupoid.mk unit (groupoid_of_group G)
 
 end category

hott/algebra/group.hlean

@@ -137,6 +137,22 @@ definition add_comm_monoid.to_comm_monoid {A : Type} [s : add_comm_monoid A] : c
   mul_comm    := add_comm_monoid.add_comm
 ⦄
 
+definition monoid.to_add_monoid {A : Type} [s : monoid A] : add_monoid A :=
+⦃ add_monoid,
+  add         := monoid.mul,
+  add_assoc   := monoid.mul_assoc,
+  zero        := monoid.one A,
+  add_zero    := monoid.mul_one,
+  zero_add    := monoid.one_mul,
+  is_set_carrier := _
+⦄
+
+definition comm_monoid.to_add_comm_monoid {A : Type} [s : comm_monoid A] : add_comm_monoid A :=
+⦃ add_comm_monoid,
+  monoid.to_add_monoid,
+  add_comm    := comm_monoid.mul_comm
+⦄
+
 section add_comm_monoid
   variables [s : add_comm_monoid A]
   include s
@@ -337,6 +353,9 @@ definition add_group.to_group {A : Type} [s : add_group A] : group A :=
 ⦃ group, add_monoid.to_monoid,
   mul_left_inv := add_group.add_left_inv ⦄
 
+definition group.to_add_group {A : Type} [s : group A] : add_group A :=
+⦃ add_group, monoid.to_add_monoid,
+  add_left_inv := group.mul_left_inv ⦄
 
 section add_group
 
@@ -528,6 +547,14 @@ end add_group
 
 structure add_comm_group [class] (A : Type) extends add_group A, add_comm_monoid A
 
+definition add_comm_group.to_comm_group {A : Type} [s : add_comm_group A] : comm_group A :=
+⦃ comm_group, add_group.to_group,
+  mul_comm := add_comm_group.add_comm ⦄
+
+definition comm_group.to_add_comm_group {A : Type} [s : comm_group A] : add_comm_group A :=
+⦃ add_comm_group, group.to_add_group,
+  add_comm := comm_group.mul_comm ⦄
+
 section add_comm_group
   variable [s : add_comm_group A]
   include s

hott/algebra/group_theory.hlean

@@ -15,19 +15,22 @@ open eq algebra pointed function is_trunc pi category equiv is_equiv
 set_option class.force_new true
 
 namespace group
+  definition pointed_Group [instance] [constructor] {i : signature} (G : Group i) : pointed G :=
+  pointed.mk 1
+  definition pType_of_Group [constructor] [reducible] {i : signature} (G : Group i) : Type* :=
+  pointed.MK G 1
+  definition Set_of_Group [constructor] {i : signature} (G : Group i) : Set := trunctype.mk G _
 
-  definition pointed_Group [instance] [constructor] (G : Group) : pointed G := pointed.mk 1
+  definition Group_of_CommGroup [coercion] [constructor] {i : signature} (G : CommGroup i) :
-  definition pType_of_Group [constructor] [reducible] (G : Group) : Type* := pointed.MK G 1
+    Group i :=
-  definition Set_of_Group [constructor] (G : Group) : Set := trunctype.mk G _
+  Group.mk i G _
 
-  definition Group_of_CommGroup [coercion] [constructor] (G : CommGroup) : Group :=
+  definition comm_group_Group_of_CommGroup [instance] [constructor] {i : signature} (G : CommGroup i)
-  Group.mk G _
-
-  definition comm_group_Group_of_CommGroup [instance] [constructor] (G : CommGroup)
     : comm_group (Group_of_CommGroup G) :=
   begin esimp, exact _ end
 
-  definition group_pType_of_Group [instance] (G : Group) : group (pType_of_Group G) :=
+  definition group_pType_of_Group [instance] {i : signature} (G : Group i) :
+    group (pType_of_Group G) :=
   Group.struct G
 
   /- group homomorphisms -/
@@ -74,18 +77,20 @@ namespace group
 
   end
 
-  structure homomorphism (G₁ G₂ : Group) : Type :=
+  structure homomorphism {i j : signature} (G₁ : Group i) (G₂ : Group j) : Type :=
     (φ : G₁ → G₂)
     (p : is_homomorphism φ)
 
   infix ` →g `:55 := homomorphism
 
-  definition group_fun [unfold 3] [coercion] := @homomorphism.φ
+  definition group_fun [unfold 5] [coercion] := @homomorphism.φ
-  definition homomorphism.struct [instance] [priority 2000] {G₁ G₂ : Group} (φ : G₁ →g G₂)
+  definition homomorphism.struct [instance] [priority 2000] {i j : signature}
+    {G₁ : Group i} {G₂ : Group j} (φ : G₁ →g G₂)
     : is_homomorphism φ :=
   homomorphism.p φ
 
-  variables {G G₁ G₂ G₃ : Group} {g h : G₁} {ψ : G₂ →g G₃} {φ₁ φ₂ : G₁ →g G₂} (φ : G₁ →g G₂)
+  variables {i j k l : signature} {G : Group i} {G₁ : Group j} {G₂ : Group k} {G₃ : Group l}
+    {g h : G₁} {ψ : G₂ →g G₃} {φ₁ φ₂ : G₁ →g G₂} (φ : G₁ →g G₂)
 
   definition to_respect_mul /- φ -/ (g h : G₁) : φ (g * h) = φ g * φ h :=
   respect_mul φ g h
@@ -99,7 +104,8 @@ namespace group
   definition to_is_embedding_homomorphism /- φ -/ (H : Π{g}, φ g = 1 → g = 1) : is_embedding φ :=
   is_embedding_homomorphism φ @H
 
-  definition is_set_homomorphism [instance] (G₁ G₂ : Group) : is_set (G₁ →g G₂) :=
+  variables (G₁ G₂)
+  definition is_set_homomorphism [instance] : is_set (G₁ →g G₂) :=
   begin
     have H : G₁ →g G₂ ≃ Σ(f : G₁ → G₂), Π(g₁ g₂ : G₁), f (g₁ * g₂) = f g₁ * f g₂,
     begin
@@ -112,6 +118,7 @@ namespace group
     apply is_trunc_equiv_closed_rev, exact H
   end
 
+  variables {G₁ G₂}
   definition pmap_of_homomorphism [constructor] /- φ -/ : pType_of_Group G₁ →* pType_of_Group G₂ :=
   pmap.mk φ begin esimp, exact respect_one φ end
 
@@ -126,13 +133,15 @@ namespace group
   definition homomorphism_compose [constructor] [trans] (ψ : G₂ →g G₃) (φ : G₁ →g G₂) : G₁ →g G₃ :=
   homomorphism.mk (ψ ∘ φ) (is_homomorphism_compose _ _)
 
-  definition homomorphism_id [constructor] [refl] (G : Group) : G →g G :=
+  variable (G)
+  definition homomorphism_id [constructor] [refl] : G →g G :=
   homomorphism.mk (@id G) (is_homomorphism_id G)
+  variable {G}
 
   infixr ` ∘g `:75 := homomorphism_compose
   notation 1       := homomorphism_id _
 
-  structure isomorphism (A B : Group) :=
+  structure isomorphism {i j : signature} (A : Group i) (B : Group j) :=
     (to_hom : A →g B)
     (is_equiv_to_hom : is_equiv to_hom)
 
@@ -151,10 +160,10 @@ namespace group
     (p : Πg₁ g₂, φ (g₁ * g₂) = φ g₁ * φ g₂) : G₁ ≃g G₂ :=
   isomorphism.mk (homomorphism.mk φ p) !to_is_equiv
 
-  definition eq_of_isomorphism {G₁ G₂ : Group} (φ : G₁ ≃g G₂) : G₁ = G₂ :=
+  definition eq_of_isomorphism {G₁ G₂ : Group i} (φ : G₁ ≃g G₂) : G₁ = G₂ :=
   Group_eq (equiv_of_isomorphism φ) (respect_mul φ)
 
-  definition isomorphism_of_eq {G₁ G₂ : Group} (φ : G₁ = G₂) : G₁ ≃g G₂ :=
+  definition isomorphism_of_eq {G₁ G₂ : Group i} (φ : G₁ = G₂) : G₁ ≃g G₂ :=
   isomorphism_of_equiv (equiv_of_eq (ap Group.carrier φ))
     begin intros, induction φ, reflexivity end
 
@@ -165,8 +174,10 @@ namespace group
     rewrite [respect_mul φ, +right_inv φ]
     end end
 
-  definition isomorphism.refl [refl] [constructor] (G : Group) : G ≃g G :=
+  variable (G)
+  definition isomorphism.refl [refl] [constructor] : G ≃g G :=
   isomorphism.mk 1 !is_equiv_id
+  variable {G}
 
   definition isomorphism.symm [symm] [constructor] (φ : G₁ ≃g G₂) : G₂ ≃g G₁ :=
   isomorphism.mk (to_ginv φ) !is_equiv_inv
@@ -175,11 +186,11 @@ namespace group
   isomorphism.mk (ψ ∘g φ) !is_equiv_compose
 
   definition isomorphism.eq_trans [trans] [constructor]
-     {G₁ G₂ G₃ : Group} (φ : G₁ = G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ :=
+     {G₁ G₂ : Group i} {G₃ : Group j} (φ : G₁ = G₂) (ψ : G₂ ≃g G₃) : G₁ ≃g G₃ :=
   proof isomorphism.trans (isomorphism_of_eq φ) ψ qed
 
   definition isomorphism.trans_eq [trans] [constructor]
-    {G₁ G₂ G₃ : Group} (φ : G₁ ≃g G₂) (ψ : G₂ = G₃) : G₁ ≃g G₃ :=
+    {G₁ : Group i} {G₂ G₃ : Group j} (φ : G₁ ≃g G₂) (ψ : G₂ = G₃) : G₁ ≃g G₃ :=
   isomorphism.trans φ (isomorphism_of_eq ψ)
 
   postfix `⁻¹ᵍ`:(max + 1) := isomorphism.symm
@@ -199,10 +210,10 @@ namespace group
 
   /- category of groups -/
 
-  definition precategory_group [constructor] : precategory Group :=
+  definition precategory_group [constructor] (i : signature) : precategory (Group i) :=
   precategory.mk homomorphism
-                 @homomorphism_compose
+                 (@homomorphism_compose _ _ _)
-                 @homomorphism_id
+                 (@homomorphism_id _)
                  (λG₁ G₂ G₃ G₄ φ₃ φ₂ φ₁, homomorphism_eq (λg, idp))
                  (λG₁ G₂ φ, homomorphism_eq (λg, idp))
                  (λG₁ G₂ φ, homomorphism_eq (λg, idp))
@@ -260,15 +271,17 @@ namespace group
 
   end
 
-  definition trivial_group_of_is_contr (G : Group) [H : is_contr G] : G ≃g G0 :=
+  variable (G)
+  definition trivial_group_of_is_contr [H : is_contr G] : G ≃g G0 :=
   begin
     fapply isomorphism_of_equiv,
     { apply equiv_unit_of_is_contr},
     { intros, reflexivity}
   end
 
-  definition trivial_group_of_is_contr' (G : Group) [H : is_contr G] : G = G0 :=
+  definition trivial_group_of_is_contr' (G : MulGroup) [H : is_contr G] : G = G0 :=
   eq_of_isomorphism (trivial_group_of_is_contr G)
+  variable {G}
 
   /-
     A group where the point in the pointed type corresponds with 1 in the group.

hott/algebra/homotopy_group.hlean

@@ -36,13 +36,13 @@ namespace eq
 
   local attribute comm_group_homotopy_group [instance]
 
-  definition ghomotopy_group [constructor] (n : ℕ) (A : Type*) : Group :=
+  definition ghomotopy_group [constructor] (n : ℕ) (A : Type*) : MulGroup :=
-  Group.mk (π[succ n] A) _
+  MulGroup.mk (π[succ n] A) _
 
-  definition cghomotopy_group [constructor] (n : ℕ) (A : Type*) : CommGroup :=
+  definition cghomotopy_group [constructor] (n : ℕ) (A : Type*) : MulCommGroup :=
-  CommGroup.mk (π[succ (succ n)] A) _
+  MulCommGroup.mk (π[succ (succ n)] A) _
 
-  definition fundamental_group [constructor] (A : Type*) : Group :=
+  definition fundamental_group [constructor] (A : Type*) : MulGroup :=
   ghomotopy_group zero A
 
   notation `πg[`:95  n:0 ` +1] `:0 A:95 := ghomotopy_group n A

hott/algebra/hott.hlean

@@ -15,8 +15,8 @@ namespace algebra
   definition trivial_group [constructor] : group unit :=
   group.mk (λx y, star) _ (λx y z, idp) star (unit.rec idp) (unit.rec idp) (λx, star) (λx, idp)
 
-  definition Trivial_group [constructor] : Group :=
+  definition Trivial_group [constructor] : MulGroup :=
-  Group.mk _ trivial_group
+  MulGroup.mk _ trivial_group
 
   abbreviation G0 := Trivial_group
 
@@ -65,15 +65,15 @@ namespace algebra
     apply pathover_idp_of_eq, exact group_eq (resp_mul)
   end
 
-  definition Group_eq_of_eq {G H : Group} (p : carrier G = carrier H)
+  definition Group_eq_of_eq {i : signature} {G H : Group i} (p : carrier G = carrier H)
     (resp_mul : Π(g h : G), cast p (g * h) = cast p g * cast p h) : G = H :=
   begin
     cases G with Gc G, cases H with Hc H,
-    apply (apd011 mk p),
+    apply (apd011 (Group.mk i) p),
     exact group_pathover resp_mul
   end
 
-  definition Group_eq {G H : Group} (f : carrier G ≃ carrier H)
+  definition Group_eq {i : signature} {G H : Group i} (f : carrier G ≃ carrier H)
     (resp_mul : Π(g h : G), f (g * h) = f g * f h) : G = H :=
   Group_eq_of_eq (ua f) (λg h, !cast_ua ⬝ resp_mul g h ⬝ ap011 mul !cast_ua⁻¹ !cast_ua⁻¹)
 

hott/homotopy/EM.hlean

@@ -14,10 +14,10 @@ open algebra pointed nat eq category group algebra is_trunc iso pointed unit tru
 namespace EM
   open groupoid_quotient
 
-  variable {G : Group}
+  variables {i : signature} {G : Group i}
-  definition EM1 (G : Group) : Type :=
+  definition EM1 {i : signature} (G : Group i) : Type :=
   groupoid_quotient (Groupoid_of_Group G)
-  definition pEM1 [constructor] (G : Group) : Type* :=
+  definition pEM1 [constructor] {i : signature} (G : Group i) : Type* :=
   pointed.MK (EM1 G) (elt star)
 
   definition base : EM1 G := elt star
@@ -95,18 +95,19 @@ namespace EM
 end EM
 
 attribute EM.base [constructor]
-attribute EM.rec EM.elim [unfold 7] [recursor 7]
+attribute EM.rec EM.elim [unfold 8] [recursor 8]
-attribute EM.rec_on EM.elim_on [unfold 4]
+attribute EM.rec_on EM.elim_on [unfold 5]
-attribute EM.set_rec EM.set_elim [unfold 6]
+attribute EM.set_rec EM.set_elim [unfold 7]
-attribute EM.prop_rec EM.prop_elim EM.elim_set [unfold 5]
+attribute EM.prop_rec EM.prop_elim EM.elim_set [unfold 6]
 
 namespace EM
   open groupoid_quotient
 
-  definition base_eq_base_equiv [constructor] (G : Group) : (base = base :> pEM1 G) ≃ G :=
+  variables {i : signature} (G : Group i)
+  definition base_eq_base_equiv [constructor] : (base = base :> pEM1 G) ≃ G :=
   !elt_eq_elt_equiv
 
-  definition fundamental_group_pEM1 (G : Group) : π₁ (pEM1 G) ≃g G :=
+  definition fundamental_group_pEM1 : π₁ (pEM1 G) ≃g G :=
   begin
     fapply isomorphism_of_equiv,
     { exact trunc_equiv_trunc 0 !base_eq_base_equiv ⬝e trunc_equiv 0 G},
@@ -114,19 +115,20 @@ namespace EM
       exact encode_con p q}
   end
 
-  proposition is_trunc_pEM1 [instance] (G : Group) : is_trunc 1 (pEM1 G) :=
+  proposition is_trunc_pEM1 [instance] : is_trunc 1 (pEM1 G) :=
   !is_trunc_groupoid_quotient
 
-  proposition is_trunc_EM1 [instance] (G : Group) : is_trunc 1 (EM1 G) :=
+  proposition is_trunc_EM1 [instance] : is_trunc 1 (EM1 G) :=
   !is_trunc_groupoid_quotient
 
-  proposition is_conn_EM1 [instance] (G : Group) : is_conn 0 (EM1 G) :=
+  proposition is_conn_EM1 [instance] : is_conn 0 (EM1 G) :=
   by apply @is_conn_groupoid_quotient; esimp; exact _
 
-  proposition is_conn_pEM1 [instance] (G : Group) : is_conn 0 (pEM1 G) :=
+  proposition is_conn_pEM1 [instance] : is_conn 0 (pEM1 G) :=
   is_conn_EM1 G
+  variable {G}
 
-  definition EM1_map [unfold 7] {G : Group} {X : Type*} (e : Ω X ≃ G)
+  definition EM1_map [unfold 7] {X : Type*} (e : Ω X ≃ G)
     (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : EM1 G → X :=
   begin
     intro x, induction x using EM.elim,
@@ -140,9 +142,9 @@ end EM
 open hopf susp
 namespace EM
   -- The K(G,n+1):
-  variables (G : CommGroup) (n : ℕ)
+  variables {i : signature} {G : CommGroup i} (n : ℕ)
 
-  definition EM1_mul [unfold 2 3] {G : CommGroup} (x x' : EM1 G) : EM1 G :=
+  definition EM1_mul [unfold 2 3] (x x' : EM1 G) : EM1 G :=
   begin
     induction x,
     { exact x'},
@@ -154,14 +156,15 @@ namespace EM
     { refine EM.prop_rec _ x', apply resp_mul}
   end
 
-  definition EM1_mul_one (G : CommGroup) (x : EM1 G) : EM1_mul x base = x :=
+  variable (G)
+  definition EM1_mul_one (x : EM1 G) : EM1_mul x base = x :=
   begin
     induction x using EM.set_rec,
     { reflexivity},
     { apply eq_pathover_id_right, apply hdeg_square, refine EM.elim_pth _ g}
   end
 
-  definition h_space_EM1 [constructor] [instance] (G : CommGroup) : h_space (pEM1 G) :=
+  definition h_space_EM1 [constructor] [instance] : h_space (pEM1 G) :=
   begin
     fapply h_space.mk,
     { exact EM1_mul},
@@ -171,22 +174,22 @@ namespace EM
   end
 
   /- K(G, n+1) -/
-  definition EMadd1 (G : CommGroup) (n : ℕ) : Type* :=
+  definition EMadd1 (n : ℕ) : Type* :=
   ptrunc (n+1) (iterate_psusp n (pEM1 G))
 
-  definition loop_EM2 (G : CommGroup) : Ω[1] (EMadd1 G 1) ≃* pEM1 G :=
+  definition loop_EM2 : Ω[1] (EMadd1 G 1) ≃* pEM1 G :=
   begin
     apply hopf.delooping, reflexivity
   end
 
-  definition homotopy_group_EM2 (G : CommGroup) : πg[1+1] (EMadd1 G 1) ≃g G :=
+  definition homotopy_group_EM2 : πg[1+1] (EMadd1 G 1) ≃g G :=
   begin
     refine ghomotopy_group_succ_in _ 0 ⬝g _,
     refine homotopy_group_isomorphism_of_pequiv 0 (loop_EM2 G) ⬝g _,
     apply fundamental_group_pEM1
   end
 
-  definition homotopy_group_EMadd1 (G : CommGroup) (n : ℕ) : πg[n+1] (EMadd1 G n) ≃g G :=
+  definition homotopy_group_EMadd1 (n : ℕ) : πg[n+1] (EMadd1 G n) ≃g G :=
   begin
     cases n with n,
     { refine homotopy_group_isomorphism_of_pequiv 0 _ ⬝g fundamental_group_pEM1 G,
@@ -201,42 +204,43 @@ namespace EM
 
   section
     local attribute EMadd1 [reducible]
-    definition is_conn_EMadd1 [instance] (G : CommGroup) (n : ℕ) : is_conn n (EMadd1 G n) := _
+    definition is_conn_EMadd1 [instance] (n : ℕ) : is_conn n (EMadd1 G n) := _
 
-    definition is_trunc_EMadd1 [instance] (G : CommGroup) (n : ℕ) : is_trunc (n+1) (EMadd1 G n) := _
+    definition is_trunc_EMadd1 [instance] (n : ℕ) : is_trunc (n+1) (EMadd1 G n) :=
+    _
   end
 
   /- K(G, n) -/
-  definition EM (G : CommGroup) : ℕ → Type*
+  definition EM {i : signature} (G : CommGroup i) : ℕ → Type*
   | 0     := pType_of_Group G
   | (k+1) := EMadd1 G k
 
   namespace ops
-    abbreviation K := EM
+    abbreviation K := @EM
   end ops
   open ops
 
-  definition phomotopy_group_EM (G : CommGroup) (n : ℕ) : π*[n] (EM G n) ≃* pType_of_Group G :=
+  definition phomotopy_group_EM (n : ℕ) : π*[n] (EM G n) ≃* pType_of_Group G :=
   begin
     cases n with n,
     { rexact ptrunc_pequiv 0 (pType_of_Group G) _},
     { apply pequiv_of_isomorphism (homotopy_group_EMadd1 G n)}
   end
 
-  definition ghomotopy_group_EM (G : CommGroup) (n : ℕ) : πg[n+1] (EM G (n+1)) ≃g G :=
+  definition ghomotopy_group_EM (n : ℕ) : πg[n+1] (EM G (n+1)) ≃g G :=
   homotopy_group_EMadd1 G n
 
-  definition is_conn_EM [instance] (G : CommGroup) (n : ℕ) : is_conn (n.-1) (EM G n) :=
+  definition is_conn_EM [instance] (n : ℕ) : is_conn (n.-1) (EM G n) :=
   begin
     cases n with n,
     { apply is_conn_minus_one, apply tr, unfold [EM], exact 1},
     { apply is_conn_EMadd1}
   end
 
-  definition is_conn_EM_succ [instance] (G : CommGroup) (n : ℕ) : is_conn n (EM G (succ n)) :=
+  definition is_conn_EM_succ [instance] (n : ℕ) : is_conn n (EM G (succ n)) :=
   is_conn_EM G (succ n)
 
-  definition is_trunc_EM [instance] (G : CommGroup) (n : ℕ) : is_trunc n (EM G n) :=
+  definition is_trunc_EM [instance] (n : ℕ) : is_trunc n (EM G n) :=
   begin
     cases n with n,
     { unfold [EM], apply semigroup.is_set_carrier},
@@ -244,26 +248,29 @@ namespace EM
   end
 
   /- Uniqueness of K(G, 1) -/
-  definition pEM1_pmap [constructor] {G : Group} {X : Type*} (e : Ω X ≃ G)
+  variable {H : Group i}
-    (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 G →* X :=
+  definition pEM1_pmap [constructor] {X : Type*} (e : Ω X ≃ H)
+    (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 H →* X :=
   begin
     apply pmap.mk (EM1_map e r),
     reflexivity,
   end
 
-  definition loop_pEM1 [constructor] (G : Group) : Ω (pEM1 G) ≃* pType_of_Group G :=
+  variable (H)
-  pequiv_of_equiv (base_eq_base_equiv G) idp
+  definition loop_pEM1 [constructor] : Ω (pEM1 H) ≃* pType_of_Group H :=
+  pequiv_of_equiv (base_eq_base_equiv H) idp
 
-  definition loop_pEM1_pmap {G : Group} {X : Type*} (e : Ω X ≃ G)
+  variable {H}
+  definition loop_pEM1_pmap {X : Type*} (e : Ω X ≃ H)
     (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] :
-    Ω→(pEM1_pmap e r) ~ e⁻¹ᵉ ∘ base_eq_base_equiv G :=
+    Ω→(pEM1_pmap e r) ~ e⁻¹ᵉ ∘ base_eq_base_equiv H :=
   begin
-    apply homotopy_of_inv_homotopy_pre (base_eq_base_equiv G),
+    apply homotopy_of_inv_homotopy_pre (base_eq_base_equiv H),
     intro g, exact !idp_con ⬝ !elim_pth
   end
 
   open trunc_index
-  definition pEM1_pequiv'.{u} {G : Group.{u}} {X : pType.{u}} (e : Ω X ≃ G)
+  definition pEM1_pequiv'.{u} {i : signature} {G : Group.{u} i} {X : pType.{u}} (e : Ω X ≃ G)
     (r : Πp q, e (p ⬝ q) = e p * e q) [is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X :=
   begin
     apply pequiv_of_pmap (pEM1_pmap e r),
@@ -280,7 +287,7 @@ namespace EM
         do 2 exact trivial_homotopy_group_of_is_trunc _ (succ_lt_succ !zero_lt_succ)}}
   end
 
-  definition pEM1_pequiv.{u} {G : Group.{u}} {X : pType.{u}} (e : π₁ X ≃g G)
+  definition pEM1_pequiv.{u} {i : signature} {G : Group.{u} i} {X : pType.{u}} (e : π₁ X ≃g G)
     [is_conn 0 X] [is_trunc 1 X] : pEM1 G ≃* X :=
   begin
     apply pEM1_pequiv' (!trunc_equiv⁻¹ᵉ ⬝e equiv_of_isomorphism e),
@@ -290,7 +297,7 @@ namespace EM
   definition pEM1_pequiv_type {X : Type*} [is_conn 0 X] [is_trunc 1 X] : pEM1 (π₁ X) ≃* X :=
   pEM1_pequiv !isomorphism.refl
 
-  definition EM_pequiv_1.{u} {G : CommGroup.{u}} {X : pType.{u}} (e : π₁ X ≃g G)
+  definition EM_pequiv_1.{u} {i : signature} {G : CommGroup.{u} i} {X : pType.{u}} (e : π₁ X ≃g G)
     [is_conn 0 X] [is_trunc 1 X] : EM G 1 ≃* X :=
   begin
     refine _ ⬝e* pEM1_pequiv e,
@@ -298,11 +305,12 @@ namespace EM
     apply is_trunc_pEM1
   end
 
-  definition EMadd1_pequiv_pEM1 (G : CommGroup) : EMadd1 G 0 ≃* pEM1 G :=
+  variable (G)
+  definition EMadd1_pequiv_pEM1 : EMadd1 G 0 ≃* pEM1 G :=
   begin apply ptrunc_pequiv, apply is_trunc_pEM1 end
 
-  definition EM1add1_pequiv_0.{u} {G : CommGroup.{u}} {X : pType.{u}} (e : π₁ X ≃g G)
+  definition EM1add1_pequiv_0.{u} {i : signature} {G : CommGroup.{u} i} {X : pType.{u}}
-    [is_conn 0 X] [is_trunc 1 X] : EMadd1 G 0 ≃* X :=
+    (e : π₁ X ≃g G) [is_conn 0 X] [is_trunc 1 X] : EMadd1 G 0 ≃* X :=
   EMadd1_pequiv_pEM1 G ⬝e* pEM1_pequiv e
 
   definition KG1_pequiv.{u} {X Y : pType.{u}} (e : π₁ X ≃g π₁ Y)
@@ -314,7 +322,8 @@ namespace EM
   !EMadd1_pequiv_pEM1 ⬝e* pEM1_pequiv fundamental_group_of_circle
 
   /- loops of EM-spaces -/
-  definition loop_EMadd1 {G : CommGroup} (n : ℕ) : Ω (EMadd1 G (succ n)) ≃* EMadd1 G n :=
+  variable {G}
+  definition loop_EMadd1 (n : ℕ) : Ω (EMadd1 G (succ n)) ≃* EMadd1 G n :=
   begin
     cases n with n,
     { symmetry, apply EM1add1_pequiv_0, rexact homotopy_group_EMadd1 G 1,
@@ -326,7 +335,8 @@ namespace EM
       symmetry, refine freudenthal_pequiv _ this, }
   end
 
-  definition loop_EM (G : CommGroup) (n : ℕ) : Ω (K G (succ n)) ≃* K G n :=
+  variable (G)
+  definition loop_EM (n : ℕ) : Ω (K G (succ n)) ≃* K G n :=
   begin
     cases n with n,
     { refine _ ⬝e* pequiv_of_isomorphism (fundamental_group_pEM1 G),

hott/homotopy/LES_of_homotopy_groups.hlean

@@ -729,12 +729,12 @@ namespace chain_complex
   | (fin.mk 2 H) := proof comm_group_homotopy_group n (pfiber f) qed
   | (fin.mk (k+3) H) := begin exfalso, apply lt_le_antisymm H, apply le_add_left end
 
-  definition Group_LES_of_homotopy_groups (x : +3ℕ) : Group.{u} :=
+  definition Group_LES_of_homotopy_groups (x : +3ℕ) : MulGroup.{u} :=
-  Group.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x))
+  MulGroup.mk (LES_of_homotopy_groups (nat.succ (pr1 x), pr2 x))
               (group_LES_of_homotopy_groups (pr1 x) (pr2 x))
 
-  definition CommGroup_LES_of_homotopy_groups (n : +3ℕ) : CommGroup.{u} :=
+  definition CommGroup_LES_of_homotopy_groups (n : +3ℕ) : MulCommGroup.{u} :=
-  CommGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n))
+  MulCommGroup.mk (LES_of_homotopy_groups (pr1 n + 2, pr2 n))
                   (comm_group_LES_of_homotopy_groups (pr1 n) (pr2 n))
 
   definition homomorphism_LES_of_homotopy_groups_fun : Π(k : +3ℕ),

hott/types/int/hott.hlean

@@ -14,13 +14,14 @@ namespace int
 
   section
   open algebra
-  definition group_integers [constructor] : Group :=
+  definition group_integers [constructor] : AddGroup :=
-  Group.mk ℤ (group_of_add_group _)
+  AddGroup.mk ℤ _
 
   notation `gℤ` := group_integers
 
-  definition CommGroup_int [constructor] : CommGroup :=
+  definition CommGroup_int [constructor] : AddCommGroup :=
-  CommGroup.mk ℤ ⦃comm_group, group_of_add_group ℤ, mul_comm := add.comm⦄
+  AddCommGroup.mk ℤ _
+
   notation `agℤ` := CommGroup_int
   end
 

library/algebra/group.lean

@@ -127,6 +127,21 @@ definition add_comm_monoid.to_comm_monoid {A : Type} [add_comm_monoid A] : comm_
   mul_comm    := add_comm_monoid.add_comm
 ⦄
 
+definition monoid.to_add_monoid {A : Type} [s : monoid A] : add_monoid A :=
+⦃ add_monoid,
+  add         := monoid.mul,
+  add_assoc   := monoid.mul_assoc,
+  zero        := monoid.one A,
+  add_zero    := monoid.mul_one,
+  zero_add    := monoid.one_mul
+⦄
+
+definition comm_monoid.to_add_comm_monoid {A : Type} [s : comm_monoid A] : add_comm_monoid A :=
+⦃ add_comm_monoid,
+  monoid.to_add_monoid,
+  add_comm    := comm_monoid.mul_comm
+⦄
+
 section add_comm_monoid
   variables [add_comm_monoid A]
 
@@ -314,6 +329,9 @@ definition add_group.to_group {A : Type} [add_group A] : group A :=
 ⦃ group, add_monoid.to_monoid,
   mul_left_inv := add_group.add_left_inv ⦄
 
+definition group.to_add_group {A : Type} [s : group A] : add_group A :=
+⦃ add_group, monoid.to_add_monoid,
+  add_left_inv := group.mul_left_inv ⦄
 
 section add_group
   variables [s : add_group A]
@@ -541,6 +559,15 @@ end add_group
 
 structure add_comm_group [class] (A : Type) extends add_group A, add_comm_monoid A
 
+definition add_comm_group.to_comm_group (A : Type) [s : add_comm_group A] : comm_group A :=
+⦃ comm_group, add_group.to_group,
+  mul_comm := add_comm_group.add_comm ⦄
+
+definition comm_group.to_add_comm_group (A : Type) [s : comm_group A] : add_comm_group A :=
+⦃ add_comm_group, group.to_add_group,
+  add_comm := comm_group.mul_comm ⦄
+
+
 section add_comm_group
   variable [s : add_comm_group A]
   include s