diff options
Diffstat (limited to 'Unit.thy')
| -rw-r--r-- | Unit.thy | 33 |
1 files changed, 16 insertions, 17 deletions
@@ -1,33 +1,32 @@ -(* Title: HoTT/Unit.thy - Author: Josh Chen +(* +Title: Unit.thy +Author: Joshua Chen +Date: 2018 Unit type *) theory Unit - imports HoTT_Base -begin +imports HoTT_Base +begin -section \<open>Constants and type rules\<close> axiomatization - Unit :: Term ("\<one>") and - pt :: Term ("\<star>") and - indUnit :: "[Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<one>)") + Unit :: t ("\<one>") and + pt :: t ("\<star>") and + indUnit :: "[t, t] \<Rightarrow> t" ("(1ind\<^sub>\<one>)") where - Unit_form: "\<one>: U O" -and - Unit_intro: "\<star>: \<one>" -and - Unit_elim: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>; a: \<one>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" -and - Unit_comp: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c" + Unit_form: "\<one>: U O" and + Unit_intro: "\<star>: \<one>" and -text "Rule attribute declarations:" + Unit_elim: "\<lbrakk>a: \<one>; c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" and -lemmas Unit_comp [comp] + Unit_comp: "\<lbrakk>c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c" + +lemmas Unit_form [form] lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim +lemmas Unit_comp [comp] end |