Proof of projection functions now harder. Should look up automation methods.

2 files changed, 15 insertions, 9 deletions

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 7794601..9b7c3e2 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -34,7 +34,7 @@ consts
   is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ :/ _)" [0, 0] 1000)
 
 axiomatization where
-  inhabited_implies_type [intro]: "\<And>a A. a : A \<Longrightarrow> A : U"
+  inhabited_implies_type: "\<And>a A. a : A \<Longrightarrow> A : U"
 
 
 section \<open>Type families\<close>
diff --git a/Sum.thy b/Sum.thy
index 93b1e72..fbfc15a 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -57,10 +57,10 @@ overloading
   fst_nondep \<equiv> fst
 begin
   definition fst_dep :: "[Term, Typefam] \<Rightarrow> Term" where
-    "fst_dep A B \<equiv> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x)"
+    "fst_dep A B \<equiv> \<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x) p"
   
   definition fst_nondep :: "[Term, Term] \<Rightarrow> Term" where
-    "fst_nondep A B \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x)"
+    "fst_nondep A B \<equiv> \<^bold>\<lambda>p: A \<times> B. indSum[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x) p"
 end
 
 overloading
@@ -68,24 +68,30 @@ overloading
   snd_nondep \<equiv> snd
 begin
   definition snd_dep :: "[Term, Typefam] \<Rightarrow> Term" where
-    "snd_dep A B \<equiv> indSum[A,B] (\<lambda>p. B fst[A,B]`p) (\<lambda>x y. y)"
+    "snd_dep A B \<equiv> \<^bold>\<lambda>p: (\<Sum>x:A. B x). indSum[A,B] (\<lambda>p. B fst[A,B]`p) (\<lambda>x y. y) p"
   
   definition snd_nondep :: "[Term, Term] \<Rightarrow> Term" where
-    "snd_nondep A B \<equiv> indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y)"
+    "snd_nondep A B \<equiv> \<^bold>\<lambda>p: A \<times> B. indSum[A, \<lambda>_. B] (\<lambda>_. B) (\<lambda>x y. y) p"
 end
 
 text "Properties of projections:"  
 
 lemma fst_dep_comp:
-  assumes "a : A" and "b : B a"
+  assumes "B: A \<rightarrow> U" and "a : A" and "b : B a"
   shows "fst[A,B]`(a,b) \<equiv> a"
-proof -
-  have "A : U" using assms(1) ..
+proof (unfold fst_dep_def)  (* GOOD AUTOMATION EXAMPLE *)
+  have "\<And>p. p : \<Sum>x:A. B x \<Longrightarrow> indSum[A, B] (\<lambda>_. A) (\<lambda>x y. x) p : A" ..
+  moreover have "(a, b) : \<Sum>x:A. B x" using assms ..
+  then have "fst[A,B]`(a,b) \<equiv> indSum[A, B] (\<lambda>_. A) (\<lambda>x y. x) (a,b)" unfolding fst_dep_def by (simp add: Prod_comp)
+  have "A : U" using assms(2) ..
   then have "\<lambda>_. A: \<Sum>x:A. B x \<rightarrow> U" .
   moreover have "\<And>x y. x : A \<Longrightarrow> (\<lambda>x y. x) x y : A" .
-  ultimately show "fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def using assms by (rule Sum_comp)
+  moreover 
+  ultimately show "fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def using assms by simp
 qed
 
+thm Sum_comp
+
 lemma snd_dep_comp:
   assumes "a : A" and "b : B a"
   shows "snd[A,B]`(a,b) \<equiv> b"