diff --git a/library/algebra/category/adjoint.lean b/library/algebra/category/adjoint.lean
index 9036dcceb..b7ed5ffef 100644
--- a/library/algebra/category/adjoint.lean
+++ b/library/algebra/category/adjoint.lean
@@ -20,7 +20,7 @@ namespace adjoint
   --I'm lazy, waiting for automation to fill this
 
   section
-  parameters {obC obD : Type} (C : category obC) {D : category obD}
+  variables {obC obD : Type} (C : category obC) {D : category obD}
 
   definition adjoint (F : C ⇒ D) (G : D ⇒ C) :=
   natural_transformation (@functor.compose _ _ _ _ _ _ (Hom D) sorry)
diff --git a/library/algebra/category/basic.lean b/library/algebra/category/basic.lean
index 620aa2fcc..accee7e75 100644
--- a/library/algebra/category/basic.lean
+++ b/library/algebra/category/basic.lean
@@ -20,16 +20,16 @@ inductive Category : Type := mk : Π (ob : Type), category ob → Category
 
 namespace category
   section
-  parameters {ob : Type} {C : category ob} 
+  variables {ob : Type} {C : category ob} 
   variables {a b c d : ob} 
-
+  include C
   definition hom [reducible] : ob → ob → Type := rec (λ hom compose id assoc idr idl, hom) C
   -- note: needs to be reducible to typecheck composition in opposite category
   definition compose [reducible] : Π {a b c : ob}, hom b c → hom a b → hom a c :=
   rec (λ hom compose id assoc idr idl, compose) C
 
   definition id [reducible] : Π {a : ob}, hom a a := rec (λ hom compose id assoc idr idl, id) C
-  definition ID [reducible] : Π (a : ob), hom a a := @id
+  definition ID [reducible] : Π (a : ob), hom a a := @id ob C
 
   infixr `∘`:60 := compose
   infixl `⟶`:25 := hom -- input ⟶ using \--> (this is a different arrow than \-> (→))
@@ -168,7 +168,7 @@ infixl `⟹`:25 := natural_transformation
 
 namespace natural_transformation
   section
-  parameters {obC obD : Type} {C : category obC} {D : category obD} {F G : C ⇒ D}
+  variables {obC obD : Type} {C : category obC} {D : category obD} {F G : C ⇒ D}
 
   definition natural_map [coercion] (η : F ⟹ G) :
       Π(a : obC), hom (object F a) (object G a) :=
@@ -180,7 +180,7 @@ namespace natural_transformation
   end
 
   section
-  parameters {obC obD : Type} {C : category obC} {D : category obD} {F G H : C ⇒ D}
+  variables {obC obD : Type} {C : category obC} {D : category obD} {F G H : C ⇒ D}
   protected definition compose (η : G ⟹ H) (θ : F ⟹ G) : F ⟹ H :=
   natural_transformation.mk
     (λ a, η a ∘ θ a)
diff --git a/library/algebra/category/constructions.lean b/library/algebra/category/constructions.lean
index d8c68f222..f14930f31 100644
--- a/library/algebra/category/constructions.lean
+++ b/library/algebra/category/constructions.lean
@@ -58,10 +58,11 @@ namespace category
 
   section
   open decidable unit empty
-  parameters (A : Type) {H : decidable_eq A}
-  private definition set_hom (a b : A) := decidable.rec_on (H a b) (λh, unit) (λh, empty)
-  private theorem set_hom_subsingleton [instance] (a b : A) : subsingleton (set_hom a b) := _
-  private definition set_compose {a b c : A} (g : set_hom b c) (f : set_hom a b) : set_hom a c :=
+  variables {A : Type} {H : decidable_eq A}
+  include H
+  definition set_hom (a b : A) := decidable.rec_on (H a b) (λh, unit) (λh, empty)
+  theorem set_hom_subsingleton [instance] (a b : A) : subsingleton (set_hom a b) := _
+  definition set_compose {a b c : A} (g : set_hom b c) (f : set_hom a b) : set_hom a c :=
   decidable.rec_on
     (H b c)
     (λ Hbc g, decidable.rec_on
@@ -70,7 +71,7 @@ namespace category
       (λh f, empty.rec _ f) f)
     (λh (g : empty), empty.rec _ g) g
 
-  definition set_category : category A :=
+  definition set_category (A : Type) {H : decidable_eq A} : category A :=
   mk (λa b, set_hom a b)
      (λ a b c g f, set_compose g f)
      (λ a, rec_on_true rfl ⋆)
@@ -150,7 +151,7 @@ end ops
   end ops
 
   section functor_category
-  parameters {obC obD : Type} (C : category obC) (D : category obD)
+  variables {obC obD : Type} (C : category obC) (D : category obD)
   definition functor_category : category (functor C D) :=
   mk (λa b, natural_transformation a b)
      (λ a b c g f, natural_transformation.compose g f)
@@ -183,7 +184,7 @@ end ops
   section --remove
   open sigma category.ops --remove sigma
   instance [persistent] slice_category
-  parameters {ob : Type} (C : category ob)
+  variables {ob : Type} (C : category ob)
   definition forgetful (x : ob) : (slice_category C x) ⇒ C :=
   functor.mk (λ a, dpr1 a)
              (λ a b f, dpr1 f)
diff --git a/library/algebra/category/limit.lean b/library/algebra/category/limit.lean
index 62577cbd4..b8d6c8f84 100644
--- a/library/algebra/category/limit.lean
+++ b/library/algebra/category/limit.lean
@@ -10,7 +10,7 @@ open eq eq.ops category functor natural_transformation
 namespace limits
 --representable functor
   section
-  parameters {obI ob : Type} {I : category obI} {C : category ob} {D : I ⇒ C}
+  variables {obI ob : Type} {I : category obI} {C : category ob} {D : I ⇒ C}
 
   definition constant_diagram (a : ob) : I ⇒ C :=
   mk (λ i, a)
diff --git a/library/algebra/category/morphism.lean b/library/algebra/category/morphism.lean
index 03eea2258..c1ced7a9a 100644
--- a/library/algebra/category/morphism.lean
+++ b/library/algebra/category/morphism.lean
@@ -8,7 +8,7 @@ open eq eq.ops category
 
 namespace morphism
   section
-  parameters {ob : Type} {C : category ob} include C
+  variables {ob : Type} {C : category ob} include C
   variables {a b c d : ob} {h : @hom ob C c d} {g : @hom ob C b c} {f : @hom ob C a b} {i : @hom ob C b a}
   inductive is_section    [class] (f : @hom ob C a b) : Type
   := mk : ∀{g}, g ∘ f = id → is_section f
@@ -79,7 +79,7 @@ namespace morphism
       : is_iso f :=
   is_iso.mk (subst (section_eq_retraction f) (retraction_compose f)) (compose_section f)
 
-  theorem inverse_unique (H H' : is_iso f) : @inverse _ _ f H = @inverse _ _ f H' :=
+  theorem inverse_unique (H H' : is_iso f) : @inverse _ _ _ _ f H = @inverse _ _ _ _ f H' :=
   inverse_eq_intro_left !inverse_compose
 
   theorem inverse_involutive (f : a ⟶ b) {H : is_iso f} : (f⁻¹)⁻¹ = f :=
@@ -99,10 +99,10 @@ namespace morphism
   is_section.mk
     (calc
       (retraction_of f ∘ retraction_of g) ∘ g ∘ f
-            = retraction_of f ∘ retraction_of g ∘ g ∘ f : symm !assoc
+            = retraction_of f ∘ retraction_of g ∘ g ∘ f : symm (assoc _ _ (g ∘ f))
         ... = retraction_of f ∘ (retraction_of g ∘ g) ∘ f : {assoc _ g f}
-        ... = retraction_of f ∘ id ∘ f : {!retraction_compose}
-        ... = retraction_of f ∘ f : {!id_left}
+        ... = retraction_of f ∘ id ∘ f : {retraction_compose g}
+        ... = retraction_of f ∘ f : {id_left f}
         ... = id : !retraction_compose)
 
   theorem composition_is_retraction [instance] (Hf : is_retraction f) (Hg : is_retraction g)
@@ -111,8 +111,8 @@ namespace morphism
     (calc
       (g ∘ f) ∘ section_of f ∘ section_of g = g ∘ f ∘ section_of f ∘ section_of g : symm !assoc
         ... = g ∘ (f ∘ section_of f) ∘ section_of g : {assoc f _ _}
-        ... = g ∘ id ∘ section_of g : {!compose_section}
-        ... = g ∘ section_of g : {!id_left}
+        ... = g ∘ id ∘ section_of g : {compose_section f}
+        ... = g ∘ section_of g : {id_left (section_of g)}
         ... = id : !compose_section)
 
   theorem composition_is_inverse [instance] (Hf : is_iso f) (Hg : is_iso g) : is_iso (g ∘ f) :=
@@ -123,7 +123,7 @@ namespace morphism
   end -- remove
   namespace isomorphic
   section --remove
-  parameters {ob : Type} {C : category ob} include C --remove
+  variables {ob : Type} {C : category ob} include C --remove
   variables {a b c d : ob} {h : @hom ob C c d} {g : @hom ob C b c} {f : @hom ob C a b} --remove
   open relation
   -- should these be coercions?
@@ -142,7 +142,7 @@ namespace morphism
   end -- remove
   end isomorphic
   section --remove
-  parameters {ob : Type} {C : category ob} include C --remove
+  variables {ob : Type} {C : category ob} include C --remove
   variables {a b c d : ob} {h : @hom ob C c d} {g : @hom ob C b c} {f : @hom ob C a b} --remove
   --remove implicit arguments below
   inductive is_mono [class] (f : @hom ob C a b) : Prop :=
@@ -202,7 +202,7 @@ namespace morphism
 
   namespace iso
   section
-  parameters {ob : Type} {C : category ob} include C
+  variables {ob : Type} {C : category ob} include C
   variables {a b c d : ob}                                         (f : @hom ob C b a)
                            (r : @hom ob C c d) (q : @hom ob C b c) (p : @hom ob C a b)
                            (g : @hom ob C d c)
@@ -247,7 +247,7 @@ namespace morphism
 
   end
   section
-  parameters {ob : Type} {C : category ob} include C
+  variables {ob : Type} {C : category ob} include C
   variables {d                   c                   b                   a : ob}
                                   {i : @hom ob C b c} {f : @hom ob C b a}
               {r : @hom ob C c d} {q : @hom ob C b c} {p : @hom ob C a b}
diff --git a/library/algebra/category/yoneda.lean b/library/algebra/category/yoneda.lean
index 066844e14..56b1f9314 100644
--- a/library/algebra/category/yoneda.lean
+++ b/library/algebra/category/yoneda.lean
@@ -9,11 +9,11 @@ open eq eq.ops category functor category.ops prod
 namespace yoneda
 --representable functor
   section
-  parameters {ob : Type} {C : category ob}
+  variables {ob : Type} {C : category ob}
   set_option pp.universes true
   check @type_category
   section
-    parameters {a a' b b' : ob} (f : @hom ob C a' a) (g : @hom ob C b b')
+    variables {a a' b b' : ob} (f : @hom ob C a' a) (g : @hom ob C b b')
 --    definition Hom_fun_fun :
   end
   definition Hom : Cᵒᵖ ×c C ⇒ type :=
diff --git a/library/logic/examples/nuprl_examples.lean b/library/logic/examples/nuprl_examples.lean
index b10b70805..7eae64aaa 100644
--- a/library/logic/examples/nuprl_examples.lean
+++ b/library/logic/examples/nuprl_examples.lean
@@ -98,7 +98,7 @@ assume H : (P → Q) ∧ ((P ∨ ¬P) ∨ (Q ∨ ¬Q)),
 
 -- 5. First-Order Logic: All and Exists
 section
-parameters {T : Type} {C : Prop} {P : T → Prop}
+variables {T : Type} {C : Prop} {P : T → Prop}
 theorem thm17a : (C → ∀x, P x) → (∀x, C → P x) :=
 assume H : C → ∀x, P x,
   take x : T, assume Hc : C,