diff --git a/hott/algebra/category/functor/examples.hlean b/hott/algebra/category/functor/examples.hlean
index 7e4848ada..8824e0611 100644
--- a/hott/algebra/category/functor/examples.hlean
+++ b/hott/algebra/category/functor/examples.hlean
@@ -110,7 +110,7 @@ namespace functor
              (functor_uncurry_id G)
              (functor_uncurry_comp G)
 
-  theorem functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F :=
+  definition functor_uncurry_functor_curry : functor_uncurry (functor_curry F) = F :=
   functor_eq (λp, ap (to_fun_ob F) !prod.eta)
   begin
     intro cd cd' fg,
@@ -134,7 +134,7 @@ namespace functor
        rewrite [▸*, ↑functor_uncurry_hom, respect_id, ▸*, id_right]}
   end
 
-  theorem functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G :=
+  definition functor_curry_functor_uncurry : functor_curry (functor_uncurry G) = G :=
   begin
     fapply functor_eq, exact (functor_curry_functor_uncurry_ob G),
     intro c c' f,
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index 4baeb3a97..84637b4d2 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -154,15 +154,15 @@ namespace is_trunc
                        (λn IH Hn, is_trunc_of_imp_is_trunc)
                        Hn H
 
-  -- the following cannot be instances in their current form, because they are looping
-  theorem is_trunc_of_is_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A :=
+  -- these must be definitions, because we need them to compute sometimes
+  definition is_trunc_of_is_contr (A : Type) (n : trunc_index) [H : is_contr A] : is_trunc n A :=
   trunc_index.rec_on n H _
 
-  theorem is_trunc_succ_of_is_hprop (A : Type) (n : trunc_index) [H : is_hprop A]
+  definition is_trunc_succ_of_is_hprop (A : Type) (n : trunc_index) [H : is_hprop A]
       : is_trunc (n.+1) A :=
   is_trunc_of_leq A (show -1 ≤ n.+1, from star)
 
-  theorem is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A]
+  definition is_trunc_succ_succ_of_is_hset (A : Type) (n : trunc_index) [H : is_hset A]
       : is_trunc (n.+2) A :=
   is_trunc_of_leq A (show 0 ≤ n.+2, from star)