From 817d69123708943f798837393cf8f4fd3fabaf3a Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Tue, 1 Sep 2015 18:08:50 -0400
Subject: [PATCH] =?UTF-8?q?fix(hott/init/nat):=20also=20define=20=E2=84=95?=
 =?UTF-8?q?=20in=20the=20top-level=20in=20HoTT?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 hott/init/nat.hlean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean
index 9187f2788..30d1ad053 100644
--- a/hott/init/nat.hlean
+++ b/hott/init/nat.hlean
@@ -8,8 +8,9 @@ import init.wf init.tactic init.hedberg init.util init.types
 
 open eq decidable sum lift is_trunc
 
+notation `ℕ` := nat
+
 namespace nat
-  notation `ℕ` := nat
 
   /- basic definitions on natural numbers -/
   inductive le (a : ℕ) : ℕ → Type₀ :=