1 files changed, 0 insertions, 83 deletions
diff --git a/More_Types.thy b/More_Types.thy
deleted file mode 100644
index ebbe10b..0000000
--- a/More_Types.thy
+++ /dev/null
@@ -1,83 +0,0 @@
-(********
-Isabelle/HoTT: Coproduct, unit, and empty types
-Feb 2019
-
-********)
-
-theory More_Types
-imports HoTT_Base
-
-begin
-
-
-section \<open>Coproduct type\<close>
-
-axiomatization
-  Cprd    :: "[t, t] \<Rightarrow> t"  (infixr "+" 50) and
-  inl     :: "[t, t, t] \<Rightarrow> t" and
-  inr     :: "[t, t, t] \<Rightarrow> t" and
-  indCprd :: "[t \<Rightarrow> t, t \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t"
-where
-  Cprd_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" and
-
-  Cprd_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl A B a: A + B" and
-
-  Cprd_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr A B b: A + B" and
-
-  Cprd_elim: "\<lbrakk>
-    u: A + B;
-    C: A + B \<leadsto> U i;
-    \<And>x. x: A \<Longrightarrow> c x: C (inl A B x);
-    \<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d u: C u" and
-
-  Cprd_cmp_inl: "\<lbrakk>
-    a: A;
-    C: A + B \<leadsto> U i;
-    \<And>x. x: A \<Longrightarrow> c x: C (inl A B x);
-    \<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d (inl A B a) \<equiv> c a" and
-
-  Cprd_cmp_inr: "\<lbrakk>
-    b: B;
-    C: A + B \<leadsto> U i;
-    \<And>x. x: A \<Longrightarrow> c x: C (inl A B x);
-    \<And>y. y: B \<Longrightarrow> d y: C (inr A B y) \<rbrakk> \<Longrightarrow> indCprd C c d (inr A B b) \<equiv> d b"
-
-lemmas Cprd_form [form]
-lemmas Cprd_routine [intro] = Cprd_form Cprd_intro_inl Cprd_intro_inr Cprd_elim
-lemmas Cprd_comp [comp] = Cprd_cmp_inl Cprd_cmp_inr
-
-
-section \<open>Unit type\<close>
-
-axiomatization
-  Unit    :: t and
-  pt      :: t and
-  indUnit :: "[t \<Rightarrow> t, t, t] \<Rightarrow> t"
-where
-  Unit_form: "Unit: U O" and
-
-  Unit_intro: "pt: Unit" and
-
-  Unit_elim: "\<lbrakk>x: Unit; c: C pt; C: Unit \<leadsto> U i\<rbrakk> \<Longrightarrow> indUnit C c x: C x" and
-
-  Unit_cmp: "\<lbrakk>c: C Unit; C: Unit \<leadsto> U i\<rbrakk> \<Longrightarrow> indUnit C c pt \<equiv> c"
-
-lemmas Unit_form [form]
-lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
-lemmas Unit_comp [comp] = Unit_cmp
-
-
-section \<open>Empty type\<close>
-
-axiomatization
-  Null    :: t and
-  indNull :: "[t \<Rightarrow> t, t] \<Rightarrow> t"
-where
-  Null_form: "Null: U O" and
-
-  Null_elim: "\<lbrakk>z: Null; C: Null \<leadsto> U i\<rbrakk> \<Longrightarrow> indNull C z: C z"
-
-lemmas Null_form [form]
-lemmas Null_routine [intro] = Null_form Null_elim
-
-end