From 57d183c7955fb54b3eb6dd431f5aec338131266b Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Fri, 22 Feb 2019 23:45:50 +0100
Subject: Cleanups and reorganization

---
 Empty.thy | 27 ---------------------------
 1 file changed, 27 deletions(-)
 delete mode 100644 Empty.thy

(limited to 'Empty.thy')

diff --git a/Empty.thy b/Empty.thy
deleted file mode 100644
index ee11045..0000000
--- a/Empty.thy
+++ /dev/null
@@ -1,27 +0,0 @@
-(*
-Title:  Empty.thy
-Author: Joshua Chen
-Date:   2018
-
-Empty type
-*)
-
-theory Empty
-imports HoTT_Base
-
-begin
-
-
-axiomatization
-  Empty    :: t  ("\<zero>") and
-  indEmpty :: "t \<Rightarrow> t"  ("(1ind\<^sub>\<zero>)")
-where
-  Empty_form: "\<zero>: U O" and
-
-  Empty_elim: "\<lbrakk>a: \<zero>; C: \<zero> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> a: C a"
-
-lemmas Empty_form [form]
-lemmas Empty_routine [intro] = Empty_form Empty_elim
-
-
-end
-- 
cgit v1.2.3