diff options
Diffstat (limited to 'Empty.thy')
| -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 |