From eee7d9771c3acd4a45ece85fd9a0bf8f7a46e0e7 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Mon, 25 May 2020 19:37:57 +0200
Subject: more reorganizing

---
 ROOT                |  5 ++---
 hott/HoTT.thy       | 10 ----------
 hott/More_List.thy  |  8 ++++++++
 hott/More_Types.thy |  2 +-
 hott/Nat.thy        |  2 +-
 5 files changed, 12 insertions(+), 15 deletions(-)
 delete mode 100644 hott/HoTT.thy
 create mode 100644 hott/More_List.thy

diff --git a/ROOT b/ROOT
index b716396..844f92b 100644
--- a/ROOT
+++ b/ROOT
@@ -28,9 +28,8 @@ session HoTT in hott = Spartan +
       Available online at https://homotopytypetheory.org/book.
   "
   theories
-    HoTT (global)
     Identity
     Equivalence
-    More_Types
     Nat
-
+    More_Types
+    More_List
diff --git a/hott/HoTT.thy b/hott/HoTT.thy
deleted file mode 100644
index 0b3040c..0000000
--- a/hott/HoTT.thy
+++ /dev/null
@@ -1,10 +0,0 @@
-theory HoTT
-imports
-  Identity
-  Equivalence
-  More_Types
-  Nat
-
-begin
-
-end
diff --git a/hott/More_List.thy b/hott/More_List.thy
new file mode 100644
index 0000000..2f868b8
--- /dev/null
+++ b/hott/More_List.thy
@@ -0,0 +1,8 @@
+theory More_List
+imports Spartan.List
+
+begin
+
+
+
+end
diff --git a/hott/More_Types.thy b/hott/More_Types.thy
index 17789f8..d29d794 100644
--- a/hott/More_Types.thy
+++ b/hott/More_Types.thy
@@ -1,5 +1,5 @@
 theory More_Types
-imports Equivalence
+imports Spartan
 
 begin
 
diff --git a/hott/Nat.thy b/hott/Nat.thy
index e129be0..d54ea7b 100644
--- a/hott/Nat.thy
+++ b/hott/Nat.thy
@@ -1,5 +1,5 @@
 theory Nat
-imports Equivalence
+imports Identity
 
 begin
 
-- 
cgit v1.2.3