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 /Coprod.thy | |
parent | 515872533295e8464799467303fff923b52a2c01 (diff) | |
parent | f0999d07a0f41284ba84fae725a0186e0ec9ff5f (diff) |
Reorganized HoTT_Base, updated theories
Diffstat (limited to '')
-rw-r--r-- | Coprod.thy | 42 |
1 files changed, 21 insertions, 21 deletions
@@ -12,45 +12,45 @@ begin section \<open>Constants and type rules\<close> axiomatization - Coprod :: "[Term, Term] \<Rightarrow> Term" (infixr "+" 50) and - inl :: "Term \<Rightarrow> Term" and - inr :: "Term \<Rightarrow> Term" and - indCoprod :: "[Term \<Rightarrow> Term, Term \<Rightarrow> Term, Term] \<Rightarrow> Term" ("(1ind\<^sub>+)") + Coprod :: "[t, t] \<Rightarrow> t" (infixr "+" 50) and + inl :: "t \<Rightarrow> t" and + inr :: "t \<Rightarrow> t" and + indCoprod :: "[t \<Rightarrow> t, t \<Rightarrow> t, t] \<Rightarrow> t" ("(1ind\<^sub>+)") where - Coprod_form: "\<lbrakk>A: U(i); B: U(i)\<rbrakk> \<Longrightarrow> A + B: U(i)" + Coprod_form: "\<lbrakk>A: U i; B: U i\<rbrakk> \<Longrightarrow> A + B: U i" and - Coprod_intro_inl: "\<lbrakk>a: A; B: U(i)\<rbrakk> \<Longrightarrow> inl(a): A + B" + Coprod_intro_inl: "\<lbrakk>a: A; B: U i\<rbrakk> \<Longrightarrow> inl a: A + B" and - Coprod_intro_inr: "\<lbrakk>b: B; A: U(i)\<rbrakk> \<Longrightarrow> inr(b): A + B" + Coprod_intro_inr: "\<lbrakk>b: B; A: U i\<rbrakk> \<Longrightarrow> inr b: A + B" and Coprod_elim: "\<lbrakk> - C: A + B \<longrightarrow> U(i); - \<And>x. x: A \<Longrightarrow> c(x): C(inl(x)); - \<And>y. y: B \<Longrightarrow> d(y): C(inr(y)); + C: A + B \<longrightarrow> U i; + \<And>x. x: A \<Longrightarrow> c x: C (inl x); + \<And>y. y: B \<Longrightarrow> d y: C (inr y); u: A + B - \<rbrakk> \<Longrightarrow> ind\<^sub>+(c)(d)(u) : C(u)" + \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d u: C u" and Coprod_comp_inl: "\<lbrakk> - C: A + B \<longrightarrow> U(i); - \<And>x. x: A \<Longrightarrow> c(x): C(inl(x)); - \<And>y. y: B \<Longrightarrow> d(y): C(inr(y)); + C: A + B \<longrightarrow> U i; + \<And>x. x: A \<Longrightarrow> c x: C (inl x); + \<And>y. y: B \<Longrightarrow> d y: C (inr y); a: A - \<rbrakk> \<Longrightarrow> ind\<^sub>+(c)(d)(inl(a)) \<equiv> c(a)" + \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inl a) \<equiv> c a" and Coprod_comp_inr: "\<lbrakk> - C: A + B \<longrightarrow> U(i); - \<And>x. x: A \<Longrightarrow> c(x): C(inl(x)); - \<And>y. y: B \<Longrightarrow> d(y): C(inr(y)); + C: A + B \<longrightarrow> U i; + \<And>x. x: A \<Longrightarrow> c x: C (inl x); + \<And>y. y: B \<Longrightarrow> d y: C (inr y); b: B - \<rbrakk> \<Longrightarrow> ind\<^sub>+(c)(d)(inr(b)) \<equiv> d(b)" + \<rbrakk> \<Longrightarrow> ind\<^sub>+ c d (inr b) \<equiv> d b" text "Admissible formation inference rules:" axiomatization where - Coprod_wellform1: "A + B: U(i) \<Longrightarrow> A: U(i)" + Coprod_wellform1: "A + B: U i \<Longrightarrow> A: U i" and - Coprod_wellform2: "A + B: U(i) \<Longrightarrow> B: U(i)" + Coprod_wellform2: "A + B: U i \<Longrightarrow> B: U i" text "Rule attribute declarations:" |