diff --git a/src/algebra/group.lean b/src/algebra/group.lean
index 52678766decf2..4f5acace902ac 100644
--- a/src/algebra/group.lean
+++ b/src/algebra/group.lean
@@ -354,6 +354,32 @@ instance [add_monoid α] : monoid (multiplicative α) :=
   mul_one := @add_zero _ _,
   ..multiplicative.semigroup }
 
+def free_monoid (α) := list α
+
+instance {α} : monoid (free_monoid α) :=
+{ one := [],
+  mul := λ x y, (x ++ y : list α),
+  mul_one := by intros; apply list.append_nil,
+  one_mul := by intros; refl,
+  mul_assoc := by intros; apply list.append_assoc }
+
+@[simp] lemma free_monoid.one_def {α} : (1 : free_monoid α) = [] := rfl
+
+@[simp] lemma free_monoid.mul_def {α} (xs ys : list α) : (xs * ys : free_monoid α) = (xs ++ ys : list α) := rfl
+
+def free_add_monoid (α) := list α
+
+instance {α} : add_monoid (free_add_monoid α) :=
+{ zero := [],
+  add := λ x y, (x ++ y : list α),
+  add_zero := by intros; apply list.append_nil,
+  zero_add := by intros; refl,
+  add_assoc := by intros; apply list.append_assoc }
+
+@[simp] lemma free_add_monoid.zero_def {α} : (1 : free_monoid α) = [] := rfl
+
+@[simp] lemma free_add_monoid.add_def {α} (xs ys : list α) : (xs * ys : free_monoid α) = (xs ++ ys : list α) := rfl
+
 section monoid
   variables [monoid α] {a b c : α}
 
diff --git a/src/category/applicative.lean b/src/category/applicative.lean
index ce1af4d2be140..1942cbc3bf703 100644
--- a/src/category/applicative.lean
+++ b/src/category/applicative.lean
@@ -55,40 +55,6 @@ end lemmas
 instance : is_comm_applicative id :=
 by refine { .. }; intros; refl
 
-namespace const
-open functor
-variables {γ : Type u} [monoid γ]
-
-protected def pure {α} (x : α) : const γ α := (1 : γ)
-protected def seq {α β : Type*} (f : const γ (α → β)) (x : const γ α) : const γ β :=
-(f * x : γ)
-
-instance : applicative (const γ) :=
-{ pure := @const.pure γ _,
-  seq := @const.seq γ _ }
-
-instance : is_lawful_applicative (const γ) :=
-by refine { .. }; intros; simp! [const.seq,const.pure,mul_assoc]
-
-end const
-
-namespace add_const
-open functor
-variables {γ : Type u} [add_monoid γ]
-
-protected def pure {α} (x : α) : add_const γ α := (0 : γ)
-protected def seq {α β : Type*} (f : add_const γ (α → β)) (x : add_const γ α) : add_const γ β :=
-(f + x : γ)
-
-instance : applicative (add_const γ) :=
-{ pure := @add_const.pure γ _,
-  seq  := @add_const.seq γ _ }
-
-instance : is_lawful_applicative (add_const γ) :=
-by refine { .. }; intros; simp! [add_const.seq,add_const.pure,add_assoc]
-
-end add_const
-
 namespace comp
 
 open function (hiding comp)
@@ -175,3 +141,17 @@ lemma comp.seq_mk {α β : Type w}
   [applicative f] [applicative g]
   (h : f (g (α → β))) (x : f (g α)) :
   comp.mk h <*> comp.mk x = comp.mk (has_seq.seq <$> h <*> x) := rfl
+
+instance {α} [has_one α] [has_mul α] : applicative (const α) :=
+{ pure := λ β x, (1 : α),
+  seq := λ β γ f x, (f * x : α) }
+
+instance {α} [monoid α] : is_lawful_applicative (const α) :=
+by refine { .. }; intros; simp [mul_assoc]
+
+instance {α} [has_zero α] [has_add α] : applicative (add_const α) :=
+{ pure := λ β x, (0 : α),
+  seq := λ β γ f x, (f + x : α) }
+
+instance {α} [add_monoid α] : is_lawful_applicative (add_const α) :=
+by refine { .. }; intros; simp
diff --git a/src/category/basic.lean b/src/category/basic.lean
index 462da0fe0709c..6e21de270f4f8 100644
--- a/src/category/basic.lean
+++ b/src/category/basic.lean
@@ -73,6 +73,8 @@ by simp [(pure_seq_eq_map _ _).symm]; simp [seq_assoc]
 end applicative
 
 -- TODO: setup `functor_norm` for `monad` laws
+attribute [functor_norm] pure_bind bind_assoc bind_pure
+
 section monad
 variables {m : Type u → Type v} [monad m] [is_lawful_monad m]
 
@@ -95,6 +97,24 @@ by rw [← bind_pure_comp_eq_map, bind_assoc]; simp [pure_bind]
 lemma seq_eq_bind_map {x : m α} {f : m (α → β)} : f <*> x = (f >>= (<$> x)) :=
 (bind_map_eq_seq m f x).symm
 
+/-- This is the Kleisli composition -/
+@[reducible] def pipe {m} [monad m] {α β γ} (f : α → m β) (g : β → m γ) := λ x, f x >>= g
+
+infix ` >=> `:55 := pipe
+
+@[functor_norm]
+lemma pipe_pure {α β} (f : α → m β) : f >=> pure = f :=
+by simp only [(>=>)] with functor_norm
+
+@[functor_norm]
+lemma pure_pipe {α β} (f : α → m β) : pure >=> f = f :=
+by simp only [(>=>)] with functor_norm
+
+@[functor_norm]
+lemma pipe_assoc {α β γ φ} (f : α → m β) (g : β → m γ) (h : γ → m φ) :
+  (f >=> g) >=> h = f >=> (g >=> h) :=
+by simp only [(>=>)] with functor_norm
+
 variables {β' γ' : Type v}
 variables {m' : Type v → Type w} [monad m']
 
diff --git a/src/category/functor.lean b/src/category/functor.lean
index c3c6d74faf145..703386168e6ce 100644
--- a/src/category/functor.lean
+++ b/src/category/functor.lean
@@ -43,10 +43,11 @@ def id.mk {α : Sort u} : α → id α := id
 namespace functor
 
 def const (α : Type*) (β : Type*) := α
-def add_const (α : Type*) := const α
 
 @[pattern] def const.mk {α β} (x : α) : const α β := x
 
+def const.mk' {α} (x : α) : const α punit := x
+
 def const.run {α β} (x : const α β) : α := x
 
 namespace const
@@ -57,17 +58,25 @@ protected def map {γ α β} (f : α → β) (x : const γ β) : const γ α :=
 
 instance {γ} : functor (const γ) :=
 { map := @const.map γ }
-instance add_const.functor {γ} : functor (add_const γ) :=
-@const.functor γ
 
 instance {γ} : is_lawful_functor (const γ) :=
 by constructor; intros; refl
 
+end const
+
+def add_const (α : Type*) := const α
+
+@[pattern]
+def add_const.mk {α β} (x : α) : add_const α β := x
+
+def add_const.run {α β} : add_const α β → α := id
+
+instance add_const.functor {γ} : functor (add_const γ) :=
+@const.functor γ
+
 instance add_const.is_lawful_functor {γ} : is_lawful_functor (add_const γ) :=
 @const.is_lawful_functor γ
 
-end const
-
 /-- `functor.comp` is a wrapper around `function.comp` for types.
     It prevents Lean's type class resolution mechanism from trying
     a `functor (comp F id)` when `functor F` would do. -/
diff --git a/src/category/traversable/basic.lean b/src/category/traversable/basic.lean
index 5a59b9592f5dd..f96ea77d9d744 100644
--- a/src/category/traversable/basic.lean
+++ b/src/category/traversable/basic.lean
@@ -20,9 +20,9 @@ variables (F : Type u → Type v) [applicative F] [is_lawful_applicative F]
 variables (G : Type u → Type w) [applicative G] [is_lawful_applicative G]
 
 structure applicative_transformation : Type (max (u+1) v w) :=
-(app : ∀ {α : Type u}, F α → G α)
-(preserves_pure' : ∀ {α : Type u} (x : α), app (pure x) = pure x)
-(preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app (x <*> y) = app x <*> app y)
+(app : ∀ α : Type u, F α → G α)
+(preserves_pure' : ∀ {α : Type u} (x : α), app _ (pure x) = pure x)
+(preserves_seq' : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app _ (x <*> y) = app _ x <*> app _ y)
 
 end applicative_transformation
 
@@ -31,7 +31,9 @@ namespace applicative_transformation
 variables (F : Type u → Type v) [applicative F] [is_lawful_applicative F]
 variables (G : Type u → Type w) [applicative G] [is_lawful_applicative G]
 
-instance : has_coe_to_fun (applicative_transformation F G) := ⟨_, λ m, m.app⟩
+instance : has_coe_to_fun (applicative_transformation F G) :=
+{ F := λ _, Π {α}, F α → G α,
+  coe := λ a, a.app }
 
 variables {F G}
 variables (η : applicative_transformation F G)
diff --git a/src/category_theory/category.lean b/src/category_theory/category.lean
index 28fdd15b5e50f..1f7de377e9057 100644
--- a/src/category_theory/category.lean
+++ b/src/category_theory/category.lean
@@ -36,25 +36,29 @@ def_replacer obviously
 class has_hom (obj : Type u) : Type (max u (v+1)) :=
 (hom : obj → obj → Type v)
 
-infixr ` ⟶ `:10 := has_hom.hom -- type as \h
+class category_struct (obj : Type u)
+extends has_hom.{v} obj :=
+(id       : Π X : obj, hom X X)
+(comp     : Π {X Y Z : obj}, hom X Y → hom Y Z → hom X Z)
+(notation `𝟙` := id)
+(infixr ` ≫ `:80 := comp)
 
 /--
 The typeclass `category C` describes morphisms associated to objects of type `C`.
 The universe levels of the objects and morphisms are unconstrained, and will often need to be
 specified explicitly, as `category.{v} C`. (See also `large_category` and `small_category`.)
 -/
-class category (obj : Type u) extends has_hom.{v} obj : Type (max u (v+1)) :=
-(id       : Π X : obj, X ⟶ X)
-(notation `𝟙` := id)
-(comp     : Π {X Y Z : obj}, (X ⟶ Y) → (Y ⟶ Z) → (X ⟶ Z))
-(infixr ` ≫ `:80 := comp)
-(id_comp' : ∀ {X Y : obj} (f : X ⟶ Y), 𝟙 X ≫ f = f . obviously)
-(comp_id' : ∀ {X Y : obj} (f : X ⟶ Y), f ≫ 𝟙 Y = f . obviously)
-(assoc'   : ∀ {W X Y Z : obj} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z),
-  (f ≫ g) ≫ h = f ≫ (g ≫ h) . obviously)
-
-notation `𝟙` := category.id -- type as \b1
-infixr ` ≫ `:80 := category.comp -- type as \gg
+class category (obj : Type u)
+extends category_struct.{v} obj :=
+(infixr ` ⟶ `:10 := hom)
+(id_comp' : ∀ {X Y : obj} (f : hom X Y), comp (id X) f = f . obviously)
+(comp_id' : ∀ {X Y : obj} (f : hom X Y), comp f (id Y) = f . obviously)
+(assoc'   : ∀ {W X Y Z : obj} (f : hom W X) (g : hom X Y) (h : hom Y Z),
+  comp (comp f g) h = comp f (comp g h) . obviously)
+
+notation `𝟙` := category_struct.id -- type as \b1
+infixr ` ≫ `:80 := category_struct.comp -- type as \gg
+infixr ` ⟶ `:10 := has_hom.hom -- type as \h
 
 -- `restate_axiom` is a command that creates a lemma from a structure field,
 -- discarding any auto_param wrappers from the type.
@@ -63,7 +67,7 @@ restate_axiom category.id_comp'
 restate_axiom category.comp_id'
 restate_axiom category.assoc'
 attribute [simp] category.id_comp category.comp_id category.assoc
-attribute [trans] category.comp
+attribute [trans] category_struct.comp
 
 lemma category.assoc_symm {C : Type u} [category.{v} C] {W X Y Z : C} (f : W ⟶ X) (g : X ⟶ Y) (h : Y ⟶ Z) :
   f ≫ (g ≫ h) = (f ≫ g) ≫ h :=
@@ -118,12 +122,19 @@ instance [preorder α] : small_category α :=
   comp := λ X Y Z f g, ⟨ ⟨ le_trans f.down.down g.down.down ⟩ ⟩ }
 
 section
-variables {C : Type u} [𝒞 : category.{v} C]
-include 𝒞
+variables {C : Type u}
+
+def End [category_struct.{v} C] (X : C) := X ⟶ X
+
+instance End.has_one [category_struct.{v} C] {X : C} : has_one (End X) := by refine { one := 𝟙 X }
+instance End.has_mul [category_struct.{v} C] {X : C} : has_mul (End X) := by refine { mul := λ x y, x ≫ y }
+instance End.monoid [category.{v} C] {X : C} : monoid (End X) :=
+by refine { .. End.has_one, .. End.has_mul, .. }; dsimp [has_mul.mul,has_one.one]; obviously
+
+@[simp] lemma End.one_def {C : Type u} [category_struct.{v} C] {X : C} : (1 : End X) = 𝟙 X := rfl
 
-def End (X : C) := X ⟶ X
+@[simp] lemma End.mul_def {C : Type u} [category_struct.{v} C] {X : C} (xs ys : End X) : xs * ys = xs ≫ ys := rfl
 
-instance {X : C} : monoid (End X) := by refine { one := 𝟙 X, mul := λ x y, x ≫ y, .. } ; obviously
 end
 
 end category_theory
diff --git a/src/category_theory/instances/kleisli.lean b/src/category_theory/instances/kleisli.lean
new file mode 100644
index 0000000000000..3f6b6d76fc833
--- /dev/null
+++ b/src/category_theory/instances/kleisli.lean
@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2018 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Simon Hudon
+
+The Kleisli construction on the Type category
+-/
+import category_theory.category
+
+universes u v
+
+namespace category_theory
+
+def Kleisli (m) [monad.{u v} m] := Type u
+
+def Kleisli.mk (m) [monad.{u v} m] (α : Type u) : Kleisli m := α
+
+instance Kleisli.category_struct {m} [monad m] : category_struct (Kleisli m) :=
+{ hom := λ α β, α → m β,
+  id := λ α x, (pure x : m α),
+  comp := λ X Y Z f g, f >=> g }
+
+instance Kleisli.category {m} [monad m] [is_lawful_monad m] : category (Kleisli m) :=
+by refine { hom := λ α β, α → m β,
+            id := λ α x, (pure x : m α),
+            comp := λ X Y Z f g, f >=> g,
+            id_comp' := _, comp_id' := _, assoc' := _ };
+   intros; ext; simp only [(>=>)] with functor_norm
+
+@[simp] lemma Kleisli.id_def {m} [monad m] [is_lawful_monad m] (α : Kleisli m) :
+  𝟙 α = @pure m _ α := rfl
+
+lemma Kleisli.comp_def {m} [monad m] [is_lawful_monad m] (α β γ : Kleisli m)
+  (xs : α ⟶ β) (ys : β ⟶ γ) (a : α) :
+  (xs ≫ ys) a = xs a >>= ys := rfl
+
+end category_theory
diff --git a/src/category_theory/instances/rings.lean b/src/category_theory/instances/rings.lean
index 078bac57a8973..65531aa87e628 100644
--- a/src/category_theory/instances/rings.lean
+++ b/src/category_theory/instances/rings.lean
@@ -7,7 +7,6 @@ Introduce CommRing -- the category of commutative rings.
 Currently only the basic setup.
 -/
 
-import category_theory.concrete_category
 import category_theory.instances.monoids
 import category_theory.fully_faithful
 import category_theory.adjunction
diff --git a/src/category_theory/natural_isomorphism.lean b/src/category_theory/natural_isomorphism.lean
index fd94b2030fd52..7fd5169b455f5 100644
--- a/src/category_theory/natural_isomorphism.lean
+++ b/src/category_theory/natural_isomorphism.lean
@@ -127,8 +127,8 @@ variables {C : Type u₁} [𝒞 : category.{v₁} C]
 include 𝒞
 
 def ulift_down_up : ulift_down.{v₁} C ⋙ ulift_up C ≅ functor.id (ulift.{u₂} C) :=
-{ hom := { app := λ X, @category.id (ulift.{u₂} C) _ X },
-  inv := { app := λ X, @category.id (ulift.{u₂} C) _ X } }
+{ hom := { app := λ X, @category_struct.id (ulift.{u₂} C) _ X },
+  inv := { app := λ X, @category_struct.id (ulift.{u₂} C) _ X } }
 
 def ulift_up_down : ulift_up.{v₁} C ⋙ ulift_down C ≅ functor.id C :=
 { hom := { app := λ X, 𝟙 X },
diff --git a/src/category_theory/opposites.lean b/src/category_theory/opposites.lean
index 41098f554577d..3f7d83c7630a6 100644
--- a/src/category_theory/opposites.lean
+++ b/src/category_theory/opposites.lean
@@ -47,6 +47,11 @@ attribute [irreducible] opposite
 @[simp] lemma unop_op (X : C) : unop (op X) = X := rfl
 @[simp] lemma op_unop (X : Cᵒᵖ) : op (unop X) = X := rfl
 
+lemma op_inj : function.injective (@op C) :=
+by { rintros _ _ ⟨ ⟩, refl }
+lemma unop_inj : function.injective (@unop C) :=
+by { rintros _ _ ⟨ ⟩, refl }
+
 section has_hom
 
 variables [𝒞 : has_hom.{v₁} C]
@@ -173,4 +178,27 @@ end
 
 end functor
 
+omit 𝒞
+
+instance opposite.has_one [has_one C] : has_one (Cᵒᵖ) :=
+{ one := op 1 }
+
+instance opposite.has_mul [has_mul C] : has_mul (Cᵒᵖ) :=
+{ mul := λ x y, op $ unop y * unop  x }
+
+@[simp] lemma opposite.unop_one [has_one C] : unop (1 : Cᵒᵖ) = (1 : C) := rfl
+
+@[simp] lemma opposite.unop_mul [has_mul C] (xs ys : Cᵒᵖ) : unop (xs * ys) = (unop ys * unop xs : C) := rfl
+
+@[simp] lemma opposite.op_one [has_one C] : op (1 : C) = 1 := rfl
+
+@[simp] lemma opposite.op_mul [has_mul C] (xs ys : C) : op (xs * ys) = (op ys * op xs) := rfl
+
+instance opposite.monoid [monoid C] : monoid (Cᵒᵖ) :=
+{ one := op 1,
+  mul := λ x y, op $ unop y * unop  x,
+  mul_one := by { intros, apply unop_inj, simp },
+  one_mul := by { intros, simp },
+  mul_assoc := by { intros, simp [mul_assoc], } }
+
 end category_theory
diff --git a/src/data/fintype.lean b/src/data/fintype.lean
index b4539a93b61bc..843784753f082 100644
--- a/src/data/fintype.lean
+++ b/src/data/fintype.lean
@@ -536,7 +536,7 @@ suffices f ∈ perms_of_list l ∨ ∃ (b : α), b ∈ l ∧ ∃ g : perm α, g
     if hffa : f (f a) = a then mem_of_ne_of_mem hfa (h _ (mt (λ h, f.bijective.1 h) hfa))
       else this _ $ by simp [mul_apply, swap_apply_def]; split_ifs; cc,
     ⟨swap a (f a) * f, mem_perms_of_list_of_mem this,
-      by rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← one_def, one_mul]⟩⟩)
+      by rw [← mul_assoc, mul_def (swap a (f a)) (swap a (f a)), swap_swap, ← equiv.perm.one_def, one_mul]⟩⟩)
 
 lemma mem_of_mem_perms_of_list : ∀ {l : list α} {f : perm α}, f ∈ perms_of_list l → ∀ {x}, f x ≠ x → x ∈ l
 | []     f h := have f = 1 := by simpa [perms_of_list] using h, by rw this; simp