aboutsummaryrefslogtreecommitdiff
path: root/hott
diff options
context:
space:
mode:
Diffstat (limited to 'hott')
-rw-r--r--hott/HoTT.thy10
-rw-r--r--hott/More_List.thy8
-rw-r--r--hott/More_Types.thy2
-rw-r--r--hott/Nat.thy2
4 files changed, 10 insertions, 12 deletions
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