diff options
-rw-r--r-- | HoTT.thy | 2 | ||||
-rw-r--r-- | Prod.thy | 19 | ||||
-rw-r--r-- | Sum.thy | 13 |
3 files changed, 2 insertions, 32 deletions
@@ -13,10 +13,12 @@ HoTT_Methods (* Types *) Coprod +Empty Equal Nat Prod Sum +Unit (* Derived definitions and properties *) EqualProps @@ -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 @@ -66,17 +66,4 @@ lemmas Sum_wellform [wellform] = Sum_wellform1 Sum_wellform2 lemmas Sum_routine [intro] = Sum_form Sum_intro Sum_elim -section \<open>Empty type\<close> - -axiomatization - Empty :: Term ("\<zero>") and - indEmpty :: "Term \<Rightarrow> Term" ("(1ind\<^sub>\<zero>)") -where - Empty_form: "\<zero> : U(O)" -and - Empty_elim: "\<lbrakk>C: \<zero> \<longrightarrow> U(i); z: \<zero>\<rbrakk> \<Longrightarrow> ind\<^sub>\<zero>(z): C(z)" - -lemmas Empty_routine [intro] = Empty_form Empty_elim - - end |