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

---
 Unit.thy | 33 +++++++++++++++++++++++++++++++++
 1 file changed, 33 insertions(+)
 create mode 100644 Unit.thy

(limited to 'Unit.thy')

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

