diff --git a/hott/init/function.hlean b/hott/init/function.hlean
index eb2af4e3df..a537900a10 100644
--- a/hott/init/function.hlean
+++ b/hott/init/function.hlean
@@ -18,23 +18,23 @@ definition compose [reducible] (f : B → C) (g : A → B) : A → C :=
 definition id [reducible] (a : A) : A :=
 a
 
-definition on_fun (f : B → B → C) (g : A → B) : A → A → C :=
+definition on_fun [reducible] (f : B → B → C) (g : A → B) : A → A → C :=
 λx y, f (g x) (g y)
 
-definition combine (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E :=
+definition combine [reducible] (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E :=
 λx y, op (f x y) (g x y)
 
-definition const {A : Type} (B : Type) (a : A) : B → A :=
+definition const [reducible] (B : Type) (a : A) : B → A :=
 λx, a
 
-definition dcompose {A : Type} {B : A → Type} {C : Π {x : A}, B x → Type}
+definition dcompose [reducible] {B : A → Type} {C : Π {x : A}, B x → Type}
   (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) :=
 λx, f (g x)
 
-definition flip {A : Type} {B : Type} {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
+definition flip [reducible] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
 λy x, f x y
 
-definition app {A : Type} {B : A → Type} (f : Πx, B x) (x : A) : B x :=
+definition app [reducible] {B : A → Type} (f : Πx, B x) (x : A) : B x :=
 f x
 
 precedence `∘'`:60
@@ -53,3 +53,6 @@ notation f `-[` op `]-` g  := combine f op g
 notation a `⟨` f `⟩` b     :=  f a b
 
 end function
+
+-- copy reducible annotations to top-level
+export [reduce-hints] function
diff --git a/library/algebra/function.lean b/library/algebra/function.lean
index 8649d51008..f76509f201 100644
--- a/library/algebra/function.lean
+++ b/library/algebra/function.lean
@@ -17,23 +17,23 @@ definition compose [reducible] (f : B → C) (g : A → B) : A → C :=
 definition id [reducible] (a : A) : A :=
 a
 
-definition on_fun (f : B → B → C) (g : A → B) : A → A → C :=
+definition on_fun [reducible] (f : B → B → C) (g : A → B) : A → A → C :=
 λx y, f (g x) (g y)
 
-definition combine (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E :=
+definition combine [reducible] (f : A → B → C) (op : C → D → E) (g : A → B → D) : A → B → E :=
 λx y, op (f x y) (g x y)
 
-definition const {A : Type} (B : Type) (a : A) : B → A :=
+definition const [reducible] (B : Type) (a : A) : B → A :=
 λx, a
 
-definition dcompose {A : Type} {B : A → Type} {C : Π {x : A}, B x → Type}
+definition dcompose [reducible] {B : A → Type} {C : Π {x : A}, B x → Type}
   (f : Π {x : A} (y : B x), C y) (g : Πx, B x) : Πx, C (g x) :=
 λx, f (g x)
 
-definition flip {A : Type} {B : Type} {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
+definition flip [reducible] {C : A → B → Type} (f : Πx y, C x y) : Πy x, C x y :=
 λy x, f x y
 
-definition app {A : Type} {B : A → Type} (f : Πx, B x) (x : A) : B x :=
+definition app [reducible] {B : A → Type} (f : Πx, B x) (x : A) : B x :=
 f x
 
 precedence `∘'`:60
@@ -47,3 +47,6 @@ infixr  $                  := app
 notation f `-[` op `]-` g  := combine f op g
 
 end function
+
+-- copy reducible annotations to top-level
+export [reduce-hints] function
diff --git a/tests/lean/hott/433.hlean b/tests/lean/hott/433.hlean
index 6bd9324340..bd31d2a004 100644
--- a/tests/lean/hott/433.hlean
+++ b/tests/lean/hott/433.hlean
@@ -94,7 +94,6 @@ namespace pi
   definition transport_V [reducible] (P : A → Type) {x y : A} (p : x = y) (u : P y) : P x :=
   p⁻¹ ▹ u
 
-  open function
   protected definition functor_pi : (Π(a:A), B a) → (Π(a':A'), B' a') := (λg a', f1 a' (g (f0 a')))
   /- Equivalences -/
   definition isequiv_functor_pi [instance] (f0 : A' → A) (f1 : Π(a':A'), B (f0 a') → B' a')