diff options
author | Josh Chen | 2018-09-16 11:03:48 +0200 |
---|---|---|
committer | Josh Chen | 2018-09-16 11:03:48 +0200 |
commit | d4900ced2e071927d81a21a9127034941f258ec3 (patch) | |
tree | c0289b3fd8337a05baa7740ca3f5e84c57f539ca /Unit.thy | |
parent | 515872533295e8464799467303fff923b52a2c01 (diff) | |
parent | f0999d07a0f41284ba84fae725a0186e0ec9ff5f (diff) |
Reorganized HoTT_Base, updated theories
Diffstat (limited to '')
-rw-r--r-- | Unit.thy | 6 |
1 files changed, 3 insertions, 3 deletions
@@ -16,13 +16,13 @@ axiomatization pt :: Term ("\<star>") and indUnit :: "[Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>\<one>)") where - Unit_form: "\<one>: U(O)" + 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)" + 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_comp: "\<lbrakk>C: \<one> \<longrightarrow> U i; c: C \<star>\<rbrakk> \<Longrightarrow> ind\<^sub>\<one> c \<star> \<equiv> c" text "Rule attribute declarations:" |