diff options
| -rw-r--r-- | ROOT | 5 | ||||
| -rw-r--r-- | hott/HoTT.thy | 10 | ||||
| -rw-r--r-- | hott/More_List.thy | 8 | ||||
| -rw-r--r-- | hott/More_Types.thy | 2 | ||||
| -rw-r--r-- | hott/Nat.thy | 2 |
5 files changed, 12 insertions, 15 deletions
@@ -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 |