diff --git a/hott/init/hedberg.hlean b/hott/init/hedberg.hlean
index bd2dab47b..681b045b1 100644
--- a/hott/init/hedberg.hlean
+++ b/hott/init/hedberg.hlean
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 Hedberg's Theorem: every type with decidable equality is a hset
 -/
 prelude
-import init.nat init.trunc
+import init.trunc
 open eq eq.ops nat truncation sigma
 
 -- TODO(Leo): move const coll and path_coll to a different file?