diff --git a/src/category_theory/endomorphism.lean b/src/category_theory/endomorphism.lean
index 78389a5de8ad0..cbb9d263996cc 100644
--- a/src/category_theory/endomorphism.lean
+++ b/src/category_theory/endomorphism.lean
@@ -68,7 +68,7 @@ def units_End_eqv_Aut : units (End X) ≃* Aut X :=
   inv_fun := λ f, ⟨f.1, f.2, f.4, f.3⟩,
   left_inv := λ ⟨f₁, f₂, f₃, f₄⟩, rfl,
   right_inv := λ ⟨f₁, f₂, f₃, f₄⟩, rfl,
-  hom := ⟨λ f g, by rcases f; rcases g; refl⟩ }
+  map_mul' := λ f g, by rcases f; rcases g; refl }
 
 end Aut
 
diff --git a/src/data/equiv/algebra.lean b/src/data/equiv/algebra.lean
index 1bd09188ba98e..a90c8ec2c08f7 100644
--- a/src/data/equiv/algebra.lean
+++ b/src/data/equiv/algebra.lean
@@ -2,6 +2,12 @@
 Copyright (c) 2018 Johannes Hölzl. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl
+-/
+
+import data.equiv.basic algebra.field
+
+/-!
+# equivs in the algebraic hierarchy
 
 The role of this file is twofold. In the first part there are theorems of the following
 form: if α has a group structure and α ≃ β then β has a group structure, and
@@ -9,10 +15,26 @@ similarly for monoids, semigroups, rings, integral domains, fields and so on.
 
 In the second part there are extensions of equiv called add_equiv,
 mul_equiv, and ring_equiv, which are datatypes representing isomorphisms
-of monoids, groups and rings.
+of add_monoids/add_groups, monoids/groups and rings.
+
+## Notations
+
+The extended equivs all have coercions to functions, and the coercions are the canonical
+notation when treating the isomorphisms as maps.
+
+## Implementation notes
 
+Bundling structures means that many things turn into definitions, meaning that to_additive
+cannot do much work for us, and conversely that we have to do a lot of naming for it.
+
+The fields for mul_equiv and add_equiv now avoid the unbundled `is_mul_hom` and `is_add_hom`,
+as these are deprecated. However ring_equiv still relies on `is_ring_hom`; this should
+be rewritten in future.
+
+## Tags
+
+equiv, mul_equiv, add_equiv, ring_equiv
 -/
-import data.equiv.basic algebra.field
 
 universes u v w x
 variables {α : Type u} {β : Type v} {γ : Type w} {δ : Type x}
@@ -199,65 +221,212 @@ protected def discrete_field [discrete_field β] : discrete_field α :=
 end instances
 end equiv
 
+set_option old_structure_cmd true
+
+/-- mul_equiv α β is the type of an equiv α ≃ β which preserves multiplication. -/
 structure mul_equiv (α β : Type*) [has_mul α] [has_mul β] extends α ≃ β :=
-(hom : is_mul_hom to_fun)
+(map_mul' : ∀ x y : α, to_fun (x * y) = to_fun x * to_fun y)
 
+/-- add_equiv α β is the type of an equiv α ≃ β which preserves addition. -/
 structure add_equiv (α β : Type*) [has_add α] [has_add β] extends α ≃ β :=
-(hom : is_add_hom to_fun)
+(map_add' : ∀ x y : α, to_fun (x + y) = to_fun x + to_fun y)
 
 attribute [to_additive add_equiv] mul_equiv
+attribute [to_additive add_equiv.cases_on] mul_equiv.cases_on
+attribute [to_additive add_equiv.has_sizeof_inst] mul_equiv.has_sizeof_inst
+attribute [to_additive add_equiv.inv_fun] mul_equiv.inv_fun
+attribute [to_additive add_equiv.left_inv] mul_equiv.left_inv
 attribute [to_additive add_equiv.mk] mul_equiv.mk
+attribute [to_additive add_equiv.mk.inj] mul_equiv.mk.inj
+attribute [to_additive add_equiv.mk.inj_arrow] mul_equiv.mk.inj_arrow
+attribute [to_additive add_equiv.mk.inj_eq] mul_equiv.mk.inj_eq
+attribute [to_additive add_equiv.mk.sizeof_spec] mul_equiv.mk.sizeof_spec
+attribute [to_additive add_equiv.map_add'] mul_equiv.map_mul'
+attribute [to_additive add_equiv.no_confusion] mul_equiv.no_confusion
+attribute [to_additive add_equiv.no_confusion_type] mul_equiv.no_confusion_type
+attribute [to_additive add_equiv.rec] mul_equiv.rec
+attribute [to_additive add_equiv.rec_on] mul_equiv.rec_on
+attribute [to_additive add_equiv.right_inv] mul_equiv.right_inv
+attribute [to_additive add_equiv.sizeof] mul_equiv.sizeof
 attribute [to_additive add_equiv.to_equiv] mul_equiv.to_equiv
-attribute [to_additive add_equiv.hom] mul_equiv.hom
+attribute [to_additive add_equiv.to_fun] mul_equiv.to_fun
 
 infix ` ≃* `:25 := mul_equiv
 infix ` ≃+ `:25 := add_equiv
 
 namespace mul_equiv
 
+@[to_additive add_equiv.has_coe_to_fun]
+instance {α β} [has_mul α] [has_mul β] : has_coe_to_fun (α ≃* β) := ⟨_, mul_equiv.to_fun⟩
+
 variables [has_mul α] [has_mul β] [has_mul γ]
 
-@[to_additive add_mul.is_add_hom]
-instance (h : α ≃* β) : is_mul_hom h.to_equiv := h.hom
+/-- A multiplicative isomorphism preserves multiplication (canonical form). -/
+def map_mul (f : α ≃* β) :  ∀ x y : α, f (x * y) = f x * f y := f.map_mul'
 
+/-- A multiplicative isomorphism preserves multiplication (deprecated). -/
+instance (h : α ≃* β) : is_mul_hom h := ⟨h.map_mul⟩
+
+/-- The identity map is a multiplicative isomorphism. -/
 @[refl] def refl (α : Type*) [has_mul α] : α ≃* α :=
-{ hom := ⟨λ _ _,rfl⟩,
+{ map_mul' := λ _ _,rfl,
 ..equiv.refl _}
 
-attribute [to_additive add_equiv.refl._proof_3] mul_equiv.refl._proof_3
-attribute [to_additive add_equiv.refl] mul_equiv.refl
-
+/-- The inverse of an isomorphism is an isomorphism. -/
 @[symm] def symm (h : α ≃* β) : β ≃* α :=
-{ hom := ⟨λ n₁ n₂, function.injective_of_left_inverse h.left_inv begin
-   rw h.hom.map_mul, unfold equiv.symm, rw [h.right_inv, h.right_inv, h.right_inv], end⟩
+{ map_mul' := λ n₁ n₂, function.injective_of_left_inverse h.left_inv begin
+    show h.to_equiv (h.to_equiv.symm (n₁ * n₂)) =
+      h ((h.to_equiv.symm n₁) * (h.to_equiv.symm n₂)),
+   rw h.map_mul,
+   show _ = h.to_equiv (_) * h.to_equiv (_),
+   rw [h.to_equiv.apply_symm_apply, h.to_equiv.apply_symm_apply, h.to_equiv.apply_symm_apply], end,
   ..h.to_equiv.symm}
 
+@[simp] theorem to_equiv_symm (f : α ≃* β) : f.symm.to_equiv = f.to_equiv.symm := rfl
+
+/-- Transitivity of multiplication-preserving isomorphisms -/
+@[trans] def trans (h1 : α ≃* β) (h2 : β ≃* γ) : (α ≃* γ) :=
+{ map_mul' := λ x y, show h2 (h1 (x * y)) = h2 (h1 x) * h2 (h1 y),
+    by rw [h1.map_mul, h2.map_mul],
+  ..h1.to_equiv.trans h2.to_equiv }
+
+/-- e.right_inv in canonical form -/
+@[simp] def apply_symm_apply (e : α ≃* β) : ∀ (y : β), e (e.symm y) = y :=
+equiv.apply_symm_apply (e.to_equiv)
+
+/-- e.left_inv in canonical form -/
+@[simp] def symm_apply_apply (e : α ≃* β) : ∀ (x : α), e.symm (e x) = x :=
+equiv.symm_apply_apply (e.to_equiv)
+
+/-- a multiplicative equiv of monoids sends 1 to 1 (and is hence a monoid isomorphism) -/
+@[simp] def map_one {α β} [monoid α] [monoid β] (h : α ≃* β) : h 1 = 1 :=
+by rw [←mul_one (h 1), ←h.apply_symm_apply 1, ←h.map_mul, one_mul]
+
+/-- A multiplicative bijection between two monoids is an isomorphism. -/
+def to_monoid_hom {α β} [monoid α] [monoid β] (h : α ≃* β) : (α →* β) :=
+{ to_fun := h,
+  map_mul' := h.map_mul,
+  map_one' := h.map_one }
+
+/-- A multiplicative bijection between two monoids is a monoid hom
+  (deprecated -- use to_monoid_hom). -/
+instance is_monoid_hom {α β} [monoid α] [monoid β] (h : α ≃* β) : is_monoid_hom h :=
+⟨h.map_one⟩
+
+/-- A multiplicative bijection between two groups is a group hom
+  (deprecated -- use to_monoid_hom). -/
+instance is_group_hom {α β} [group α] [group β] (h : α ≃* β) :
+  is_group_hom h := { map_mul := h.map_mul }
+
+end mul_equiv
+
+namespace add_equiv
+
+variables [has_add α] [has_add β] [has_add γ]
+
+/-- An additive isomorphism preserves addition (canonical form). -/
+def map_add (f : α ≃+ β) :  ∀ x y : α, f (x + y) = f x + f y := f.map_add'
+
+attribute [to_additive add_equiv.map_add] mul_equiv.map_mul
+attribute [to_additive add_equiv.map_add.equations._eqn_1] mul_equiv.map_mul.equations._eqn_1
+
+/-- A additive isomorphism preserves multiplication (deprecated). -/
+instance (h : α ≃+ β) : is_add_hom h := ⟨h.map_add⟩
+
+/-- The identity map is an additive isomorphism. -/
+@[refl] def refl (α : Type*) [has_add α] : α ≃+ α :=
+{ map_add' := λ _ _,rfl,
+..equiv.refl _}
+
+attribute [to_additive add_equiv.refl] mul_equiv.refl
+attribute [to_additive add_equiv.refl._proof_1] mul_equiv.refl._proof_1
+attribute [to_additive add_equiv.refl._proof_2] mul_equiv.refl._proof_2
+attribute [to_additive add_equiv.refl._proof_3] mul_equiv.refl._proof_3
+attribute [to_additive add_equiv.refl.equations._eqn_1] mul_equiv.refl.equations._eqn_1
+
+/-- The inverse of an isomorphism is an isomorphism. -/
+@[symm] def symm (h : α ≃+ β) : β ≃+ α :=
+{ map_add' := λ n₁ n₂, function.injective_of_left_inverse h.left_inv begin
+    show h.to_equiv (h.to_equiv.symm (n₁ + n₂)) =
+      h ((h.to_equiv.symm n₁) + (h.to_equiv.symm n₂)),
+   rw h.map_add,
+   show _ = h.to_equiv (_) + h.to_equiv (_),
+   rw [h.to_equiv.apply_symm_apply, h.to_equiv.apply_symm_apply, h.to_equiv.apply_symm_apply], end,
+  ..h.to_equiv.symm}
+
+attribute [to_additive add_equiv.symm] mul_equiv.symm
 attribute [to_additive add_equiv.symm._proof_1] mul_equiv.symm._proof_1
 attribute [to_additive add_equiv.symm._proof_2] mul_equiv.symm._proof_2
 attribute [to_additive add_equiv.symm._proof_3] mul_equiv.symm._proof_3
-attribute [to_additive add_equiv.symm] mul_equiv.symm
+attribute [to_additive add_equiv.symm.equations._eqn_1] mul_equiv.symm.equations._eqn_1
 
-@[trans] def trans (h1 : α ≃* β) (h2 : β ≃* γ) : (α ≃* γ) :=
-{ hom := is_mul_hom.comp _ _,
-  ..equiv.trans h1.to_equiv h2.to_equiv }
+@[simp] theorem to_equiv_symm (f : α ≃+ β) : f.symm.to_equiv = f.to_equiv.symm := rfl
 
+attribute [to_additive add_equiv.to_equiv_symm] mul_equiv.to_equiv_symm
+
+/-- Transitivity of addition-preserving isomorphisms -/
+@[trans] def trans (h1 : α ≃+ β) (h2 : β ≃+ γ) : (α ≃+ γ) :=
+{ map_add' := λ x y, show h2 (h1 (x + y)) = h2 (h1 x) + h2 (h1 y),
+    by rw [h1.map_add, h2.map_add],
+  ..h1.to_equiv.trans h2.to_equiv }
+
+attribute [to_additive add_equiv.trans] mul_equiv.trans
 attribute [to_additive add_equiv.trans._proof_1] mul_equiv.trans._proof_1
 attribute [to_additive add_equiv.trans._proof_2] mul_equiv.trans._proof_2
 attribute [to_additive add_equiv.trans._proof_3] mul_equiv.trans._proof_3
-attribute [to_additive add_equiv.trans] mul_equiv.trans
+attribute [to_additive add_equiv.trans.equations._eqn_1] mul_equiv.trans.equations._eqn_1
 
-end mul_equiv
+/-- e.right_inv in canonical form -/
+def apply_symm_apply (e : α ≃+ β) : ∀ (y : β), e (e.symm y) = y :=
+equiv.apply_symm_apply (e.to_equiv)
+
+attribute [to_additive add_equiv.apply_symm_apply] mul_equiv.apply_symm_apply
+attribute [to_additive add_equiv.apply_symm_apply.equations._eqn_1] mul_equiv.apply_symm_apply.equations._eqn_1
+
+/-- e.left_inv in canonical form -/
+def symm_apply_apply (e : α ≃+ β) : ∀ (x : α), e.symm (e x) = x :=
+equiv.symm_apply_apply (e.to_equiv)
+
+attribute [to_additive add_equiv.symm_apply_apply] mul_equiv.symm_apply_apply
+attribute [to_additive add_equiv.symm_apply_apply.equations._eqn_1] mul_equiv.symm_apply_apply.equations._eqn_1
+
+/-- an additive equiv of monoids sends 0 to 0 (and is hence an  `add_monoid` isomorphism) -/
+def map_zero {α β} [add_monoid α] [add_monoid β] (h : α ≃+ β) : h 0 = 0 :=
+by rw [←add_zero (h 0), ←h.apply_symm_apply 0, ←h.map_add, zero_add]
+
+attribute [to_additive add_equiv.map_zero] mul_equiv.map_one
+attribute [to_additive add_equiv.map_zero.equations._eqn_1] mul_equiv.map_one.equations._eqn_1
+
+/-- An additive bijection between two add_monoids is an isomorphism. -/
+def to_add_monoid_hom {α β} [add_monoid α] [add_monoid β] (h : α ≃+ β) : (α →+ β) :=
+{ to_fun := h,
+  map_add' := h.map_add,
+  map_zero' := h.map_zero }
+
+attribute [to_additive add_equiv.to_add_monoid_hom] mul_equiv.to_monoid_hom
+attribute [to_additive add_equiv.to_add_monoid_hom._proof_1] mul_equiv.to_monoid_hom._proof_1
+attribute [to_additive add_equiv.to_add_monoid_hom.equations._eqn_1]
+  mul_equiv.to_monoid_hom.equations._eqn_1
+
+/-- an additive bijection between two add_monoids is an add_monoid hom
+(deprecated -- use to_add_monoid_hom) -/
+instance is_add_monoid_hom {α β} [add_monoid α] [add_monoid β] (h : α ≃+ β) : is_add_monoid_hom h :=
+⟨h.map_zero⟩
+
+attribute [to_additive add_equiv.is_add_monoid_hom] mul_equiv.is_monoid_hom
+attribute [to_additive add_equiv.is_add_monoid_hom.equations._eqn_1]
+  mul_equiv.is_monoid_hom.equations._eqn_1
+
+/-- An additive bijection between two add_groups is an add_group hom
+  (deprecated -- use to_monoid_hom). -/
+instance is_add_group_hom {α β} [add_group α] [add_group β] (h : α ≃+ β) :
+  is_add_group_hom h := { map_add := h.map_add }
 
--- equiv of monoids
-@[to_additive add_equiv.is_add_monoid_hom]
-instance mul_equiv.is_monoid_hom [monoid α] [monoid β] (h : α ≃* β) : is_monoid_hom h.to_equiv :=
-{ map_one := by rw [← mul_one (h.to_equiv 1), ← h.to_equiv.apply_symm_apply 1,
-                    ← is_mul_hom.map_mul h.to_equiv, one_mul] }
+attribute [to_additive add_equiv.is_add_group_hom] mul_equiv.is_group_hom
+attribute [to_additive add_equiv.is_add_group_hom.equations._eqn_1]
+  mul_equiv.is_group_hom.equations._eqn_1
 
--- equiv of groups
-@[to_additive add_equiv.is_add_group_hom]
-instance mul_equiv.is_group_hom [group α] [group β] (h : α ≃* β) :
-  is_group_hom h.to_equiv := { ..h.hom }
+end add_equiv
 
 namespace units
 
@@ -265,11 +434,11 @@ variables [monoid α] [monoid β] [monoid γ]
 (f : α → β) (g : β → γ) [is_monoid_hom f] [is_monoid_hom g]
 
 def map_equiv (h : α ≃* β) : units α ≃* units β :=
-{ to_fun := map h.to_equiv,
-  inv_fun := map h.symm.to_equiv,
+{ to_fun := map h,
+  inv_fun := map h.symm,
   left_inv := λ u, ext $ h.left_inv u,
   right_inv := λ u, ext $ h.right_inv u,
-  hom := ⟨λ a b, units.ext $ is_mul_hom.map_mul h.to_equiv a b⟩}
+  map_mul' := λ a b, units.ext $ h.map_mul a b}
 
 end units
 
@@ -283,23 +452,26 @@ namespace ring_equiv
 variables [ring α] [ring β] [ring γ]
 
 instance (h : α ≃r β) : is_ring_hom h.to_equiv := h.hom
+instance ring_equiv.is_ring_hom' (h : α ≃r β) : is_ring_hom h.to_fun := h.hom
 
 def to_mul_equiv (e : α ≃r β) : α ≃* β :=
-{ hom := by apply_instance, .. e.to_equiv }
+{ map_mul' := e.hom.map_mul, .. e.to_equiv }
 
 def to_add_equiv (e : α ≃r β) : α ≃+ β :=
-{ hom := by apply_instance, .. e.to_equiv }
+{ map_add' := e.hom.map_add, .. e.to_equiv }
 
 protected def refl (α : Type*) [ring α] : α ≃r α :=
 { hom := is_ring_hom.id, .. equiv.refl α }
 
 protected def symm {α β : Type*} [ring α] [ring β] (e : α ≃r β) : β ≃r α :=
-{ hom := { .. e.to_mul_equiv.symm.is_monoid_hom, .. e.to_add_equiv.symm.hom },
+{ hom := { map_one := e.to_mul_equiv.symm.map_one,
+           map_mul := e.to_mul_equiv.symm.map_mul,
+           map_add := e.to_add_equiv.symm.map_add },
   .. e.to_equiv.symm }
 
 protected def trans {α β γ : Type*} [ring α] [ring β] [ring γ]
   (e₁ : α ≃r β) (e₂ : β ≃r γ) : α ≃r γ :=
-{ hom := is_ring_hom.comp _ _, .. e₁.1.trans e₂.1  }
+{ hom := is_ring_hom.comp _ _, .. e₁.to_equiv.trans e₂.to_equiv  }
 
 instance symm.is_ring_hom {e : α ≃r β} : is_ring_hom e.to_equiv.symm := hom e.symm
 
diff --git a/src/data/mv_polynomial.lean b/src/data/mv_polynomial.lean
index 146ece5a09575..968658559c2c9 100644
--- a/src/data/mv_polynomial.lean
+++ b/src/data/mv_polynomial.lean
@@ -983,14 +983,14 @@ def ring_equiv_of_equiv (e : β ≃ γ) : mv_polynomial β α ≃r mv_polynomial
   hom       := rename.is_ring_hom e }
 
 def ring_equiv_congr [comm_ring γ] (e : α ≃r γ) : mv_polynomial β α ≃r mv_polynomial β γ :=
-{ to_fun    := map e.to_fun,
-  inv_fun   := map e.symm.to_fun,
+{ to_fun    := map e.to_equiv,
+  inv_fun   := map e.symm.to_equiv,
   left_inv  := assume p,
-    have (e.symm.to_equiv.to_fun ∘ e.to_equiv.to_fun) = id,
+    have (e.symm.to_equiv ∘ e.to_equiv) = id,
     { ext a, exact e.to_equiv.symm_apply_apply a },
     by simp only [map_map, this, map_id],
   right_inv := assume p,
-    have (e.to_equiv.to_fun ∘ e.symm.to_equiv.to_fun) = id,
+    have (e.to_equiv ∘ e.symm.to_equiv) = id,
     { ext a, exact e.to_equiv.apply_symm_apply a },
     by simp only [map_map, this, map_id],
   hom       := map.is_ring_hom e.to_fun }
diff --git a/src/linear_algebra/basic.lean b/src/linear_algebra/basic.lean
index 12943f21f841a..9a638bdbdfb76 100644
--- a/src/linear_algebra/basic.lean
+++ b/src/linear_algebra/basic.lean
@@ -1587,7 +1587,7 @@ def general_linear_equiv : general_linear_group α β ≃* (β ≃ₗ[α] β) :=
     cases f,
     congr
   end,
-  hom := ⟨λ x y, by {ext, refl}⟩ }
+  map_mul' := λ x y, by {ext, refl} }
 
 @[simp] lemma general_linear_equiv_to_linear_map (f : general_linear_group α β) :
   ((general_linear_equiv α β).to_equiv f).to_linear_map = f.val :=
diff --git a/src/ring_theory/free_comm_ring.lean b/src/ring_theory/free_comm_ring.lean
index 231bb3e87aaa2..1ad9d0b3cd762 100644
--- a/src/ring_theory/free_comm_ring.lean
+++ b/src/ring_theory/free_comm_ring.lean
@@ -265,21 +265,21 @@ end
 
 def subsingleton_equiv_free_comm_ring [subsingleton α] :
   free_ring α ≃r free_comm_ring α :=
-{ to_equiv := @functor.map_equiv _ _ free_abelian_group _ _ $ multiset.subsingleton_equiv α,
-  hom :=
+{ hom :=
   begin
     delta functor.map_equiv,
     rw congr_arg is_ring_hom _,
     work_on_goal 2 { symmetry, exact coe_eq α },
     apply_instance
-  end }
+  end,
+  ..@functor.map_equiv _ _ free_abelian_group _ _ $ multiset.subsingleton_equiv α }
 
 instance [subsingleton α] : comm_ring (free_ring α) :=
 { mul_comm := λ x y,
   by rw [← (subsingleton_equiv_free_comm_ring α).left_inv (y * x),
-        is_ring_hom.map_mul ((subsingleton_equiv_free_comm_ring α).to_equiv).to_fun,
+        is_ring_hom.map_mul ((subsingleton_equiv_free_comm_ring α)).to_fun,
         mul_comm,
-        ← is_ring_hom.map_mul ((subsingleton_equiv_free_comm_ring α).to_equiv).to_fun,
+        ← is_ring_hom.map_mul ((subsingleton_equiv_free_comm_ring α)).to_fun,
         (subsingleton_equiv_free_comm_ring α).left_inv],
   .. free_ring.ring α }
 
diff --git a/src/ring_theory/noetherian.lean b/src/ring_theory/noetherian.lean
index 7e2808abeb46c..92f80a60f82b1 100644
--- a/src/ring_theory/noetherian.lean
+++ b/src/ring_theory/noetherian.lean
@@ -393,7 +393,7 @@ instance is_noetherian_ring_range {R} [comm_ring R] {S} [comm_ring S] (f : R →
 
 theorem is_noetherian_ring_of_ring_equiv (R) [comm_ring R] {S} [comm_ring S]
   (f : R ≃r S) [is_noetherian_ring R] : is_noetherian_ring S :=
-is_noetherian_ring_of_surjective R S f.1 f.1.surjective
+is_noetherian_ring_of_surjective R S f.1 f.to_equiv.surjective
 
 namespace is_noetherian_ring