From de6294a4ce1a908e9939152d0880a4ced90ad7f3 Mon Sep 17 00:00:00 2001
From: Floris van Doorn <fpv@andrew.cmu.edu>
Date: Fri, 15 May 2015 17:36:16 -0400
Subject: [PATCH] feat(hott.core): add more files to core.hlean

---
 hott/core.hlean          | 2 ++
 hott/types/default.hlean | 1 +
 2 files changed, 3 insertions(+)

diff --git a/hott/core.hlean b/hott/core.hlean
index 42d8c5706..3bdb9fbaa 100644
--- a/hott/core.hlean
+++ b/hott/core.hlean
@@ -9,3 +9,5 @@ The core of the HoTT library
 -/
 
 import types
+import cubical.pathover cubical.square
+import hit.circle
diff --git a/hott/types/default.hlean b/hott/types/default.hlean
index 5c082671c..48739ad73 100644
--- a/hott/types/default.hlean
+++ b/hott/types/default.hlean
@@ -7,3 +7,4 @@ Authors: Floris van Doorn
 -/
 
 import .sigma .prod .pi .equiv .fiber .eq .trunc .arrow .pointed .function .trunc .bool
+import .nat .int