diff --git a/hott/hit/sphere.hlean b/hott/hit/sphere.hlean
index 1a9d24f5a..e8af75c56 100644
--- a/hott/hit/sphere.hlean
+++ b/hott/hit/sphere.hlean
@@ -40,7 +40,7 @@ namespace sphere_index
   definition add (n m : sphere_index) : sphere_index :=
   sphere_index.rec_on m n (λ k l, l .+1)
 
-  definition leq (n m : sphere_index) : Type₁ :=
+  definition leq (n m : sphere_index) : Type₀ :=
   sphere_index.rec_on n (λm, unit) (λ n p m, sphere_index.rec_on m (λ p, empty) (λ m q p, p m) p) m
 
   infix `+1+`:65 := sphere_index.add
diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean
index 80a25c291..3c6576f3e 100644
--- a/hott/init/datatypes.hlean
+++ b/hott/init/datatypes.hlean
@@ -19,7 +19,7 @@ notation `Type₃` := Type.{3}
 inductive unit.{l} : Type.{l} :=
 star : unit
 
-inductive empty.{l} : Type.{l}
+inductive empty : Type₀
 
 inductive eq.{l} {A : Type.{l}} (a : A) : A → Type.{l} :=
 refl : eq a a
diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index 3af17582e..ceff140d5 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -11,7 +11,7 @@ import init.reserved_notation
 
 /- not -/
 
-definition not.{l} (a : Type.{l}) := a → empty.{l}
+definition not (a : Type) := a → empty
 prefix `¬` := not
 
 definition absurd {a b : Type} (H₁ : a) (H₂ : ¬a) : b :=
diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean
index 65a76a027..c949c2b5d 100644
--- a/hott/init/trunc.hlean
+++ b/hott/init/trunc.hlean
@@ -20,7 +20,7 @@ namespace is_trunc
 
  /- Truncation levels -/
 
-  inductive trunc_index : Type₁ :=
+  inductive trunc_index : Type₀ :=
   | minus_two : trunc_index
   | succ : trunc_index → trunc_index
 
@@ -38,7 +38,7 @@ namespace is_trunc
   definition add (n m : trunc_index) : trunc_index :=
   trunc_index.rec_on m n (λ k l, l .+1)
 
-  definition leq (n m : trunc_index) : Type₁ :=
+  definition leq (n m : trunc_index) : Type₀ :=
   trunc_index.rec_on n (λm, unit) (λ n p m, trunc_index.rec_on m (λ p, empty) (λ m q p, p m) p) m
   end trunc_index
 
diff --git a/hott/init/types.hlean b/hott/init/types.hlean
index c63bcca5f..9a645915f 100644
--- a/hott/init/types.hlean
+++ b/hott/init/types.hlean
@@ -191,7 +191,7 @@ iff.intro (assume H, pr1 H) (assume H, pair H star)
 definition unit_prod (a : Type) : unit × a ↔ a :=
 iff.intro (assume H, pr2 H) (assume H, pair star H)
 
-definition prod_empty.{l} (a : Type.{l}) : a × empty.{l} ↔ empty.{l} :=
+definition prod_empty (a : Type) : a × empty ↔ empty :=
 iff.intro (assume H, pr2 H) (assume H, !empty.elim H)
 
 definition empty_prod (a : Type) : empty × a ↔ empty :=
diff --git a/hott/types/hprop_trunc.hlean b/hott/types/hprop_trunc.hlean
index 392a00338..eed5360bf 100644
--- a/hott/types/hprop_trunc.hlean
+++ b/hott/types/hprop_trunc.hlean
@@ -46,15 +46,7 @@ namespace is_trunc
       { apply equiv.to_is_equiv, apply is_contr.sigma_char},
       apply (@is_hprop.mk), intros,
       fapply sigma_eq, {apply x.2},
-      apply (@is_hprop.elim),
-      apply is_trunc_pi, intro a,
-      apply is_hprop.mk, intro w z,
-      have H : is_hset A,
-      begin
-        apply is_trunc_succ, apply is_trunc_succ,
-        apply is_contr.mk, exact y.2
-      end,
-      fapply (@is_hset.elim A _ _ _ w z)},
+      apply (@is_hprop.elim)},
     { intro n' IH A,
       apply is_trunc_is_equiv_closed,
       apply equiv.to_is_equiv,