aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--Empty.thy30
-rw-r--r--Unit.thy33
2 files changed, 63 insertions, 0 deletions
diff --git a/Empty.thy b/Empty.thy
new file mode 100644
index 0000000..1b339ba
--- /dev/null
+++ b/Empty.thy
@@ -0,0 +1,30 @@
+(* Title: HoTT/Empty.thy
+ Author: Josh Chen
+
+Empty type
+*)
+
+theory Empty
+ imports HoTT_Base
+begin
+
+
+section \<open>Constants and type rules\<close>
+
+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)"
+
+
+text "Rule attribute declarations:"
+
+lemmas Empty_routine [intro] = Empty_form Empty_elim
+
+
+end
diff --git a/Unit.thy b/Unit.thy
new file mode 100644
index 0000000..6adfb02
--- /dev/null
+++ b/Unit.thy
@@ -0,0 +1,33 @@
+(* Title: HoTT/Unit.thy
+ Author: Josh Chen
+
+Unit type
+*)
+
+theory Unit
+ imports HoTT_Base
+begin
+
+
+section \<open>Constants and type rules\<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"
+
+
+text "Rule attribute declarations:"
+
+lemmas Unit_comp [comp]
+lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
+
+end