Cleanups and reorganization

1 files changed, 0 insertions, 32 deletions

diff --git a/Unit.thy b/Unit.thy
deleted file mode 100644
index 7c221f0..0000000
--- a/Unit.thy
+++ /dev/null
@@ -1,32 +0,0 @@
-(*
-Title:  Unit.thy
-Author: Joshua Chen
-Date:   2018
-
-Unit type
-*)
-
-theory Unit
-imports HoTT_Base
-
-begin
-
-
-axiomatization
-  Unit    :: t  ("\<one>") and
-  pt      :: t  ("\<star>") and
-  indUnit :: "[t, t] \<Rightarrow> t"  ("(1ind\<^sub>\<one>)")
-where
-  Unit_form: "\<one>: U O" and
-
-  Unit_intro: "\<star>: \<one>" and
-
-  Unit_elim: "\<lbrakk>a: \<one>; c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" and
-
-  Unit_comp: "\<lbrakk>c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c"
-
-lemmas Unit_form [form]
-lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
-lemmas Unit_comp [comp]
-
-end