diff --git a/library/init/category/cont.lean b/library/init/category/cont.lean
index 673221dc9e..4f5f692e4c 100644
--- a/library/init/category/cont.lean
+++ b/library/init/category/cont.lean
@@ -10,33 +10,33 @@ prelude
 import init.category.alternative init.category.combinators init.category.lift
 universes u v w
 
-structure cont_t (r : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
-(run : (α → m r) → m r)
+structure cont_t (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+(run : (α → m ρ) → m ρ)
 
 attribute [pp_using_anonymous_constructor] cont_t
 
 class monad_cont (m : Type u → Type v) :=
 (call_cc {α β : Type u} : ((α → m β) → m α) → m α)
 
-@[reducible] def cont (r α : Type u) : Type u := cont_t r id α
+@[reducible] def cont (ρ α : Type u) : Type u := cont_t ρ id α
 
 namespace cont_t
 section
-  parameters {r : Type u} {m : Type u → Type v}
+  parameters {ρ : Type u} {m : Type u → Type v}
 
-  protected def pure {α : Type u} (a : α) : cont_t r m α :=
+  protected def pure {α : Type u} (a : α) : cont_t ρ m α :=
   ⟨λ cc, cc a⟩
 
-  protected def bind {α β : Type u} (ma : cont_t r m α) (f : α → cont_t r m β) : cont_t r m β :=
+  protected def bind {α β : Type u} (ma : cont_t ρ m α) (f : α → cont_t ρ m β) : cont_t ρ m β :=
   ⟨λ cc, ma.run (λ a, (f a).run cc)⟩
 
-  instance : monad (cont_t r m) :=
+  instance : monad (cont_t ρ m) :=
   { pure := @pure, bind := @bind }
 
-  protected def call_cc {α β : Type u} (f : (α → cont_t r m β) → cont_t r m α) : cont_t r m α :=
+  protected def call_cc {α β : Type u} (f : (α → cont_t ρ m β) → cont_t ρ m α) : cont_t ρ m α :=
   ⟨λ cc, (f (λ a, ⟨λ _, cc a⟩)).run cc⟩
 
-  instance : monad_cont (cont_t r m) :=
+  instance : monad_cont (cont_t ρ m) :=
   ⟨@call_cc⟩
 end
 end cont_t
diff --git a/library/init/category/lawful.lean b/library/init/category/lawful.lean
index b1896ff171..de6d5ab000 100644
--- a/library/init/category/lawful.lean
+++ b/library/init/category/lawful.lean
@@ -173,51 +173,51 @@ instance (m : Type u → Type v) [monad m] [is_lawful_monad m] (ε : Type u) : i
 
 namespace reader_t
 section
-  variable  {r : Type u}
+  variable  {ρ : Type u}
   variable  {m : Type u → Type v}
   variables {α β : Type u}
-  variables (x : reader_t r m α) (cfg : r)
+  variables (x : reader_t ρ m α) (r : ρ)
 
-  lemma ext {x x' : reader_t r m α} (h : ∀ cfg, x.run cfg = x'.run cfg) : x = x' :=
+  lemma ext {x x' : reader_t ρ m α} (h : ∀ r, x.run r = x'.run r) : x = x' :=
   by cases x; cases x'; simp [show x = x', from funext h]
 
   variable  [monad m]
 
-  @[simp] lemma run_pure (a) : (pure a : reader_t r m α).run cfg = pure a := rfl
-  @[simp] lemma run_bind (f : α → reader_t r m β) :
-    (x >>= f).run cfg = x.run cfg >>= λ a, (f a).run cfg := rfl
-  @[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run cfg = f <$> x.run cfg :=
+  @[simp] lemma run_pure (a) : (pure a : reader_t ρ m α).run r = pure a := rfl
+  @[simp] lemma run_bind (f : α → reader_t ρ m β) :
+    (x >>= f).run r = x.run r >>= λ a, (f a).run r := rfl
+  @[simp] lemma run_map (f : α → β) [is_lawful_monad m] : (f <$> x).run r = f <$> x.run r :=
   by rw ←bind_pure_comp_eq_map m; refl
   @[simp] lemma run_monad_lift {n} [has_monad_lift_t n m] (x : n α) :
-    (monad_lift x : reader_t r m α).run cfg = (monad_lift x : m α) := rfl
+    (monad_lift x : reader_t ρ m α).run r = (monad_lift x : m α) := rfl
   @[simp] lemma run_monad_map {m' n n'} [monad m'] [monad_functor_t n n' m m'] (f : ∀ {α}, n α → n' α) :
-    (monad_map @f x : reader_t r m' α).run cfg = monad_map @f (x.run cfg) := rfl
-  @[simp] lemma run_read : (reader_t.read : reader_t r m r).run cfg = pure cfg := rfl
+    (monad_map @f x : reader_t ρ m' α).run r = monad_map @f (x.run r) := rfl
+  @[simp] lemma run_read : (reader_t.read : reader_t ρ m ρ).run r = pure r := rfl
 end
 end reader_t
 
-instance (r : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] : is_lawful_monad (reader_t r m) :=
+instance (ρ : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] : is_lawful_monad (reader_t ρ m) :=
 { id_map := by intros; apply reader_t.ext; intro; simp,
   pure_bind := by intros; apply reader_t.ext; intro; simp,
   bind_assoc := by intros; apply reader_t.ext; intro; simp [bind_assoc] }
 
 
 namespace cont_t
-  variable  {r : Type u}
+  variable  {ρ : Type u}
   variable  {m : Type u → Type v}
   variables {α β : Type u}
-  variables (x : cont_t r m α)
+  variables (x : cont_t ρ m α)
 
-  lemma ext {x x' : cont_t r m α} (h : ∀ cc, x.run cc = x'.run cc) : x = x' :=
+  lemma ext {x x' : cont_t ρ m α} (h : ∀ cc, x.run cc = x'.run cc) : x = x' :=
   by cases x; cases x'; simp [show x = x', from funext h]
 
-  @[simp] lemma run_pure (a : α) (cc : α → m r) : (pure a : cont_t r m α).run cc = cc a := rfl
-  @[simp] lemma run_bind (f : α → cont_t r m β) (cc : β → m r) :
+  @[simp] lemma run_pure (a : α) (cc : α → m ρ) : (pure a : cont_t ρ m α).run cc = cc a := rfl
+  @[simp] lemma run_bind (f : α → cont_t ρ m β) (cc : β → m ρ) :
     (x >>= f).run cc = x.run (λ a, (f a).run cc) := rfl
-  @[simp] lemma run_map (f : α → β) (cc : β → m r) : (f <$> x).run cc = x.run (cc ∘ f) := rfl
+  @[simp] lemma run_map (f : α → β) (cc : β → m ρ) : (f <$> x).run cc = x.run (cc ∘ f) := rfl
 end cont_t
 
-instance (r : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] : is_lawful_monad (cont_t r m) :=
+instance (ρ : Type u) (m : Type u → Type v) [monad m] [is_lawful_monad m] : is_lawful_monad (cont_t ρ m) :=
 { id_map := by intros; apply cont_t.ext; simp,
   pure_bind := by intros; apply cont_t.ext; simp,
   bind_assoc := by intros; apply cont_t.ext; simp }
diff --git a/library/init/category/reader.lean b/library/init/category/reader.lean
index 945e81d9a1..e91ef9fe6c 100644
--- a/library/init/category/reader.lean
+++ b/library/init/category/reader.lean
@@ -10,38 +10,38 @@ prelude
 import init.category.lift init.category.id
 universes u v w
 
-structure reader_t (r : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
-(run : r → m α)
+structure reader_t (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
+(run : ρ → m α)
 
-@[reducible] def reader (r : Type u) := reader_t r id
+@[reducible] def reader (ρ : Type u) := reader_t ρ id
 
 attribute [pp_using_anonymous_constructor] reader_t
 
 namespace reader_t
 section
-  variable  {r : Type u}
+  variable  {ρ : Type u}
   variable  {m : Type u → Type v}
   variable  [monad m]
   variables {α β : Type u}
 
-  protected def read : reader_t r m r :=
+  protected def read : reader_t ρ m ρ :=
   ⟨pure⟩
 
-  protected def pure (a : α) : reader_t r m α :=
+  protected def pure (a : α) : reader_t ρ m α :=
   ⟨λ r, pure a⟩
 
-  protected def bind (x : reader_t r m α) (f : α → reader_t r m β) : reader_t r m β :=
+  protected def bind (x : reader_t ρ m α) (f : α → reader_t ρ m β) : reader_t ρ m β :=
   ⟨λ r, do a ← x.run r,
            (f a).run r⟩
 
-  instance : monad (reader_t r m) :=
+  instance : monad (reader_t ρ m) :=
   { pure := @reader_t.pure _ _ _, bind := @reader_t.bind _ _ _ }
 
-  protected def lift (a : m α) : reader_t r m α :=
+  protected def lift (a : m α) : reader_t ρ m α :=
   ⟨λ r, a⟩
 
-  instance (m) [monad m] : has_monad_lift m (reader_t r m) :=
-  ⟨@reader_t.lift r m _⟩
+  instance (m) [monad m] : has_monad_lift m (reader_t ρ m) :=
+  ⟨@reader_t.lift ρ m _⟩
 
   protected def monad_map {r m m'} [monad m] [monad m'] {α} (f : Π {α}, m α → m' α) : reader_t r m α → reader_t r m' α :=
   λ x, ⟨λ r, f (x.run r)⟩
@@ -52,31 +52,31 @@ end
 end reader_t
 
 
-/-- A specialization of `monad_lift` to `reader_t` that allows `r` to be inferred. -/
-class monad_reader_lift (r : out_param (Type u)) (m : out_param (Type u → Type v)) (n : Type u → Type w) :=
-[has_lift : has_monad_lift_t (reader_t r m) n]
+/-- A specialization of `monad_lift` to `reader_t` that allows `ρ` to be inferred. -/
+class monad_reader_lift (ρ : out_param (Type u)) (m : out_param (Type u → Type v)) (n : Type u → Type w) :=
+[has_lift : has_monad_lift_t (reader_t ρ m) n]
 
 attribute [instance] monad_reader_lift.mk
 local attribute [instance] monad_reader_lift.has_lift
 
-def monad_reader_lift.read {r : Type u} {m : Type u → Type v} {n : Type u → Type w} [monad m] [monad_reader_lift r m n] : n r :=
-@monad_lift _ _ _ _ (reader_t.read : reader_t r m _)
+def monad_reader_lift.read {ρ : Type u} {m : Type u → Type v} {n : Type u → Type w} [monad m] [monad_reader_lift ρ m n] : n ρ :=
+@monad_lift _ _ _ _ (reader_t.read : reader_t ρ m _)
 export monad_reader_lift (read)
 
 
 /-- A specialization of `monad_map` to `reader_t` that allows `r` to be inferred. -/
-class monad_reader_functor (r r' : out_param (Type u)) (m : out_param (Type u → Type v)) (n n' : Type u → Type w) :=
-[functor {} : monad_functor_t (reader_t r m) (reader_t r' m) n n']
+class monad_reader_functor (ρ ρ' : out_param (Type u)) (m : out_param (Type u → Type v)) (n n' : Type u → Type w) :=
+[functor {} : monad_functor_t (reader_t ρ m) (reader_t ρ' m) n n']
 
 attribute [instance] monad_reader_functor.mk
 local attribute [instance] monad_reader_functor.functor
 
-def with_reader_t {r r' m} [monad m] {α} (f : r' → r) : reader_t r m α → reader_t r' m α :=
+def with_reader_t {ρ ρ' m} [monad m] {α} (f : ρ' → ρ) : reader_t ρ m α → reader_t ρ' m α :=
 λ x, ⟨λ r, x.run (f r)⟩
 
-def with_reader {r r'} {m n n'} [monad m] [monad_reader_functor r r' m n n'] {α : Type u} (f : r' → r) : n α → n' α :=
-monad_map $ λ α, (with_reader_t f : reader_t r m α → reader_t r' m α)
+def with_reader {ρ ρ'} {m n n'} [monad m] [monad_reader_functor ρ ρ' m n n'] {α : Type u} (f : ρ' → ρ) : n α → n' α :=
+monad_map $ λ α, (with_reader_t f : reader_t ρ m α → reader_t ρ' m α)
 
 
-instance (r : Type u) (m out) [monad_run out m] : monad_run (λ α, r → out α) (reader_t r m) :=
+instance (ρ : Type u) (m out) [monad_run out m] : monad_run (λ α, ρ → out α) (reader_t ρ m) :=
 ⟨λ α x, run ∘ x.run, λ α a, reader_t.mk (unrun ∘ a)⟩