diff options
| author | Josh Chen | 2019-02-22 23:45:50 +0100 |
|---|---|---|
| committer | Josh Chen | 2019-02-22 23:45:50 +0100 |
| commit | 57d183c7955fb54b3eb6dd431f5aec338131266b (patch) | |
| tree | ae6bfabbd8fcd63ee7d5140ca842599efbd58c16 /Empty.thy | |
| parent | 0036345412d5c145b63693ed672b175018fa3791 (diff) | |
Cleanups and reorganization
Diffstat (limited to '')
| -rw-r--r-- | Empty.thy | 27 |
1 files changed, 0 insertions, 27 deletions
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 |