diff options
author | Josh Chen | 2018-09-18 11:39:40 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-18 11:39:40 +0200 |
commit | a9588dfbd929fbc1b53a5c9b4f41fc5eb4ed4e46 (patch) | |
tree | ef21f4328214618f98ee465e92fb3308dfb786da /Empty.thy | |
parent | a2bb39ee8002eccc04b0cdaa82143840e6ec2565 (diff) | |
parent | 6857e783fa5cb91f058be322a18fb9ea583f2aad (diff) |
Merge branch 'develop', ready for release 0.1.0
Diffstat (limited to 'Empty.thy')
-rw-r--r-- | Empty.thy | 25 |
1 files changed, 11 insertions, 14 deletions
@@ -1,29 +1,26 @@ -(* 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 :: Term ("\<zero>") and - indEmpty :: "Term \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)") + 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_form [form] lemmas Empty_routine [intro] = Empty_form Empty_elim |