Proved that the inductor on Sum has the correct type.

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