Move Empty and Unit types to their own theories

3 files changed, 2 insertions, 32 deletions

diff --git a/HoTT.thy b/HoTT.thy
index 60e0e71..abb1085 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -13,10 +13,12 @@ HoTT_Methods
 
 (* Types *)
 Coprod
+Empty
 Equal
 Nat
 Prod
 Sum
+Unit
 
 (* Derived definitions and properties *)
 EqualProps
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
diff --git a/Sum.thy b/Sum.thy
index f97bef1..8d0b0e6 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -66,17 +66,4 @@ lemmas Sum_wellform [wellform] = Sum_wellform1 Sum_wellform2
 lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim
 
 
-section \<open>Empty type\<close>
-
-axiomatization
-  Empty :: Term  ("\<zero>") and
-  indEmpty :: "Term \<Rightarrow> Term"  ("(1ind\<^sub>\<zero>)")
-where
-  Empty_form: "\<zero> : U(O)"
-and
-  Empty_elim: "\<lbrakk>C: \<zero> \<longrightarrow> U(i); z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero>(z): C(z)"
-
-lemmas Empty_routine [intro] = Empty_form Empty_elim
-
-
 end