diff --git a/hott/algebra/category/groupoid.hlean b/hott/algebra/category/groupoid.hlean
index 078111cf2d..5ee7ff5f37 100644
--- a/hott/algebra/category/groupoid.hlean
+++ b/hott/algebra/category/groupoid.hlean
@@ -66,7 +66,7 @@ namespace category
   end
 
   -- Conversely we can turn each group into a groupoid on the unit type
-  definition groupoid_of_group.{l} (A : Type.{l}) [G : group A] : groupoid.{l l} unit :=
+  definition groupoid_of_group.{l} (A : Type.{l}) [G : group A] : groupoid.{0 l} unit :=
   begin
     fapply groupoid.mk, fapply precategory.mk,
       intros, exact A,
diff --git a/hott/hit/suspension.hlean b/hott/hit/suspension.hlean
index 3dc240210b..9005d100e5 100644
--- a/hott/hit/suspension.hlean
+++ b/hott/hit/suspension.hlean
@@ -10,7 +10,7 @@ import .pushout types.pointed
 
 open pushout unit eq equiv equiv.ops pointed
 
-definition suspension (A : Type) : Type := pushout (λ(a : A), star.{0}) (λ(a : A), star.{0})
+definition suspension (A : Type) : Type := pushout (λ(a : A), star) (λ(a : A), star)
 
 namespace suspension
   variable {A : Type}
diff --git a/hott/init/datatypes.hlean b/hott/init/datatypes.hlean
index ea43aa821b..15416c0b89 100644
--- a/hott/init/datatypes.hlean
+++ b/hott/init/datatypes.hlean
@@ -14,7 +14,10 @@ notation `Type₁` := Type.{1}
 notation `Type₂` := Type.{2}
 notation `Type₃` := Type.{3}
 
-inductive unit.{l} : Type.{l} :=
+inductive poly_unit.{l} : Type.{l} :=
+star : poly_unit
+
+inductive unit : Type₀ :=
 star : unit
 
 inductive empty : Type₀
diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean
index 32da11ddfe..10849f07ee 100644
--- a/hott/init/equiv.hlean
+++ b/hott/init/equiv.hlean
@@ -8,7 +8,7 @@ Ported from Coq HoTT
 
 prelude
 import .path .function
-open eq function
+open eq function lift
 
 /- Equivalences -/
 
@@ -140,6 +140,9 @@ namespace is_equiv
 
   end
 
+  definition is_equiv_up [instance] (A : Type) : is_equiv (up : A → lift A) :=
+  adjointify up down (λa, by induction a;reflexivity) (λa, idp)
+
   section
   variables {A B C : Type} (f : A → B) {f' : A → B} [Hf : is_equiv f] (g : B → C)
   include Hf
@@ -293,6 +296,8 @@ namespace equiv
   definition equiv_of_equiv_of_eq {A B C : Type} (p : A = B) (q : B ≃ C) : A ≃ C := p⁻¹ ▸ q
   definition equiv_of_eq_of_equiv {A B C : Type} (p : A ≃ B) (q : B = C) : A ≃ C := q   ▸ p
 
+  definition equiv_lift (A : Type) : A ≃ lift A := equiv.mk up _
+
   namespace ops
     postfix `⁻¹` := equiv.symm -- overloaded notation for inverse
   end ops
diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean
index 12288a6e7e..e322b6a339 100644
--- a/hott/init/funext.hlean
+++ b/hott/init/funext.hlean
@@ -8,7 +8,7 @@ Ported from Coq HoTT
 
 prelude
 import .trunc .equiv .ua
-open eq is_trunc sigma function is_equiv equiv prod unit prod.ops
+open eq is_trunc sigma function is_equiv equiv prod unit prod.ops lift
 
 /-
    We now prove that funext follows from a couple of weaker-looking forms
@@ -208,24 +208,21 @@ end
 -- implies (with dependent eta) also the strong dependent funext.
 theorem weak_funext_of_ua : weak_funext :=
   (λ (A : Type) (P : A → Type) allcontr,
-    let U := (λ (x : A), unit) in
-  have pequiv : Π (x : A), P x ≃ U x,
+    let U := (λ (x : A), lift unit) in
+  have pequiv : Π (x : A), P x ≃ unit,
     from (λ x, @equiv_unit_of_is_contr (P x) (allcontr x)),
   have psim : Π (x : A), P x = U x,
-    from (λ x, @is_equiv.inv _ _
-      equiv_of_eq (univalence _ _) (pequiv x)),
+    from (λ x, eq_of_equiv_lift (pequiv x)),
   have p : P = U,
     from @nondep_funext_from_ua A Type P U psim,
-  have tU' : is_contr (A → unit),
-    from is_contr.mk (λ x, ⋆)
-      (λ f, @nondep_funext_from_ua A unit (λ x, ⋆) f
-        (λ x, unit.rec_on (f x) idp)),
+  have tU' : is_contr (A → lift unit),
+    from is_contr.mk (λ x, up ⋆)
+      (λ f, nondep_funext_from_ua (λa, by induction (f a) with u;induction u;reflexivity)),
   have tU : is_contr (Π x, U x),
     from tU',
   have tlast : is_contr (Πx, P x),
-    from eq.transport _ p⁻¹ tU,
-  tlast
-)
+    from p⁻¹ ▸ tU,
+  tlast)
 
 -- In the following we will proof function extensionality using the univalence axiom
 definition funext_of_ua : funext :=
diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean
index 95d8bd3621..bbed73018f 100644
--- a/hott/init/ua.hlean
+++ b/hott/init/ua.hlean
@@ -46,7 +46,8 @@ ap10 (cast_ua_fn f) a
 definition ua_equiv_of_eq [reducible] {A B : Type} (p : A = B) : ua (equiv_of_eq p) = p :=
 left_inv equiv_of_eq p
 
-
+definition eq_of_equiv_lift {A B : Type} (f : A ≃ B) : A = lift B :=
+ua (f ⬝e !equiv_lift)
 
 namespace equiv
   -- One consequence of UA is that we can transport along equivalencies of types
diff --git a/library/init/datatypes.lean b/library/init/datatypes.lean
index 89732ca913..fbe78e49ad 100644
--- a/library/init/datatypes.lean
+++ b/library/init/datatypes.lean
@@ -16,7 +16,10 @@ notation `Type₃` := Type.{3}
 set_option structure.eta_thm     true
 set_option structure.proj_mk_thm true
 
-inductive unit.{l} : Type.{l} :=
+inductive poly_unit.{l} : Type.{l} :=
+star : poly_unit
+
+inductive unit : Type₁ :=
 star : unit
 
 inductive true : Prop :=
@@ -24,7 +27,7 @@ intro : true
 
 inductive false : Prop
 
-inductive empty : Type
+inductive empty : Type₁
 
 inductive eq {A : Type} (a : A) : A → Prop :=
 refl : eq a a
diff --git a/src/frontends/lean/inductive_cmd.cpp b/src/frontends/lean/inductive_cmd.cpp
index b1ff6bb77d..f5c42820c4 100644
--- a/src/frontends/lean/inductive_cmd.cpp
+++ b/src/frontends/lean/inductive_cmd.cpp
@@ -726,7 +726,7 @@ struct inductive_cmd_fn {
     }
 
     environment mk_aux_decls(environment env, buffer<inductive_decl> const & decls) {
-        bool has_unit = has_unit_decls(env);
+        bool has_unit = has_poly_unit_decls(env);
         bool has_eq   = has_eq_decls(env);
         bool has_heq  = has_heq_decls(env);
         bool has_prod = has_prod_decls(env);
diff --git a/src/library/constants.cpp b/src/library/constants.cpp
index de0bb7e14c..b8cbcca3ec 100644
--- a/src/library/constants.cpp
+++ b/src/library/constants.cpp
@@ -140,8 +140,8 @@ name const * g_true = nullptr;
 name const * g_true_intro = nullptr;
 name const * g_is_trunc_is_hset = nullptr;
 name const * g_is_trunc_is_hprop = nullptr;
-name const * g_unit = nullptr;
-name const * g_unit_star = nullptr;
+name const * g_poly_unit = nullptr;
+name const * g_poly_unit_star = nullptr;
 name const * g_well_founded = nullptr;
 void initialize_constants() {
     g_absurd = new name{"absurd"};
@@ -281,8 +281,8 @@ void initialize_constants() {
     g_true_intro = new name{"true", "intro"};
     g_is_trunc_is_hset = new name{"is_trunc", "is_hset"};
     g_is_trunc_is_hprop = new name{"is_trunc", "is_hprop"};
-    g_unit = new name{"unit"};
-    g_unit_star = new name{"unit", "star"};
+    g_poly_unit = new name{"poly_unit"};
+    g_poly_unit_star = new name{"poly_unit", "star"};
     g_well_founded = new name{"well_founded"};
 }
 void finalize_constants() {
@@ -423,8 +423,8 @@ void finalize_constants() {
     delete g_true_intro;
     delete g_is_trunc_is_hset;
     delete g_is_trunc_is_hprop;
-    delete g_unit;
-    delete g_unit_star;
+    delete g_poly_unit;
+    delete g_poly_unit_star;
     delete g_well_founded;
 }
 name const & get_absurd_name() { return *g_absurd; }
@@ -564,7 +564,7 @@ name const & get_true_name() { return *g_true; }
 name const & get_true_intro_name() { return *g_true_intro; }
 name const & get_is_trunc_is_hset_name() { return *g_is_trunc_is_hset; }
 name const & get_is_trunc_is_hprop_name() { return *g_is_trunc_is_hprop; }
-name const & get_unit_name() { return *g_unit; }
-name const & get_unit_star_name() { return *g_unit_star; }
+name const & get_poly_unit_name() { return *g_poly_unit; }
+name const & get_poly_unit_star_name() { return *g_poly_unit_star; }
 name const & get_well_founded_name() { return *g_well_founded; }
 }
diff --git a/src/library/constants.h b/src/library/constants.h
index ccd8fe09ac..3cca60ef06 100644
--- a/src/library/constants.h
+++ b/src/library/constants.h
@@ -142,7 +142,7 @@ name const & get_true_name();
 name const & get_true_intro_name();
 name const & get_is_trunc_is_hset_name();
 name const & get_is_trunc_is_hprop_name();
-name const & get_unit_name();
-name const & get_unit_star_name();
+name const & get_poly_unit_name();
+name const & get_poly_unit_star_name();
 name const & get_well_founded_name();
 }
diff --git a/src/library/definitional/cases_on.cpp b/src/library/definitional/cases_on.cpp
index 724a987f2e..e8288b2bc9 100644
--- a/src/library/definitional/cases_on.cpp
+++ b/src/library/definitional/cases_on.cpp
@@ -83,8 +83,8 @@ environment mk_cases_on(environment const & env, name const & n) {
     optional<expr> star;
     // we use unit if num_types > 1
     if (num_types > 1) {
-        unit = mk_constant(get_unit_name(), to_list(elim_univ));
-        star = mk_constant(get_unit_star_name(), to_list(elim_univ));
+        unit = mk_constant(get_poly_unit_name(), to_list(elim_univ));
+        star = mk_constant(get_poly_unit_star_name(), to_list(elim_univ));
     }
 
     // rec_params order
diff --git a/src/library/definitional/equations.cpp b/src/library/definitional/equations.cpp
index 5ddf68af4b..e19f0eed65 100644
--- a/src/library/definitional/equations.cpp
+++ b/src/library/definitional/equations.cpp
@@ -1663,7 +1663,7 @@ class equation_compiler_fn {
                 C = Fun(C_args, type);
             } else {
                 expr d    = binding_domain(C_type);
-                expr unit = mk_constant(get_unit_name(), rlvl);
+                expr unit = mk_constant(get_poly_unit_name(), rlvl);
                 to_telescope_ext(d, C_args);
                 C = Fun(C_args, unit);
             }
@@ -1706,7 +1706,7 @@ class equation_compiler_fn {
                 new_ctx.append(rest);
                 F               = compile_pat_match(program(prg_i, to_list(new_ctx)), *p_idx);
             } else {
-                expr star    = mk_constant(get_unit_star_name(), rlvl);
+                expr star    = mk_constant(get_poly_unit_star_name(), rlvl);
                 buffer<expr> F_args;
                 F_args.append(C_args);
                 below        = mk_app(below, F_args);
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 5507320ba8..2831c9eaef 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -97,8 +97,8 @@ bool has_constructor(environment const & env, name const & c, name const & I, un
     return is_constant(type) && const_name(type) == I;
 }
 
-bool has_unit_decls(environment const & env) {
-    return has_constructor(env, get_unit_star_name(), get_unit_name(), 0);
+bool has_poly_unit_decls(environment const & env) {
+    return has_constructor(env, get_poly_unit_star_name(), get_poly_unit_name(), 0);
 }
 
 bool has_eq_decls(environment const & env) {
@@ -408,11 +408,11 @@ expr mk_and_elim_right(type_checker & tc, expr const & H) {
 }
 
 expr mk_unit(level const & l) {
-    return mk_constant(get_unit_name(), {l});
+    return mk_constant(get_poly_unit_name(), {l});
 }
 
 expr mk_unit_mk(level const & l) {
-    return mk_constant(get_unit_star_name(), {l});
+    return mk_constant(get_poly_unit_star_name(), {l});
 }
 
 expr mk_prod(type_checker & tc, expr const & A, expr const & B) {
diff --git a/src/library/util.h b/src/library/util.h
index 0d04d88f28..eb3fc27a56 100644
--- a/src/library/util.h
+++ b/src/library/util.h
@@ -33,7 +33,7 @@ bool is_standard(environment const & env);
 */
 bool is_norm_pi(type_checker & tc, expr & e, constraint_seq & cs);
 
-bool has_unit_decls(environment const & env);
+bool has_poly_unit_decls(environment const & env);
 bool has_eq_decls(environment const & env);
 bool has_heq_decls(environment const & env);
 bool has_prod_decls(environment const & env);
@@ -117,8 +117,8 @@ expr mk_and_intro(type_checker & tc, expr const & Ha, expr const & Hb);
 expr mk_and_elim_left(type_checker & tc, expr const & H);
 expr mk_and_elim_right(type_checker & tc, expr const & H);
 
-expr mk_unit(level const & l);
-expr mk_unit_mk(level const & l);
+expr mk_poly_unit(level const & l);
+expr mk_poly_unit_mk(level const & l);
 expr mk_prod(type_checker & tc, expr const & A, expr const & B);
 expr mk_pair(type_checker & tc, expr const & a, expr const & b);
 expr mk_pr1(type_checker & tc, expr const & p);
diff --git a/tests/lean/run/fib_brec.lean b/tests/lean/run/fib_brec.lean
index 2ccf338e9e..ecd88c82bf 100644
--- a/tests/lean/run/fib_brec.lean
+++ b/tests/lean/run/fib_brec.lean
@@ -6,7 +6,7 @@ namespace nat
   definition brec_on {C : nat → Type} (n : nat) (F : Π (n : nat), @nat.below C n → C n) : C n :=
   have general : C n × @nat.below C n, from
     nat.rec_on n
-      (pair (F zero unit.star) unit.star)
+      (pair (F zero poly_unit.star) poly_unit.star)
       (λ (n₁ : nat) (r₁ : C n₁ × @nat.below C n₁),
          have b : @nat.below C (succ n₁), from
            r₁,
diff --git a/tests/lean/run/forest.lean b/tests/lean/run/forest.lean
index ef0195d040..c21dbddd77 100644
--- a/tests/lean/run/forest.lean
+++ b/tests/lean/run/forest.lean
@@ -1,4 +1,4 @@
-import data.prod data.unit
+import data.prod
 open prod
 
 inductive tree (A : Type) : Type :=
@@ -18,7 +18,7 @@ definition tree.below.{l₁ l₂}
     (λ t : forest A, Type.{max 1 l₂})
     t
     (λ (a : A) (f : forest A) (r : Type.{max 1 l₂}), prod.{l₂ (max 1 l₂)} (C₂ f) r)
-    unit.{max 1 l₂}
+    poly_unit.{max 1 l₂}
     (λ (t : tree A) (f : forest A) (rt : Type.{max 1 l₂}) (rf : Type.{max 1 l₂}),
         prod.{(max 1 l₂) (max 1 l₂)} (prod.{l₂ (max 1 l₂)} (C₁ t) rt) (prod.{l₂ (max 1 l₂)} (C₂ f) rf))
 
@@ -32,7 +32,7 @@ definition forest.below.{l₁ l₂}
     (λ t : forest A, Type.{max 1 l₂})
     f
     (λ (a : A) (f : forest A) (r : Type.{max 1 l₂}), prod.{l₂ (max 1 l₂)} (C₂ f) r)
-    unit.{max 1 l₂}
+    poly_unit.{max 1 l₂}
     (λ (t : tree A) (f : forest A) (rt : Type.{max 1 l₂}) (rf : Type.{max 1 l₂}),
         prod.{(max 1 l₂) (max 1 l₂)} (prod.{l₂ (max 1 l₂)} (C₁ t) rt) (prod.{l₂ (max 1 l₂)} (C₂ f) rf))
 
@@ -57,7 +57,7 @@ have general : prod.{l₂ (max 1 l₂)} (C₁ t) (tree.below A C₁ C₂ t), fro
          F₁ (tree.node a f) b,
        prod.mk.{l₂ (max 1 l₂)} c b)
     (have b : forest.below A C₁ C₂ (forest.nil A), from
-      unit.star.{max 1 l₂},
+      poly_unit.star.{max 1 l₂},
      have c : C₂ (forest.nil A), from
       F₂ (forest.nil A) b,
      prod.mk.{l₂ (max 1 l₂)} c b)
@@ -93,7 +93,7 @@ have general : prod.{l₂ (max 1 l₂)} (C₂ f) (forest.below A C₁ C₂ f), f
          F₁ (tree.node a f) b,
        prod.mk.{l₂ (max 1 l₂)} c b)
     (have b : forest.below A C₁ C₂ (forest.nil A), from
-      unit.star.{max 1 l₂},
+      poly_unit.star.{max 1 l₂},
      have c : C₂ (forest.nil A), from
       F₂ (forest.nil A) b,
      prod.mk.{l₂ (max 1 l₂)} c b)
diff --git a/tests/lean/run/ftree_brec.lean b/tests/lean/run/ftree_brec.lean
index a05f61155a..785915542b 100644
--- a/tests/lean/run/ftree_brec.lean
+++ b/tests/lean/run/ftree_brec.lean
@@ -1,4 +1,4 @@
-import data.unit data.prod
+import data.prod
 
 inductive ftree (A : Type) (B : Type) : Type :=
 | leafa : ftree A B
@@ -16,7 +16,7 @@ definition below.{l l₁ l₂} {A : Type.{l₁}} {B : Type.{l₂}} (C : ftree A
   A
   B
   (λ t : ftree A B,  Type.{max l₁ l₂ (l+1)})
-  unit.{max l₁ l₂ (l+1)}
+  poly_unit.{max l₁ l₂ (l+1)}
   (λ (f₁ : A → B → ftree A B)
      (f₂ : B → ftree A B)
      (r₁ : Π (a : A) (b : B), Type.{max l₁ l₂ (l+1)})
@@ -60,7 +60,7 @@ have gen : prod.{(l+1) (max l₁ l₂ (l+1))} (C t) (@below A B C t), from
     B
     (λ t : ftree A B, prod.{(l+1) (max l₁ l₂ (l+1))} (C t) (@below A B C t))
     (have b : @below A B C (leafa A B), from
-       unit.star.{max l₁ l₂ (l+1)},
+       poly_unit.star.{max l₁ l₂ (l+1)},
      have c : C (leafa A B), from
        F (leafa A B) b,
      prod.mk.{(l+1) (max l₁ l₂ (l+1))} c b)
diff --git a/tests/lean/run/tree.lean b/tests/lean/run/tree.lean
index 7a488a79a0..10844e949d 100644
--- a/tests/lean/run/tree.lean
+++ b/tests/lean/run/tree.lean
@@ -44,7 +44,7 @@ end manual
     definition below_rec_on (t : tree A) (H : Π (n : tree A), @tree.below A C n → C n) : C t
     := have general : C t × @tree.below A C t, from
         tree.rec_on t
-          (λa, (H (leaf a) unit.star, unit.star))
+          (λa, (H (leaf a) poly_unit.star, poly_unit.star))
           (λ (l r : tree A) (Hl : C l × @tree.below A C l) (Hr : C r × @tree.below A C r),
             have b : @tree.below A C (node l r), from
               ((pr₁ Hl, pr₂ Hl), (pr₁ Hr, pr₂ Hr)),
diff --git a/tests/lean/run/univ_problem.lean b/tests/lean/run/univ_problem.lean
index 5fa87dfe25..93359ae180 100644
--- a/tests/lean/run/univ_problem.lean
+++ b/tests/lean/run/univ_problem.lean
@@ -1,4 +1,4 @@
-import logic data.nat.basic data.prod data.unit
+import logic data.nat.basic data.prod
 open nat prod
 
 inductive vector (A : Type) : nat → Type :=
@@ -17,7 +17,7 @@ namespace vector
     definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), @vector.below A C n v → C n v) : C n v :=
     have general : C n v × @vector.below A C n v, from
       vector.rec_on v
-       (pair (H zero vnil unit.star) unit.star)
+       (pair (H zero vnil poly_unit.star) poly_unit.star)
        (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × @vector.below A C n₁ v₁),
           have b : @vector.below A C _ (vcons a₁ v₁), from
             r₁,
diff --git a/tests/lean/run/vector.lean b/tests/lean/run/vector.lean
index 94061c22c1..a02d78c6db 100644
--- a/tests/lean/run/vector.lean
+++ b/tests/lean/run/vector.lean
@@ -33,7 +33,7 @@ namespace vector
     definition brec_on {n : nat} (v : vector A n) (H : Π (n : nat) (v : vector A n), @vector.below A C n v → C n v) : C n v :=
     have general : C n v × @vector.below A C n v, from
       vector.rec_on v
-       (pair (H zero vnil unit.star) unit.star)
+       (pair (H zero vnil poly_unit.star) poly_unit.star)
        (λ (n₁ : nat) (a₁ : A) (v₁ : vector A n₁) (r₁ : C n₁ v₁ × @vector.below A C n₁ v₁),
           have b : @vector.below A C _ (vcons a₁ v₁), from
             r₁,