diff options
Diffstat (limited to '')
| -rw-r--r-- | Unit.thy | 32 |
1 files changed, 0 insertions, 32 deletions
diff --git a/Unit.thy b/Unit.thy deleted file mode 100644 index 7c221f0..0000000 --- a/Unit.thy +++ /dev/null @@ -1,32 +0,0 @@ -(* -Title: Unit.thy -Author: Joshua Chen -Date: 2018 - -Unit type -*) - -theory Unit -imports HoTT_Base - -begin - - -axiomatization - 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>a: \<one>; c: C \<star>; C: \<one> \<longrightarrow> U i\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c a: C a" and - - 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 |