diff options
author | Josh Chen | 2018-06-05 17:35:49 +0200 |
---|---|---|
committer | Josh Chen | 2018-06-05 17:35:49 +0200 |
commit | 80412abb0fdec553d80a56af16d1cfd8da52e7ed (patch) | |
tree | e8476f69851b355dee28e703171efb8e7150ff47 /HoTT.thy | |
parent | c73a924eb679dea0455414a91dcdeb66b3f827f9 (diff) |
Proved that the inductor on Sum has the correct type.
Diffstat (limited to 'HoTT.thy')
-rw-r--r-- | HoTT.thy | 48 |
1 files changed, 31 insertions, 17 deletions
@@ -46,14 +46,14 @@ axiomatization Prod :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" syntax - "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Prod>_:_./ _)" 10) - "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<^bold>\<lambda>_:_./ _)" 10) + "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Prod>_:_./ _)" 30) + "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<^bold>\<lambda>_:_./ _)" 30) translations "\<Prod>x:A. B" \<rightleftharpoons> "CONST Prod A (\<lambda>x. B)" "\<^bold>\<lambda>x:A. b" \<rightleftharpoons> "CONST lambda A (\<lambda>x. b)" (* The above syntax translations bind the x in the expressions B, b. *) -abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 30) +abbreviation Function :: "[Term, Term] \<Rightarrow> Term" (infixr "\<rightarrow>" 10) where "A\<rightarrow>B \<equiv> \<Prod>_:A. B" axiomatization @@ -69,7 +69,7 @@ where Prod_comp [simp]: "\<And>(A::Term) (b::Term \<Rightarrow> Term) (a::Term). a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)" and - Prod_uniq [simp]: "\<And>(A::Term) (f::Term). \<^bold>\<lambda>x:A. (f`x) \<equiv> f" + Prod_uniq [simp]: "\<And>A f::Term. \<^bold>\<lambda>x:A. (f`x) \<equiv> f" lemmas Prod_formation = Prod_form Prod_form[rotated] @@ -80,7 +80,7 @@ subsubsection \<open>Dependent pair/sum\<close> axiomatization Sum :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" syntax - "_Sum" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 10) + "_Sum" :: "[idt, Term, Term] \<Rightarrow> Term" ("(3\<Sum>_:_./ _)" 20) translations "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)" @@ -89,7 +89,7 @@ abbreviation Pair :: "[Term, Term] \<Rightarrow> Term" (infixr "\<times>" 50) axiomatization pair :: "[Term, Term] \<Rightarrow> Term" ("(1'(_,/ _'))") and - indSum :: "[Term \<Rightarrow> Term] \<Rightarrow> Term" + indSum :: "(Term \<Rightarrow> Term) \<Rightarrow> Term" where Sum_form: "\<And>(A::Term) (B::Term \<Rightarrow> Term). \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x) : U" and @@ -97,9 +97,9 @@ where \<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> (a, b) : \<Sum>x:A. B(x)" and Sum_elim [elim]: "\<And>(A::Term) (B::Term \<Rightarrow> Term) (C::Term \<Rightarrow> Term) (f::Term) (p::Term). - \<lbrakk>C: \<Sum>x:A. B(x) \<rightarrow> U; f : \<Prod>x:A. \<Prod>y:B(x). C((x,y)); p : \<Sum>x:A. B(x)\<rbrakk> \<Longrightarrow> (indSum C)`f`p : C(p)" and + \<lbrakk>C: \<Sum>x:A. B(x) \<rightarrow> U; f : \<Prod>x:A. \<Prod>y:B(x). C((x,y)); p : \<Sum>x:A. B(x)\<rbrakk> \<Longrightarrow> indSum(C)`f`p : C(p)" and - Sum_comp [simp]: "\<And>(C::Term \<Rightarrow> Term) (f::Term) (a::Term) (b::Term). (indSum C)`f`(a,b) \<equiv> f`a`b" + Sum_comp [simp]: "\<And>(C::Term \<Rightarrow> Term) (f::Term) (a::Term) (b::Term). indSum(C)`f`(a,b) \<equiv> f`a`b" lemmas Sum_formation = Sum_form Sum_form[rotated] @@ -118,16 +118,16 @@ overloading snd_nondep \<equiv> snd begin definition fst_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where - "fst_dep A B \<equiv> (indSum (\<lambda>_. A))`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). x)" + "fst_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). x)" definition snd_dep :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" where - "snd_dep A B \<equiv> (indSum (\<lambda>_. A))`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)" + "snd_dep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)" definition fst_nondep :: "[Term, Term] \<Rightarrow> Term" where - "fst_nondep A B \<equiv> (indSum (\<lambda>_. A))`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)" + "fst_nondep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x)" definition snd_nondep :: "[Term, Term] \<Rightarrow> Term" where - "snd_nondep A B \<equiv> (indSum (\<lambda>_. A))`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. y)" + "snd_nondep A B \<equiv> indSum(\<lambda>_. A)`(\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. y)" end lemma fst_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def by simp @@ -136,18 +136,32 @@ lemma snd_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> snd[A,B lemma fst_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a" unfolding fst_nondep_def by simp lemma snd_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_nondep_def by simp -\<comment> \<open>Simplification rules for Sum\<close> +\<comment> \<open>Simplification rules for projections\<close> lemmas fst_snd_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp subsubsection \<open>Equality type\<close> axiomatization - Equal :: "Term \<Rightarrow> Term \<Rightarrow> Term \<Rightarrow> Term" ("(_ =_ _)") and - refl :: "Term \<Rightarrow> Term" ("(refl'(_'))") + Equal :: "[Term, Term, Term] \<Rightarrow> Term" +syntax + "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term" ("(3_ =\<^sub>_/ _)") +translations + "a =\<^sub>A b" \<rightleftharpoons> "CONST Equal A a b" + +axiomatization + refl :: "Term \<Rightarrow> Term" and + indEqual :: "([Term, Term, Term] \<Rightarrow> Term) \<Rightarrow> Term" where - Equal_form: "\<And>A a b. \<lbrakk>a : A; b : A\<rbrakk> \<Longrightarrow> a =A b : U" and - Equal_intro: "\<And>A x. x : A \<Longrightarrow> refl x : x =A x" + Equal_form: "\<And>A a b::Term. \<lbrakk>A : U; a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U" and + + Equal_intro [intro]: "\<And>A x::Term. x : A \<Longrightarrow> refl(x) : x =\<^sub>A x" + +(* and + + Equal_elim [elim]: "\<And>(C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (x::Term) (y::Term) (p::Term). + \<lbrakk>\<rbrakk> \<Longrightarrow> (indEqual C)`f`x`y`p : C(x)(y)(p)" +*) (* subsubsection \<open>Empty type\<close> |