From 1ff1905f052de51a942282af1f9950c7ec71c20c Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Sat, 18 Aug 2018 23:58:29 +0200
Subject: Forgot to add the theories for Empty and Unit

---
 Empty.thy | 30 ++++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)
 create mode 100644 Empty.thy

(limited to 'Empty.thy')

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
-- 
cgit v1.2.3