diff --git a/library/data/equiv.lean b/library/data/equiv.lean
index 5d1abc0b9..1523df6e9 100644
--- a/library/data/equiv.lean
+++ b/library/data/equiv.lean
@@ -13,19 +13,31 @@ open function
 
 structure equiv [class] (A B : Type) :=
   (to_fun    : A → B)
-  (inv       : B → A)
-  (left_inv  : left_inverse inv to_fun)
-  (right_inv : right_inverse inv to_fun)
+  (inv_fun   : B → A)
+  (left_inv  : left_inverse inv_fun to_fun)
+  (right_inv : right_inverse inv_fun to_fun)
 
 namespace equiv
+definition perm [reducible] (A : Type) := equiv A A
+
 infix `≃`:50 := equiv
 
-namespace ops
-  attribute equiv.to_fun [coercion]
-  definition inverse [reducible] {A B : Type} [h : A ≃ B] : B → A :=
-  λ b, @equiv.inv A B h b
-  postfix `⁻¹` := inverse
-end ops
+definition fn {A B : Type} (e : equiv A B) : A → B :=
+@equiv.to_fun A B e
+
+infixr `∙`:100 := fn
+
+definition inv {A B : Type} [e : equiv A B] : B → A :=
+@equiv.inv_fun A B e
+
+lemma eq_of_to_fun_eq {A B : Type} : ∀ {e₁ e₂ : equiv A B}, fn e₁ = fn e₂ → e₁ = e₂
+| (mk f₁ g₁ l₁ r₁) (mk f₂ g₂ l₂ r₂) h :=
+  assert f₁ = f₂, from h,
+  assert g₁ = g₂, from funext (λ x,
+    assert f₁ (g₁ x) = f₂ (g₂ x), from eq.trans (r₁ x) (eq.symm (r₂ x)),
+    have f₁ (g₁ x) = f₁ (g₂ x),   by rewrite [-h at this]; exact this,
+    show g₁ x = g₂ x,             from injective_of_left_inverse l₁ this),
+  by congruence; repeat assumption
 
 protected definition refl [refl] (A : Type) : A ≃ A :=
 mk (@id A) (@id A) (λ x, rfl) (λ x, rfl)
@@ -39,6 +51,40 @@ protected definition trans [trans] {A B C : Type} : A ≃ B → B ≃ C → A 
    (show ∀ x, g₁ (g₂ (f₂ (f₁ x))) = x, by intros; rewrite [l₂, l₁]; reflexivity)
    (show ∀ x, f₂ (f₁ (g₁ (g₂ x))) = x, by intros; rewrite [r₁, r₂]; reflexivity)
 
+abbreviation id {A : Type} := equiv.refl A
+
+namespace ops
+  postfix `⁻¹` := equiv.symm
+  postfix `⁻¹` := equiv.inv
+  notation e₁ `∘` e₂  := equiv.trans e₂ e₁
+end ops
+open equiv.ops
+
+lemma id_apply {A : Type} (x : A) : id ∙ x = x :=
+rfl
+
+lemma compose_apply {A B C : Type} (g : B ≃ C) (f : A ≃ B) (x : A) : (g ∘ f) ∙ x = g ∙ f ∙ x :=
+begin cases g, cases f, esimp end
+
+lemma inverse_apply_apply {A B : Type} : ∀ (e : A ≃ B) (x : A), e⁻¹ ∙ e ∙ x = x
+| (mk f₁ g₁ l₁ r₁) x := begin unfold [equiv.symm, fn], rewrite l₁ end
+
+lemma eq_iff_eq_of_injective {A B : Type} {f : A → B} (inj : injective f) (a b : A) : f a = f b ↔ a = b :=
+iff.intro
+  (suppose f a = f b, inj this)
+  (suppose a = b,     by rewrite this)
+
+lemma apply_eq_iff_eq {A B : Type} : ∀ (f : A ≃ B) (x y : A), f ∙ x = f ∙ y ↔ x = y
+| (mk f₁ g₁ l₁ r₁) x y := eq_iff_eq_of_injective (injective_of_left_inverse l₁) x y
+
+lemma apply_eq_iff_eq_inverse_apply {A B : Type} : ∀ (f : A ≃ B) (x : A) (y : B), f ∙ x = y ↔ x = f⁻¹ ∙ y
+| (mk f₁ g₁ l₁ r₁) x y :=
+  begin
+    esimp, unfold [equiv.symm, fn], apply iff.intro,
+    suppose f₁ x = y, by subst y; rewrite l₁,
+    suppose x = g₁ y, by subst x; rewrite r₁
+  end
+
 definition false_equiv_empty : empty ≃ false :=
 mk (λ e, empty.rec _ e) (λ h, false.rec _ h) (λ e, empty.rec _ e) (λ h, false.rec _ h)
 
@@ -258,12 +304,81 @@ definition inhabited_of_equiv {A B : Type} [h : inhabited A] : A ≃ B → inhab
 
 section
 open subtype
-override equiv.ops
-definition subtype_equiv_of_subtype {A B : Type} {p : A → Prop} : A ≃ B → {a : A | p a} ≃ {b : B | p (b⁻¹)}
+definition subtype_equiv_of_subtype {A B : Type} {p : A → Prop} : A ≃ B → {a : A | p a} ≃ {b : B | p b⁻¹}
 | (mk f g l r) :=
   mk (λ s, match s with tag v h := tag (f v) (eq.rec_on (eq.symm (l v)) h) end)
      (λ s, match s with tag v h := tag (g v) (eq.rec_on (eq.symm (r v)) h) end)
      (λ s, begin cases s, esimp, congruence, rewrite l, reflexivity end)
      (λ s, begin cases s, esimp, congruence, rewrite r, reflexivity end)
 end
+
+section swap
+variable {A : Type}
+variable [h : decidable_eq A]
+include h
+open decidable
+
+definition swap_core (a b r : A) : A :=
+if r = a then b
+else if r = b then a
+else r
+
+lemma swap_core_swap_core (r a b : A) : swap_core a b (swap_core a b r) = r :=
+by_cases
+  (suppose r = a, by_cases
+    (suppose r = b,   begin unfold swap_core, rewrite [if_pos `r = a`, if_pos (eq.refl b), -`r = a`, -`r = b`, if_pos (eq.refl r)] end)
+    (suppose ¬ r = b,
+      assert b ≠ a, from assume h, begin rewrite h at this, contradiction end,
+      begin unfold swap_core, rewrite [*if_pos `r = a`, if_pos (eq.refl b), if_neg `b ≠ a`, `r = a`] end))
+  (suppose ¬ r = a, by_cases
+    (suppose r = b,   begin unfold swap_core, rewrite [if_neg `¬ r = a`, *if_pos `r = b`, if_pos (eq.refl a), this] end)
+    (suppose ¬ r = b, begin unfold swap_core, rewrite [*if_neg `¬ r = a`, *if_neg `¬ r = b`, if_neg `¬ r = a`] end))
+
+lemma swap_core_self (r a : A) : swap_core a a r = r :=
+by_cases
+  (suppose r = a, begin unfold swap_core, rewrite [*if_pos this, this] end)
+  (suppose r ≠ a, begin unfold swap_core, rewrite [*if_neg this] end)
+
+lemma swap_core_comm (r a b : A) : swap_core a b r = swap_core b a r :=
+by_cases
+  (suppose r = a, by_cases
+    (suppose r = b,   begin unfold swap_core, rewrite [if_pos `r = a`, if_pos `r = b`, -`r = a`, -`r = b`] end)
+    (suppose ¬ r = b, begin unfold swap_core, rewrite [*if_pos `r = a`, if_neg `¬ r = b`] end))
+  (suppose ¬ r = a, by_cases
+    (suppose r = b,   begin unfold swap_core, rewrite [if_neg `¬ r = a`, *if_pos `r = b`]    end)
+    (suppose ¬ r = b, begin unfold swap_core, rewrite [*if_neg `¬ r = a`, *if_neg `¬ r = b`] end))
+
+definition swap (a b : A) : perm A :=
+mk (swap_core a b)
+   (swap_core a b)
+   (λ x, abstract by rewrite swap_core_swap_core end)
+   (λ x, abstract by rewrite swap_core_swap_core end)
+
+lemma swap_self (a : A) : swap a a = id :=
+eq_of_to_fun_eq (funext (λ x, begin unfold [swap, fn], rewrite swap_core_self end))
+
+lemma swap_comm (a b : A) : swap a b = swap b a :=
+eq_of_to_fun_eq (funext (λ x, begin unfold [swap, fn], rewrite swap_core_comm end))
+
+lemma swap_apply_def (a b : A) (x : A) : swap a b ∙ x = if x = a then b else if x = b then a else x :=
+rfl
+
+lemma swap_apply_left (a b : A) : swap a b ∙ a = b :=
+if_pos rfl
+
+lemma swap_apply_right (a b : A) : swap a b ∙ b = a :=
+by_cases
+  (suppose b = a, by rewrite [swap_apply_def, this, *if_pos rfl])
+  (suppose b ≠ a, by rewrite [swap_apply_def, if_pos rfl, if_neg this])
+
+lemma swap_apply_of_ne_of_ne {a b : A} {x : A} : x ≠ a → x ≠ b → swap a b ∙ x = x :=
+assume h₁ h₂, by rewrite [swap_apply_def, if_neg h₁, if_neg h₂]
+
+lemma swap_swap (a b : A) : swap a b ∘ swap a b = id :=
+eq_of_to_fun_eq (funext (λ x, begin unfold [swap, fn, equiv.trans, equiv.refl], rewrite swap_core_swap_core end))
+
+lemma swap_compose_apply (a b : A) (π : perm A) (x : A) : (swap a b ∘ π) ∙ x = if π ∙ x = a then b else if π ∙ x = b then a else π ∙ x :=
+begin cases π, reflexivity end
+
+end swap
 end equiv
diff --git a/library/data/fin.lean b/library/data/fin.lean
index c1d718cdd..78f8f2970 100644
--- a/library/data/fin.lean
+++ b/library/data/fin.lean
@@ -374,15 +374,15 @@ open sum equiv decidable
 definition fin_zero_equiv_empty : fin 0 ≃ empty :=
 ⦃ equiv,
   to_fun    := λ f : (fin 0), elim0 f,
-  inv       := λ e : empty, empty.rec _ e,
+  inv_fun   := λ e : empty, empty.rec _ e,
   left_inv  := λ f : (fin 0), elim0 f,
   right_inv := λ e : empty, empty.rec _ e
 ⦄
 
 definition fin_one_equiv_unit : fin 1 ≃ unit :=
 ⦃ equiv,
-  to_fun := λ f : (fin 1), unit.star,
-  inv    := λ u : unit,    fin.zero 0,
+  to_fun  := λ f : (fin 1), unit.star,
+  inv_fun := λ u : unit,    fin.zero 0,
   left_inv := begin
     intro f, change mk 0 !zero_lt_succ = f, cases f with v h, congruence,
     have v +1 ≤ 1, from succ_le_of_lt h,
@@ -406,7 +406,7 @@ assert aux₁ : ∀ {v}, v < m → (v + n) < (n + m), from
     | sum.inl (mk v hlt) := mk v     (lt_add_of_lt_right hlt m)
     | sum.inr (mk v hlt) := mk (v+n) (aux₁ hlt)
     end,
-  inv := λ f : fin (n + m),
+  inv_fun := λ f : fin (n + m),
     match f with
     | mk v hlt := if h : v < n then sum.inl (mk v h) else sum.inr (mk (v-n) (sub_lt_of_lt_add hlt (le_of_not_gt h)))
     end,
@@ -444,7 +444,7 @@ assert aux₃ : ∀ {v}, v < n * m → v div n < m, from
   take v, assume h, by rewrite mul.comm at h; exact div_lt_of_lt_mul h,
 ⦃ equiv,
   to_fun   := λ p : (fin n × fin m), match p with (mk v₁ hlt₁, mk v₂ hlt₂) := mk (v₁ + v₂ * n) (aux₁ hlt₁ hlt₂) end,
-  inv      := λ f : fin (n*m), match f with (mk v hlt) := (mk (v mod n) (aux₂ v), mk (v div n) (aux₃ hlt)) end,
+  inv_fun  := λ f : fin (n*m), match f with (mk v hlt) := (mk (v mod n) (aux₂ v), mk (v div n) (aux₃ hlt)) end,
   left_inv := begin
     intro p, cases p with f₁ f₂, cases f₁ with v₁ hlt₁, cases f₂ with v₂ hlt₂, esimp,
     congruence,