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

---
 Unit.thy | 32 --------------------------------
 1 file changed, 32 deletions(-)
 delete mode 100644 Unit.thy

(limited to 'Unit.thy')

diff --git a/Unit.thy b/Unit.thy
deleted file mode 100644
index 7c221f0..0000000
--- a/Unit.thy
+++ /dev/null
@@ -1,32 +0,0 @@
-(*
-Title:  Unit.thy
-Author: Joshua Chen
-Date:   2018
-
-Unit type
-*)
-
-theory Unit
-imports HoTT_Base
-
-begin
-
-
-axiomatization
-  Unit    :: t  ("\<one>") and
-  pt      :: t  ("\<star>") and
-  indUnit :: "[t, t] \<Rightarrow> t"  ("(1ind\<^sub>\<one>)")
-where
-  Unit_form: "\<one>: U O" and
-
-  Unit_intro: "\<star>: \<one>" and
-
-  Unit_elim: "\<lbrakk>a: \<one>; c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" and
-
-  Unit_comp: "\<lbrakk>c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c"
-
-lemmas Unit_form [form]
-lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim
-lemmas Unit_comp [comp]
-
-end
-- 
cgit v1.2.3