diff options
author | Josh Chen | 2018-09-17 13:13:55 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-17 13:13:55 +0200 |
commit | 76ac8ed82317f3f62f26ecc88f412c61004bcffa (patch) | |
tree | 02f3f3f5f87027d38520e376c577e7e6621fa6cf /Empty.thy | |
parent | ea0c0c5427888982adce10ab25cebe445997f08b (diff) |
Reorganizing theories
Diffstat (limited to '')
-rw-r--r-- | Empty.thy | 22 |
1 files changed, 9 insertions, 13 deletions
@@ -1,28 +1,24 @@ -(* Title: HoTT/Empty.thy - Author: Josh Chen +(* +Title: Empty.thy +Author: Joshua Chen +Date: 2018 Empty type *) theory Empty - imports HoTT_Base -begin - +imports HoTT_Base -section \<open>Constants and type rules\<close> +begin -section \<open>Empty type\<close> axiomatization - Empty :: t ("\<zero>") and + Empty :: t ("\<zero>") and indEmpty :: "t \<Rightarrow> t" ("(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" - + Empty_form: "\<zero>: U O" and -text "Rule attribute declarations:" + Empty_elim: "\<lbrakk>a: \<zero>; C: \<zero> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero> a: C a" lemmas Empty_routine [intro] = Empty_form Empty_elim |