diff options
Diffstat (limited to 'Prod.thy')
-rw-r--r-- | Prod.thy | 19 |
1 files changed, 0 insertions, 19 deletions
@@ -81,23 +81,4 @@ syntax "_COMPOSE" :: "[Term, Term] \<Rightarrow> Term" (infixr "\<circ>" 70) translations "g \<circ> f" \<rightleftharpoons> "g o f" -section \<open>Unit type\<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" - -lemmas Unit_comp [comp] -lemmas Unit_routine [intro] = Unit_form Unit_intro Unit_elim - - end |