diff options
author | Josh Chen | 2018-08-18 23:58:29 +0200 |
---|---|---|
committer | Josh Chen | 2018-08-18 23:58:29 +0200 |
commit | 1ff1905f052de51a942282af1f9950c7ec71c20c (patch) | |
tree | d6690505b3d20b8bc39fc080eb17b1e727f53339 /Empty.thy | |
parent | 2498c1512a81a9a73a5a8b6a1a0018ad824df778 (diff) |
Forgot to add the theories for Empty and Unit
Diffstat (limited to 'Empty.thy')
-rw-r--r-- | Empty.thy | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/Empty.thy b/Empty.thy new file mode 100644 index 0000000..1b339ba --- /dev/null +++ b/Empty.thy @@ -0,0 +1,30 @@ +(* Title: HoTT/Empty.thy + Author: Josh Chen + +Empty type +*) + +theory Empty + imports HoTT_Base +begin + + +section \<open>Constants and type rules\<close> + +section \<open>Empty type\<close> + +axiomatization + Empty :: Term ("\<zero>") and + indEmpty :: "Term \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)") +where + Empty_form: "\<zero> : U(O)" +and + Empty_elim: "\<lbrakk>C: \<zero> \<longrightarrow> U(i); z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero>(z): C(z)" + + +text "Rule attribute declarations:" + +lemmas Empty_routine [intro] = Empty_form Empty_elim + + +end |