From 4b799a9da44855c4767ace3a8153eb3d3b7d8ed0 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Wed, 3 Dec 2014 19:28:32 -0500
Subject: [PATCH] fix(hott/trunc): add explicit coercion so that the notation
 works if nat is not opened

---
 library/hott/trunc.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/hott/trunc.lean b/library/hott/trunc.lean
index 6dc07a6d9..8fd11254e 100644
--- a/library/hott/trunc.lean
+++ b/library/hott/trunc.lean
@@ -71,7 +71,7 @@ namespace truncation
   -- should this be notation or definitions?
   notation `is_contr` := is_trunc -2
   notation `is_hprop` := is_trunc -1
-  notation `is_hset`  := is_trunc nat.zero
+  notation `is_hset`  := is_trunc (nat_to_trunc_index nat.zero)
   -- definition is_contr := is_trunc -2
   -- definition is_hprop := is_trunc -1
   -- definition is_hset  := is_trunc 0