aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--HoTT.thy48
-rw-r--r--HoTT_Theorems.thy77
2 files changed, 81 insertions, 44 deletions
diff --git a/HoTT.thy b/HoTT.thy
index 68de364..ef39734 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -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>
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy
index a44c8f9..1ac4484 100644
--- a/HoTT_Theorems.thy
+++ b/HoTT_Theorems.thy
@@ -21,19 +21,19 @@ text "Declaring \<open>Prod_intro\<close> with the \<open>intro\<close> attribut
lemma "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" ..
proposition "A \<equiv> B \<Longrightarrow> \<^bold>\<lambda>x:A. x : B\<rightarrow>A"
- proof -
- assume assm: "A \<equiv> B"
- have id: "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" ..
- from assm have "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp
- with id show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" ..
- qed
+proof -
+ assume assm: "A \<equiv> B"
+ have id: "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" ..
+ from assm have "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp
+ with id show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" ..
+qed
proposition "\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. x : A\<rightarrow>B\<rightarrow>A"
- proof
- fix a
- assume "a : A"
- then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" ..
- qed
+proof
+ fix a
+ assume "a : A"
+ then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" ..
+qed
subsection \<open>Function application\<close>
@@ -61,9 +61,9 @@ proof (rule Prod_formation)
fix x::Term
assume *: "x : A"
show "\<Prod>y:B(x). C x y : U"
- proof (rule Prod_formation)
- show "B(x) : U" using * by (rule assms)
- qed (rule assms)
+ proof (rule Prod_formation)
+ show "B(x) : U" using * by (rule assms)
+ qed (rule assms)
qed (rule assms)
proposition triply_curried:
@@ -81,36 +81,59 @@ proposition triply_curried:
proof (rule Prod_formation)
fix x::Term assume 1: "x : A"
show "\<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z) : U"
+ proof (rule Prod_formation)
+ show "B(x) : U" using 1 by (rule assms)
+
+ fix y::Term assume 2: "y : B(x)"
+ show "\<Prod>z:C(x)(y). D(x)(y)(z) : U"
proof (rule Prod_formation)
- show "B(x) : U" using 1 by (rule assms)
-
- fix y::Term assume 2: "y : B(x)"
- show "\<Prod>z:C(x)(y). D(x)(y)(z) : U"
- proof (rule Prod_formation)
- show "C x y : U" using 2 by (rule assms)
- show "\<And>z::Term. z : C(x)(y) \<Longrightarrow> D(x)(y)(z) : U" by (rule assms)
- qed
+ show "C x y : U" using 2 by (rule assms)
+ show "\<And>z::Term. z : C(x)(y) \<Longrightarrow> D(x)(y)(z) : U" by (rule assms)
qed
+ qed
qed (rule assms)
-lemma
+lemma curried_type:
fixes
a b A::Term and
B::"Term \<Rightarrow> Term" and
f C::"[Term, Term] \<Rightarrow> Term"
- assumes "\<And>x y::Term. f x y : C x y"
+ assumes "\<And>x y::Term. \<lbrakk>x : A; y : B(x)\<rbrakk> \<Longrightarrow> f x y : C x y"
shows "\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). f x y : \<Prod>x:A. \<Prod>y:B(x). C x y"
proof
fix x::Term
+ assume *: "x : A"
show "\<^bold>\<lambda>y:B(x). f x y : \<Prod>y:B(x). C x y"
- proof
- show "\<And>y. f x y : C x y" by (rule assms)
- qed
+ proof
+ fix y::Term
+ assume **: "y : B(x)"
+ show "f x y : C x y" using * ** by (rule assms)
+ qed
qed
text "Note that the propositions and proofs above often say nothing about the well-formedness of the types, or the well-typedness of the lambdas involved; one has to be very explicit and prove such things separately!
This is the result of the choices made regarding the premises of the type rules."
+text "The following shows that the dependent sum inductor has the type we expect it to have:"
+
+lemma
+ assumes "C: \<Sum>x:A. B(x) \<rightarrow> U"
+ shows "indSum(C) : \<Prod>f:(\<Prod>x:A. \<Prod>y:B(x). C((x,y))). \<Prod>p:(\<Sum>x:A. B(x)). C(p)"
+proof -
+ define F and P where
+ "F \<equiv> \<Prod>x:A. \<Prod>y:B(x). C((x,y))" and
+ "P \<equiv> \<Sum>x:A. B(x)"
+
+ have "\<^bold>\<lambda>f:F. \<^bold>\<lambda>p:P. indSum(C)`f`p : \<Prod>f:F. \<Prod>p:P. C(p)"
+ proof (rule curried_type)
+ fix f p::Term
+ assume "f : F" and "p : P"
+ with assms show "indSum(C)`f`p : C(p)" unfolding F_def P_def ..
+ qed
+
+ then show "indSum(C) : \<Prod>f:F. \<Prod>p:P. C(p)" by simp
+qed
+
text "Polymorphic identity function."
consts Ui::Term