From 2e93e5d6a75ec21c86ddb4ef27e19cf9b1323dba Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 19 Dec 2014 20:50:53 -0800
Subject: [PATCH] fix(hott/init): minimize number of universe parameters

---
 hott/init/default.hlean | 2 +-
 hott/init/logic.hlean   | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/hott/init/default.hlean b/hott/init/default.hlean
index 08705dd86..a0c9b5e74 100644
--- a/hott/init/default.hlean
+++ b/hott/init/default.hlean
@@ -10,4 +10,4 @@ import init.bool init.num init.priority init.relation init.wf
 import init.types.sigma init.types.prod init.types.empty
 import init.trunc init.path init.equiv init.util
 import init.axioms.ua init.axioms.funext init.axioms.funext_from_ua
-import init.hedberg
+import init.hedberg init.nat
diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean
index a4b12c57f..12dbff7ab 100644
--- a/hott/init/logic.hlean
+++ b/hott/init/logic.hlean
@@ -7,7 +7,7 @@ Authors: Leonardo de Moura
 prelude
 import init.datatypes init.reserved_notation
 
-definition not (a : Type) := a → empty
+definition not.{l} (a : Type.{l}) := a → empty.{l}
 prefix `¬` := not
 
 definition absurd {a : Type} {b : Type} (H₁ : a) (H₂ : ¬a) : b :=
@@ -203,7 +203,7 @@ end inhabited
 -- decidable
 -- ---------
 
-inductive decidable [class] (p : Type) : Type :=
+inductive decidable.{l} [class] (p : Type.{l}) : Type.{l} :=
 inl :  p → decidable p,
 inr : ¬p → decidable p