Move Empty and Unit types to their own theories

1 files changed, 0 insertions, 19 deletions

diff --git a/Prod.thy b/Prod.thy
index 9dbb01e..b0408b9 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -81,23 +81,4 @@ syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<circ>" 70)
 translations "g \<circ> f" \<rightleftharpoons> "g o f"
 
 
-section \<open>Unit type\<close>
-
-axiomatization
-  Unit :: Term  ("\<one>") and
-  pt :: Term    ("\<star>") and
-  indUnit :: "[Term, Term] \<Rightarrow> Term"  ("(1ind\<^sub>\<one>)")
-where
-  Unit_form: "\<one>: U(O)"
-and
-  Unit_intro: "\<star>: \<one>"
-and
-  Unit_elim: "\<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>); a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(a) : C(a)"
-and
-  Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U(i); c: C(\<star>)\<rbrakk> \<Longrightarrow> ind\<^sub>\<one>(c)(\<star>) \<equiv> c"
-
-lemmas Unit_comp [comp]
-lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
-
-
 end