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 /Unit.thy | |
parent | 2498c1512a81a9a73a5a8b6a1a0018ad824df778 (diff) |
Forgot to add the theories for Empty and Unit
Diffstat (limited to '')
-rw-r--r-- | Unit.thy | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/Unit.thy b/Unit.thy new file mode 100644 index 0000000..6adfb02 --- /dev/null +++ b/Unit.thy @@ -0,0 +1,33 @@ +(* Title: HoTT/Unit.thy + Author: Josh Chen + +Unit type +*) + +theory Unit + 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>)") +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" + + +text "Rule attribute declarations:" + +lemmas Unit_comp [comp] +lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim + +end |