diff --git a/algebra/direct_sum.hlean b/algebra/direct_sum.hlean
index 7e8a892..db2df16 100644
--- a/algebra/direct_sum.hlean
+++ b/algebra/direct_sum.hlean
@@ -12,32 +12,32 @@ open eq algebra is_trunc set_quotient relation sigma prod sum list trunc functio
 
 namespace group
 
-  variables {G G' : Group} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
-            {A B : AbGroup}
+  variables {G G' : AddGroup} (H : subgroup_rel G) (N : normal_subgroup_rel G) {g g' h h' k : G}
+            {A B : AddAbGroup}
 
   variables (X : Set) {l l' : list (X ⊎ X)}
 
   section
 
-    parameters {I : Set} (Y : I → AbGroup)
-    variables {A' : AbGroup} {Y' : I → AbGroup}
+    parameters {I : Set} (Y : I → AddAbGroup)
+    variables {A' : AddAbGroup} {Y' : I → AddAbGroup}
 
-    definition dirsum_carrier : AbGroup := free_ab_group (trunctype.mk (Σi, Y i) _)
+    definition dirsum_carrier : AddAbGroup := free_ab_group (trunctype.mk (Σi, Y i) _)
     local abbreviation ι [constructor] := @free_ab_group_inclusion
     inductive dirsum_rel : dirsum_carrier → Type :=
-    | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ * ι ⟨i, y₂⟩ * (ι ⟨i, y₁ * y₂⟩)⁻¹)
+    | rmk : Πi y₁ y₂, dirsum_rel (ι ⟨i, y₁⟩ + ι ⟨i, y₂⟩ +  -(ι ⟨i, y₁ + y₂⟩))
 
     definition dirsum : AddAbGroup := quotient_ab_group_gen dirsum_carrier (λg, ∥dirsum_rel g∥)
 
-    -- definition dirsum_carrier_incl [constructor] (i : I) : Y i →g dirsum_carrier :=
+    -- definition dirsum_carrier_incl [constructor] (i : I) : Y i →a dirsum_carrier :=
 
-    definition dirsum_incl [constructor] (i : I) : Y i →g dirsum :=
-    homomorphism.mk (λy, class_of (ι ⟨i, y⟩))
+    definition dirsum_incl [constructor] (i : I) : Y i →a dirsum :=
+    add_homomorphism.mk (λy, class_of (ι ⟨i, y⟩))
       begin intro g h, symmetry, apply gqg_eq_of_rel, apply tr, apply dirsum_rel.rmk end
 
     parameter {Y}
     definition dirsum.rec {P : dirsum → Type} [H : Πg, is_prop (P g)]
-      (h₁ : Πi (y : Y i), P (dirsum_incl i y)) (h₂ : P 1) (h₃ : Πg h, P g → P h → P (g * h)) :
+      (h₁ : Πi (y : Y i), P (dirsum_incl i y)) (h₂ : P 0) (h₃ : Πg h, P g → P h → P (g + h)) :
       Πg, P g :=
     begin
       refine @set_quotient.rec_prop _ _ _ H _,
@@ -49,42 +49,42 @@ namespace group
         exact h₃ _ _ (h₁ i y) ih,
       induction v with i y,
       refine h₃ (gqg_map _ _ (class_of [inr ⟨i, y⟩])) _ _ ih,
-      refine transport P _ (h₁ i y⁻¹),
+      refine transport P _ (h₁ i (-y)),
       refine _ ⬝ !one_mul,
-      refine _ ⬝ ap (λx, mul x _) (to_respect_one (dirsum_incl i)),
+      refine _ ⬝ ap (λx, mul x _) (to_respect_zero (dirsum_incl i)),
       apply gqg_eq_of_rel',
       apply tr, esimp,
-      refine transport dirsum_rel _ (dirsum_rel.rmk i y⁻¹ y),
-      rewrite [mul.left_inv, mul.assoc],
+      refine transport dirsum_rel _ (dirsum_rel.rmk i (-y) y),
+      rewrite [add.left_inv, add.assoc],
     end
 
-    definition dirsum_homotopy {φ ψ : dirsum →g A'}
+    definition dirsum_homotopy {φ ψ : dirsum →a A'}
       (h : Πi (y : Y i), φ (dirsum_incl i y) = ψ (dirsum_incl i y)) : φ ~ ψ :=
     begin
       refine dirsum.rec _ _ _,
           exact h,
-        refine !respect_one ⬝ !respect_one⁻¹,
-      intro g₁ g₂ h₁ h₂, rewrite [+ to_respect_mul, h₁, h₂]
+        refine !to_respect_zero ⬝ !to_respect_zero⁻¹,
+      intro g₁ g₂ h₁ h₂, rewrite [+ to_respect_add, h₁, h₂]
     end
 
-    definition dirsum_elim_resp_quotient (f : Πi, Y i →g A') (g : dirsum_carrier)
+    definition dirsum_elim_resp_quotient (f : Πi, Y i →a A') (g : dirsum_carrier)
       (r : ∥dirsum_rel g∥) : free_ab_group_elim (λv, f v.1 v.2) g = 1 :=
     begin
       induction r with r, induction r,
-      rewrite [to_respect_mul, to_respect_inv], apply mul_inv_eq_of_eq_mul,
-      rewrite [one_mul, to_respect_mul, ▸*, ↑foldl, +one_mul, to_respect_mul]
+      rewrite [to_respect_add, to_respect_neg], apply add_neg_eq_of_eq_add,
+      rewrite [zero_add, to_respect_add, ▸*, ↑foldl, +one_mul, to_respect_add]
     end
 
-    definition dirsum_elim [constructor] (f : Πi, Y i →g A') : dirsum →g A' :=
+    definition dirsum_elim [constructor] (f : Πi, Y i →a A') : dirsum →a A' :=
     gqg_elim _ (free_ab_group_elim (λv, f v.1 v.2)) (dirsum_elim_resp_quotient f)
 
-    definition dirsum_elim_compute (f : Πi, Y i →g A') (i : I) :
+    definition dirsum_elim_compute (f : Πi, Y i →a A') (i : I) :
       dirsum_elim f ∘g dirsum_incl i ~ f i :=
     begin
-      intro g, apply one_mul
+      intro g, apply zero_add
     end
 
-    definition dirsum_elim_unique (f : Πi, Y i →g A') (k : dirsum →g A')
+    definition dirsum_elim_unique (f : Πi, Y i →a A') (k : dirsum →a A')
       (H : Πi, k ∘g dirsum_incl i ~ f i) : k ~ dirsum_elim f :=
     begin
       apply gqg_elim_unique,
@@ -96,25 +96,25 @@ namespace group
 
   variables {I J : Set} {Y Y' Y'' : I → AddAbGroup}
 
-  definition dirsum_functor [constructor] (f : Πi, Y i →g Y' i) : dirsum Y →g dirsum Y' :=
+  definition dirsum_functor [constructor] (f : Πi, Y i →a Y' i) : dirsum Y →a dirsum Y' :=
   dirsum_elim (λi, dirsum_incl Y' i ∘g f i)
 
-  theorem dirsum_functor_compose (f' : Πi, Y' i →g Y'' i) (f : Πi, Y i →g Y' i) :
-    dirsum_functor f' ∘g dirsum_functor f ~ dirsum_functor (λi, f' i ∘g f i) :=
+  theorem dirsum_functor_compose (f' : Πi, Y' i →a Y'' i) (f : Πi, Y i →a Y' i) :
+    dirsum_functor f' ∘a dirsum_functor f ~ dirsum_functor (λi, f' i ∘a f i) :=
   begin
     apply dirsum_homotopy,
     intro i y, reflexivity,
   end
 
   variable (Y)
-  definition dirsum_functor_gid : dirsum_functor (λi, gid (Y i)) ~ gid (dirsum Y) :=
+  definition dirsum_functor_gid : dirsum_functor (λi, aid (Y i)) ~ aid (dirsum Y) :=
   begin
     apply dirsum_homotopy,
     intro i y, reflexivity,
   end
   variable {Y}
 
-  definition dirsum_functor_add (f f' : Πi, Y i →g Y' i) :
+  definition dirsum_functor_add (f f' : Πi, Y i →a Y' i) :
     homomorphism_add (dirsum_functor f) (dirsum_functor f') ~
     dirsum_functor (λi, homomorphism_add (f i) (f' i)) :=
   begin
@@ -122,14 +122,14 @@ namespace group
     intro i y, exact sorry
   end
 
-  definition dirsum_functor_homotopy {f f' : Πi, Y i →g Y' i} (p : f ~2 f') :
+  definition dirsum_functor_homotopy {f f' : Πi, Y i →a Y' i} (p : f ~2 f') :
     dirsum_functor f ~ dirsum_functor f' :=
   begin
     apply dirsum_homotopy,
     intro i y, exact sorry
   end
 
-  definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →g dirsum Y :=
+  definition dirsum_functor_left [constructor] (f : J → I) : dirsum (Y ∘ f) →a dirsum Y :=
   dirsum_elim (λj, dirsum_incl Y (f j))
 
 end group
diff --git a/algebra/left_module.hlean b/algebra/left_module.hlean
index 3664b60..165a5ab 100644
--- a/algebra/left_module.hlean
+++ b/algebra/left_module.hlean
@@ -20,8 +20,8 @@ infixl ` • `:73 := has_scalar.smul
 namespace left_module
 
 structure left_module (R M : Type) [ringR : ring R] extends has_scalar R M, ab_group M renaming
-  mul→add mul_assoc→add_assoc one→zero one_mul→zero_add mul_one→add_zero inv→neg
-  mul_left_inv→add_left_inv mul_comm→add_comm :=
+  mul → add mul_assoc → add_assoc one → zero one_mul → zero_add mul_one → add_zero inv → neg
+  mul_left_inv → add_left_inv mul_comm → add_comm :=
 (smul_left_distrib : Π (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y)))
 (smul_right_distrib : Π (r s : R) (x : M), smul (ring.add _ r s) x = (add (smul r x) (smul s x)))
 (mul_smul : Π r s x, smul (mul r s) x = smul r (smul s x))
@@ -146,9 +146,18 @@ end module_hom
 structure LeftModule (R : Ring) :=
 (carrier : Type) (struct : left_module R carrier)
 
-attribute LeftModule.carrier [coercion]
 attribute LeftModule.struct [instance]
 
+section
+local attribute LeftModule.carrier [coercion]
+
+definition AddAbGroup_of_LeftModule [coercion] {R : Ring} (M : LeftModule R) : AddAbGroup :=
+AddAbGroup.mk M (LeftModule.struct M)
+end
+
+definition LeftModule.struct2 [instance] {R : Ring} (M : LeftModule R) : left_module R M :=
+LeftModule.struct M
+
 definition pointed_LeftModule_carrier [instance] {R : Ring} (M : LeftModule R) :
   pointed (LeftModule.carrier M) :=
 pointed.mk zero
@@ -156,9 +165,6 @@ pointed.mk zero
 definition pSet_of_LeftModule {R : Ring} (M : LeftModule R) : Set* :=
 pSet.mk' (LeftModule.carrier M)
 
-definition AddAbGroup_of_LeftModule [coercion] {R : Ring} (M : LeftModule R) : AddAbGroup :=
-AddAbGroup.mk M _
-
 definition left_module_AddAbGroup_of_LeftModule [instance] {R : Ring} (M : LeftModule R) :
   left_module R (AddAbGroup_of_LeftModule M) :=
 LeftModule.struct M
@@ -182,8 +188,7 @@ LeftModule.mk G (left_module_of_ab_group G R smul h1 h2 h3 h4)
 section
   variables {R : Ring} {M M₁ M₂ M₃ : LeftModule R}
 
-  definition smul_homomorphism [constructor] (M : LeftModule R) (r : R) :
-    AddAbGroup_of_LeftModule M →g AddAbGroup_of_LeftModule M :=
+  definition smul_homomorphism [constructor] (M : LeftModule R) (r : R) : M →a M :=
   add_homomorphism.mk (λg, r • g) (smul_left_distrib r)
 
   proposition to_smul_left_distrib (a : R) (u v : M) : a • (u + v) = a • u + a • v :=
@@ -261,9 +266,6 @@ end
 
   section
 
-  definition LeftModule.struct2 [instance] (M : LeftModule R) : left_module R M :=
-  LeftModule.struct M
-
   definition homomorphism.mk' [constructor] (φ : M₁ → M₂)
     (p : Π(g₁ g₂ : M₁), φ (g₁ + g₂) = φ g₁ + φ g₂)
     (q : Π(r : R) x, φ (r • x) = r • φ x) : M₁ →lm M₂ :=
diff --git a/move_to_lib.hlean b/move_to_lib.hlean
index 3bf0054..f9f53a0 100644
--- a/move_to_lib.hlean
+++ b/move_to_lib.hlean
@@ -32,6 +32,28 @@ namespace algebra
 
   definition one_unique {A : Type} [group A] {a : A} (H : Πb, a * b = b) : a = 1 :=
   !mul_one⁻¹ ⬝ H 1
+
+  definition pSet_of_AddGroup [constructor] [reducible] [coercion] (G : AddGroup) : Set* :=
+  pSet_of_Group G
+  attribute algebra._trans_of_pSet_of_AddGroup [unfold 1]
+  attribute algebra._trans_of_pSet_of_AddGroup_1 algebra._trans_of_pSet_of_AddGroup_2 [constructor]
+
+  definition pType_of_AddGroup [reducible] [constructor] : AddGroup → Type* :=
+  algebra._trans_of_pSet_of_AddGroup_1
+  definition Set_of_AddGroup [reducible] [constructor] : AddGroup → Set :=
+  algebra._trans_of_pSet_of_AddGroup_2
+
+  definition AddGroup_of_AddAbGroup [coercion] [constructor] (G : AddAbGroup) : AddGroup :=
+  AddGroup.mk G _
+
+  attribute algebra._trans_of_AddGroup_of_AddAbGroup_1
+            algebra._trans_of_AddGroup_of_AddAbGroup
+            algebra._trans_of_AddGroup_of_AddAbGroup_3 [constructor]
+  attribute algebra._trans_of_AddGroup_of_AddAbGroup_2 [unfold 1]
+
+  definition add_ab_group_AddAbGroup2 [instance] (G : AddAbGroup) : add_ab_group G :=
+  AddAbGroup.struct G
+
 end algebra
 
 namespace eq
@@ -484,20 +506,48 @@ namespace pointed
 end pointed open pointed
 
 namespace group
-  open is_trunc
+  open is_trunc algebra
 
   definition to_fun_isomorphism_trans {G H K : Group} (φ : G ≃g H) (ψ : H ≃g K) :
     φ ⬝g ψ ~ ψ ∘ φ :=
   by reflexivity
 
-  definition add_homomorphism.mk [constructor] {G H : AddGroup} (φ : G → H) (h : is_add_hom φ) : G →g H :=
+  definition add_homomorphism (G H : AddGroup) : Type := homomorphism G H
+  infix ` →a `:55 := add_homomorphism
+
+  definition agroup_fun [coercion] {G H : AddGroup} (φ : G →a H) : G → H :=
+  φ
+
+  definition add_homomorphism.struct [instance] {G H : AddGroup} (φ : G →a H) : is_add_hom φ :=
+  homomorphism.addstruct φ
+
+  definition add_homomorphism.mk [constructor] {G H : AddGroup} (φ : G → H) (h : is_add_hom φ) : G →a H :=
   homomorphism.mk φ h
 
-  definition homomorphism_add [constructor] {G H : AddAbGroup} (φ ψ : G →g H) : G →g H :=
+  definition add_homomorphism_compose [constructor] [trans] {G₁ G₂ G₃ : AddGroup}
+    (ψ : G₂ →a G₃) (φ : G₁ →a G₂) : G₁ →a G₃ :=
+  add_homomorphism.mk (ψ ∘ φ) (is_add_hom_compose _ _)
+
+  definition add_homomorphism_id [constructor] [refl] (G : AddGroup) : G →a G :=
+  add_homomorphism.mk (@id G) (is_add_hom_id G)
+
+  abbreviation aid [constructor] := @add_homomorphism_id
+  infixr ` ∘a `:75 := add_homomorphism_compose
+
+  definition to_respect_add' {H₁ H₂ : AddGroup} (χ : H₁ →a H₂) (g h : H₁) : χ (g + h) = χ g + χ h :=
+  respect_add χ g h
+
+  theorem to_respect_zero' {H₁ H₂ : AddGroup} (χ : H₁ →a H₂) : χ 0 = 0 :=
+  respect_zero χ
+
+  theorem to_respect_neg' {H₁ H₂ : AddGroup} (χ : H₁ →a H₂) (g : H₁) : χ (-g) = -(χ g) :=
+  respect_neg χ g
+
+  definition homomorphism_add [constructor] {G H : AddAbGroup} (φ ψ : G →a H) : G →a H :=
   add_homomorphism.mk (λg, φ g + ψ g)
     abstract begin
-      intro g g', refine ap011 add !to_respect_add !to_respect_add ⬝ _,
-      refine !add.assoc ⬝ ap (add _) (!add.assoc⁻¹ ⬝ ap (λx, x * _) !add.comm ⬝ !add.assoc) ⬝ !add.assoc⁻¹
+      intro g g', refine ap011 add !to_respect_add' !to_respect_add' ⬝ _,
+      refine !add.assoc ⬝ ap (add _) (!add.assoc⁻¹ ⬝ ap (λx, x + _) !add.comm ⬝ !add.assoc) ⬝ !add.assoc⁻¹
     end end
 
   definition pmap_of_homomorphism_gid (G : Group) : pmap_of_homomorphism (gid G) ~* pid G :=
@@ -948,7 +998,6 @@ namespace sphere
     { exact psusp_pequiv e }
   end
 
-
   -- definition constant_sphere_map_sphere {n m : ℕ} (H : n < m) (f : S* n →* S* m) :
   --   f ~* pconst (S* n) (S* m) :=
   -- begin