Type rules now have \"all\" premises explicitly stated, matching the formulation in the HoTT book.

6 files changed, 215 insertions, 135 deletions

diff --git a/Equal.thy b/Equal.thy
index b9f676f..12ed272 100644
--- a/Equal.thy
+++ b/Equal.thy
@@ -1,81 +1,85 @@
+(*  Title:  HoTT/Equal.thy
+    Author: Josh Chen
+    Date:   Jun 2018
+
+Equality type.
+*)
+
 theory Equal
-  imports HoTT_Base Prod
+  imports HoTT_Base
 
 begin
 
-subsection \<open>Equality type\<close>
-  
-    axiomatization
-      Equal :: "[Term, Term, Term] \<Rightarrow> Term"
-
-    syntax
-      "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term"        ("(3_ =\<^sub>_/ _)" [101, 101] 100)
-      "_EQUAL_ASCII" :: "[Term, Term, Term] \<Rightarrow> Term"  ("(3_ =[_]/ _)" [101, 0, 101] 100)
-    translations
-      "a =[A] b" \<rightleftharpoons> "CONST Equal A a b"
-      "a =\<^sub>A b" \<rightharpoonup> "CONST Equal A a b"
-    
-    axiomatization
-      refl :: "Term \<Rightarrow> Term"  ("(refl'(_'))") and
-      indEqual :: "[Term, [Term, Term, Term] \<Rightarrow> Term] \<Rightarrow> Term"  ("(indEqual[_])")
-    where
-      Equal_form: "\<And>A a b::Term. \<lbrakk>A : U; a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U"
-      (* Should I write a permuted version \<open>\<lbrakk>A : U; b : A; a : A\<rbrakk> \<Longrightarrow> \<dots>\<close>? *)
-    and
-      Equal_intro [intro]: "\<And>A x::Term. x : A \<Longrightarrow> refl(x) : x =\<^sub>A x"
-    and
-      Equal_elim [elim]:
-        "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term) (b::Term) (p::Term).
-          \<lbrakk> \<And>x y::Term. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<rightarrow> U;
-            f : \<Prod>x:A. C(x)(x)(refl(x));
-            a : A;
-            b : A;
-            p : a =\<^sub>A b \<rbrakk>
-        \<Longrightarrow> indEqual[A](C)`f`a`b`p : C(a)(b)(p)"
-    and
-      Equal_comp [simp]:
-        "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term). indEqual[A](C)`f`a`a`refl(a) \<equiv> f`a"
-    
-    lemmas Equal_formation [intro] = Equal_form Equal_form[rotated 1] Equal_form[rotated 2]
-    
-    subsubsection \<open>Properties of equality\<close>
-    
-    text "Symmetry/Path inverse"
-    
-    definition inv :: "[Term, Term, Term] \<Rightarrow> Term"  ("(1inv[_,/ _,/ _])")
-      where "inv[A,x,y] \<equiv> indEqual[A](\<lambda>x y _. y =\<^sub>A x)`(\<^bold>\<lambda>x:A. refl(x))`x`y"
-    
-    lemma inv_comp: "\<And>A a::Term. a : A \<Longrightarrow> inv[A,a,a]`refl(a) \<equiv> refl(a)" unfolding inv_def by simp
-    
-    text "Transitivity/Path composition"
-    
-    \<comment> \<open>"Raw" composition function\<close>
-    definition compose' :: "Term \<Rightarrow> Term"  ("(1compose''[_])")
-      where "compose'[A] \<equiv> indEqual[A](\<lambda>x y _. \<Prod>z:A. \<Prod>q: y =\<^sub>A z. x =\<^sub>A z)`(indEqual[A](\<lambda>x z _. x =\<^sub>A z)`(\<^bold>\<lambda>x:A. refl(x)))"
-    
-    \<comment> \<open>"Natural" composition function\<close>
-    abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1compose[_,/ _,/ _,/ _])")
-      where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. \<^bold>\<lambda>q:y =\<^sub>A z. compose'[A]`x`y`p`z`q"
-    
-    (**** GOOD CANDIDATE FOR AUTOMATION ****)
-    lemma compose_comp:
-      assumes "a : A"
-      shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" using assms Equal_intro[OF assms] unfolding compose'_def by simp
-    
-    text "The above proof is a good candidate for proof automation; in particular we would like the system to be able to automatically find the conditions of the \<open>using\<close> clause in the proof.
-    This would likely involve something like:
-      1. Recognizing that there is a function application that can be simplified.
-      2. Noting that the obstruction to applying \<open>Prod_comp\<close> is the requirement that \<open>refl(a) : a =\<^sub>A a\<close>.
-      3. Obtaining such a condition, using the known fact \<open>a : A\<close> and the introduction rule \<open>Equal_intro\<close>."
-    
-    lemmas Equal_simps [simp] = inv_comp compose_comp
-    
-    subsubsection \<open>Pretty printing\<close>
-    
-    abbreviation inv_pretty :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1_\<^sup>-\<^sup>1[_, _, _])" 500)
-      where "p\<^sup>-\<^sup>1[A,x,y] \<equiv> inv[A,x,y]`p"
-    
-    abbreviation compose_pretty :: "[Term, Term, Term, Term, Term, Term] \<Rightarrow> Term"  ("(1_ \<bullet>[_, _, _, _]/ _)")
-      where "p \<bullet>[A,x,y,z] q \<equiv> compose[A,x,y,z]`p`q"
+axiomatization
+  Equal :: "[Term, Term, Term] \<Rightarrow> Term" and
+  refl :: "Term \<Rightarrow> Term"  ("(refl'(_'))" 1000) and
+  indEqual :: "[Term, [Term, Term, Term] \<Rightarrow> Term] \<Rightarrow> Term"  ("(indEqual[_])")
+
+syntax
+  "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term"        ("(3_ =\<^sub>_/ _)" [101, 101] 100)
+  "_EQUAL_ASCII" :: "[Term, Term, Term] \<Rightarrow> Term"  ("(3_ =[_]/ _)" [101, 0, 101] 100)
+translations
+  "a =[A] b" \<rightleftharpoons> "CONST Equal A a b"
+  "a =\<^sub>A b" \<rightharpoonup> "CONST Equal A a b"
+
+axiomatization where
+  Equal_form: "\<And>A a b::Term. \<lbrakk>A : U; a : A; b : A\<rbrakk> \<Longrightarrow> a =\<^sub>A b : U"
+  (* Should I write a permuted version \<open>\<lbrakk>A : U; b : A; a : A\<rbrakk> \<Longrightarrow> \<dots>\<close>? *)
+and
+  Equal_intro [intro]: "\<And>A x::Term. x : A \<Longrightarrow> refl(x) : x =\<^sub>A x"
+and
+  Equal_elim [elim]:
+    "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term) (b::Term) (p::Term).
+      \<lbrakk> \<And>x y::Term. \<lbrakk>x : A; y : A\<rbrakk> \<Longrightarrow> C(x)(y): x =\<^sub>A y \<rightarrow> U;
+        f : \<Prod>x:A. C(x)(x)(refl(x));
+        a : A;
+        b : A;
+        p : a =\<^sub>A b \<rbrakk>
+    \<Longrightarrow> indEqual[A](C)`f`a`b`p : C(a)(b)(p)"
+and
+  Equal_comp [simp]:
+    "\<And>(A::Term) (C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term). indEqual[A](C)`f`a`a`refl(a) \<equiv> f`a"
+
+lemmas Equal_formation [intro] = Equal_form Equal_form[rotated 1] Equal_form[rotated 2]
+
+subsubsection \<open>Properties of equality\<close>
+
+text "Symmetry/Path inverse"
+
+definition inv :: "[Term, Term, Term] \<Rightarrow> Term"  ("(1inv[_,/ _,/ _])")
+  where "inv[A,x,y] \<equiv> indEqual[A](\<lambda>x y _. y =\<^sub>A x)`(\<^bold>\<lambda>x:A. refl(x))`x`y"
+
+lemma inv_comp: "\<And>A a::Term. a : A \<Longrightarrow> inv[A,a,a]`refl(a) \<equiv> refl(a)" unfolding inv_def by simp
+
+text "Transitivity/Path composition"
+
+\<comment> \<open>"Raw" composition function\<close>
+definition compose' :: "Term \<Rightarrow> Term"  ("(1compose''[_])")
+  where "compose'[A] \<equiv> indEqual[A](\<lambda>x y _. \<Prod>z:A. \<Prod>q: y =\<^sub>A z. x =\<^sub>A z)`(indEqual[A](\<lambda>x z _. x =\<^sub>A z)`(\<^bold>\<lambda>x:A. refl(x)))"
+
+\<comment> \<open>"Natural" composition function\<close>
+abbreviation compose :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1compose[_,/ _,/ _,/ _])")
+  where "compose[A,x,y,z] \<equiv> \<^bold>\<lambda>p:x =\<^sub>A y. \<^bold>\<lambda>q:y =\<^sub>A z. compose'[A]`x`y`p`z`q"
+
+(**** GOOD CANDIDATE FOR AUTOMATION ****)
+lemma compose_comp:
+  assumes "a : A"
+  shows "compose[A,a,a,a]`refl(a)`refl(a) \<equiv> refl(a)" using assms Equal_intro[OF assms] unfolding compose'_def by simp
+
+text "The above proof is a good candidate for proof automation; in particular we would like the system to be able to automatically find the conditions of the \<open>using\<close> clause in the proof.
+This would likely involve something like:
+  1. Recognizing that there is a function application that can be simplified.
+  2. Noting that the obstruction to applying \<open>Prod_comp\<close> is the requirement that \<open>refl(a) : a =\<^sub>A a\<close>.
+  3. Obtaining such a condition, using the known fact \<open>a : A\<close> and the introduction rule \<open>Equal_intro\<close>."
+
+lemmas Equal_simps [simp] = inv_comp compose_comp
+
+subsubsection \<open>Pretty printing\<close>
+
+abbreviation inv_pretty :: "[Term, Term, Term, Term] \<Rightarrow> Term"  ("(1_\<^sup>-\<^sup>1[_, _, _])" 500)
+  where "p\<^sup>-\<^sup>1[A,x,y] \<equiv> inv[A,x,y]`p"
+
+abbreviation compose_pretty :: "[Term, Term, Term, Term, Term, Term] \<Rightarrow> Term"  ("(1_ \<bullet>[_, _, _, _]/ _)")
+  where "p \<bullet>[A,x,y,z] q \<equiv> compose[A,x,y,z]`p`q"
 
 end
\ No newline at end of file
diff --git a/HoTT.thy b/HoTT.thy
new file mode 100644
index 0000000..405364e
--- /dev/null
+++ b/HoTT.thy
@@ -0,0 +1,15 @@
+(*  Title:  HoTT/HoTT.thy
+    Author: Josh Chen
+
+Load all the component modules for the HoTT logic.
+*)
+
+theory HoTT imports
+  HoTT_Base
+  Prod Sum
+
+begin
+
+\<comment> \<open>Maybe tactic setup can go in here?\<close>
+
+end
\ No newline at end of file
diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 9650c4c..9b422c4 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -1,5 +1,6 @@
 (*  Title:  HoTT/HoTT_Base.thy
     Author: Josh Chen
+    Date:   Jun 2018
 
 Basic setup and definitions of a homotopy type theory object logic.
 *)
@@ -9,23 +10,43 @@ theory HoTT_Base
 
 begin
 
-section \<open>Basic definitions\<close>
+section \<open>Setup\<close>
 
-text "A single meta-level type \<open>Term\<close> suffices to implement the object-level types and terms.
-We do not implement universes, but simply follow the informal notation in the HoTT book."
+text "Set up type checking routines, proof methods etc."
+
+
+section \<open>Metalogical definitions\<close>
+
+text "A single meta-type \<open>Term\<close> suffices to implement the object-logic types and terms.
+Our implementation does not have universes, and we simply use \<open>a : U\<close> as a convenient shorthand meaning ``\<open>a\<close> is a type''."
 
 typedecl Term
 
+
 section \<open>Judgments\<close>
 
 consts
-is_a_type :: "Term \<Rightarrow> prop"           ("(_ : U)" [0] 1000)
-is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(3_ :/ _)" [0, 0] 1000)
+is_a_type :: "Term \<Rightarrow> prop"           ("(1_ :/ U)" [0] 1000)
+is_of_type :: "[Term, Term] \<Rightarrow> prop"  ("(1_ :/ _)" [0, 0] 1000)
+
+
+section \<open>Type families\<close>
+
+text "A (one-variable) type family is a meta lambda term \<open>P :: Term \<Rightarrow> Term\<close> that further satisfies the following property."
+
+type_synonym Typefam = "Term \<Rightarrow> Term"
+
+abbreviation is_type_family :: "[Typefam, Term] \<Rightarrow> prop"  ("(3_:/ _ \<rightarrow> U)")
+  where "P: A \<rightarrow> U \<equiv> (\<And>x. x : A \<Longrightarrow> P x : U)"
+
+text "There is an obvious generalization to multivariate type families, but implementing such an abbreviation involves writing ML and is for the moment not really crucial."
 
 
 section \<open>Definitional equality\<close>
 
-text "We use the Pure equality \<open>\<equiv>\<close> for definitional/judgmental equality of types and terms in our theory."
+text "The Pure equality \<open>\<equiv>\<close> is used for definitional aka judgmental equality of types and terms."
+
+\<comment> \<open>Do these ever need to be used?
 
 theorem equal_types:
   assumes "A \<equiv> B" and "A : U"
@@ -35,18 +56,11 @@ theorem equal_type_element:
   assumes "A \<equiv> B" and "x : A"
   shows "x : B" using assms by simp
 
-lemmas type_equality [intro, simp] =
+lemmas type_equality =
   equal_types
   equal_types[rotated]
   equal_type_element
   equal_type_element[rotated]
-
-
-section \<open>Type families\<close>
-
-text "A type family is a meta lambda term \<open>P :: Term \<Rightarrow> Term\<close> that further satisfies the following property."
-
-abbreviation is_type_family :: "[Term \<Rightarrow> Term, Term] \<Rightarrow> prop"  ("(3_:/ _ \<rightarrow> U)")
-  where "P: A \<rightarrow> U \<equiv> (\<And>x. x : A \<Longrightarrow> P(x) : U)"
+\<close>
 
 end
\ No newline at end of file
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy
index 95f1d0c..2c2a31d 100644
--- a/HoTT_Theorems.thy
+++ b/HoTT_Theorems.thy
@@ -1,5 +1,6 @@
 theory HoTT_Theorems
   imports HoTT
+
 begin
 
 text "A bunch of theorems and other statements for sanity-checking, as well as things that should be automatically simplified.
@@ -9,8 +10,7 @@ Things that *should* be automated:
   \<bullet> Checking that the argument to a (dependent/non-dependent) function matches the type? Also the arguments to a pair?"
 
 \<comment> \<open>Turn on trace for unification and the simplifier, for debugging.\<close>
-declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=1]]
-
+declare[[unify_trace_simp, unify_trace_types, simp_trace, simp_trace_depth_limit=5]]
 
 section \<open>\<Prod> type\<close>
 
@@ -22,17 +22,18 @@ 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" ..
+  assume "A \<equiv> B"
+  then have *: "A\<rightarrow>A \<equiv> B\<rightarrow>A" by simp
+
+  have "\<^bold>\<lambda>x:A. x : A\<rightarrow>A" ..
+  with * show "\<^bold>\<lambda>x:A. x : B\<rightarrow>A" by simp
 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" .. 
+  then show "\<^bold>\<lambda>y:B. a : B \<rightarrow> A" ..
 qed
 
 
@@ -42,7 +43,15 @@ proposition "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. x)`a \<equiv> a" by
 
 text "Currying:"
 
-lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B. y)`a`b \<equiv> b" by simp
+term "lambda A (\<lambda>x. \<^bold>\<lambda>y:B(x). y)"
+
+thm Prod_comp[where ?B = "\<lambda>x. \<Prod>y:B(x). B(x)"]
+
+lemma "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)`a \<equiv> \<^bold>\<lambda>y:B(a). y"
+proof (rule Prod_comp[where ?B = "\<lambda>x. \<Prod>y:B(x). B(x)"])
+  show "\<And>x. a : A \<Longrightarrow> x : A \<Longrightarrow> \<^bold>\<lambda>y:B x. y : B x \<rightarrow> B x"
+
+lemma "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). y)`a`b \<equiv> b"  by simp
 
 lemma "a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. \<^bold>\<lambda>y:B(x). f x y)`a \<equiv> \<^bold>\<lambda>y:B(a). f a y" by simp
 
diff --git a/Prod.thy b/Prod.thy
index 9ecab4d..113998e 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -1,5 +1,6 @@
 (*  Title:  HoTT/Prod.thy
     Author: Josh Chen
+    Date:   Jun 2018
 
 Dependent product (function) type for the HoTT logic.
 *)
@@ -10,8 +11,9 @@ theory Prod
 begin
 
 axiomatization
-  Prod :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
+  Prod :: "[Term, Typefam] \<Rightarrow> Term" and
   lambda :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
+  \<comment> \<open>Application binds tighter than abstraction.\<close>
   appl :: "[Term, Term] \<Rightarrow> Term"  (infixl "`" 60)
 
 syntax
@@ -29,15 +31,20 @@ translations
 
 \<comment> \<open>Type rules\<close>
 axiomatization where
-  Prod_form [intro]: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B(x) : U"
+  Prod_form [intro]: "\<And>A B. \<lbrakk>A : U; B : A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Prod>x:A. B x : U"
 and
-  Prod_intro [intro]: "\<And>A B b. (\<And>x. x : A \<Longrightarrow> b(x) : B(x)) \<Longrightarrow> \<^bold>\<lambda>x:A. b(x) : \<Prod>x:A. B(x)"
+  Prod_intro [intro]: "\<And>A B b. (\<And>x. x : A \<Longrightarrow> b x : B x) \<Longrightarrow> \<^bold>\<lambda>x:A. b x : \<Prod>x:A. B x"
 and
-  Prod_elim [elim]: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B(x); a : A\<rbrakk> \<Longrightarrow> f`a : B(a)"
+  Prod_elim [elim]: "\<And>A B f a. \<lbrakk>f : \<Prod>x:A. B x; a : A\<rbrakk> \<Longrightarrow> f`a : B a"
 and
-  Prod_comp [simp]: "\<And>A b a. a : A \<Longrightarrow> (\<^bold>\<lambda>x:A. b(x))`a \<equiv> b(a)"
+  Prod_comp [simp]: "\<And>A B b a. \<lbrakk>\<And>x. x : A \<Longrightarrow> b x : B x; a : A\<rbrakk> \<Longrightarrow> (\<^bold>\<lambda>x:A. b x)`a \<equiv> b a"
 and
-  Prod_uniq [simp]: "\<And>A f. \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
+  Prod_uniq [simp]: "\<And>A B f. f : \<Prod>x:A. B x \<Longrightarrow> \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
+
+\<comment> \<open>The funny thing about the first premises of the computation and uniqueness rules is that they introduce a variable B that doesn't actually explicitly appear in the statement of the conclusion.
+In a sense, they say something like "if this condition holds for some type family B... (then we can apply the rule)".
+This forces the theorem prover to search for a suitable B. Is this additional overhead necessary?
+It *is* a safety check for well-formedness...\<close>
 
 text "Note that the syntax \<open>\<^bold>\<lambda>\<close> (bold lambda) used for dependent functions clashes with the proof term syntax (cf. \<section>2.5.2 of the Isabelle/Isar Implementation)."
 
diff --git a/Sum.thy b/Sum.thy
index e34749a..8dab3e8 100644
--- a/Sum.thy
+++ b/Sum.thy
@@ -1,5 +1,6 @@
 (*  Title:  HoTT/Sum.thy
     Author: Josh Chen
+    Date:   Jun 2018
 
 Dependent sum type.
 *)
@@ -10,9 +11,9 @@ theory Sum
 begin
 
 axiomatization
-  Sum :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term" and
+  Sum :: "[Term, Typefam] \<Rightarrow> Term" and
   pair :: "[Term, Term] \<Rightarrow> Term"  ("(1'(_,/ _'))") and
-  indSum :: "(Term \<Rightarrow> Term) \<Rightarrow> Term"
+  indSum :: "[Term, Typefam, Typefam, [Term, Term] \<Rightarrow> Term] \<Rightarrow> Term"  ("(1indSum[_,/ _])")
 
 syntax
   "_SUM" :: "[idt, Term, Term] \<Rightarrow> Term"        ("(3\<Sum>_:_./ _)" 20)
@@ -23,25 +24,29 @@ translations
   "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)"
 
 axiomatization where
-  Sum_form [intro]: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B(x) : U"
+  Sum_form [intro]: "\<And>A B. \<lbrakk>A : U; B: A \<rightarrow> U\<rbrakk> \<Longrightarrow> \<Sum>x:A. B x : U"
 and
-  Sum_intro [intro]: "\<And>A B a b. \<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> (a, b) : \<Sum>x:A. B(x)"
+  Sum_intro [intro]: "\<And>A B a b. \<lbrakk>B: A \<rightarrow> U; a : A; b : B a\<rbrakk> \<Longrightarrow> (a,b) : \<Sum>x:A. B x"
 and
-  Sum_elim [elim]: "\<And>A B C f p.
-    \<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)"
+  Sum_elim [elim]: "\<And>A B C f p. \<lbrakk>
+    C: \<Sum>x:A. B x \<rightarrow> U;
+    \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y);
+    p : \<Sum>x:A. B x
+    \<rbrakk> \<Longrightarrow> (indSum[A,B] 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"
-
-text "We choose to formulate the elimination rule by using the object-level function type and function application as much as possible.
-Hence only the type family \<open>C\<close> is left as a meta-level argument to the inductor indSum."
+  Sum_comp [simp]: "\<And>A B C f a b. \<lbrakk>
+    C: \<Sum>x:A. B x \<rightarrow> U;
+    \<And>x y. \<lbrakk>x : A; y : B x\<rbrakk> \<Longrightarrow> f x y : C (x,y);
+    a : A;
+    b : B a
+    \<rbrakk> \<Longrightarrow> (indSum[A,B] C f)`(a,b) \<equiv> f a b"
 
 \<comment> \<open>Nondependent pair\<close>
 abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
-  where "A\<times>B \<equiv> \<Sum>_:A. B"
+  where "A \<times> B \<equiv> \<Sum>_:A. B"
+
 
-subsubsection \<open>Projections\<close>
+section \<open>Projections\<close>
 
 consts
   fst :: "[Term, 'a] \<Rightarrow> Term"  ("(1fst[/_,/ _])")
@@ -49,30 +54,56 @@ consts
 
 overloading
   fst_dep \<equiv> fst
-  snd_dep \<equiv> snd
   fst_nondep \<equiv> fst
-  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)"
-  
-  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)"
+  definition fst_dep :: "[Term, Typefam] \<Rightarrow> Term" where
+    "fst_dep A B \<equiv> indSum[A,B] (\<lambda>_. A) (\<lambda>x y. x)"
   
   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[A, \<lambda>_. B] (\<lambda>_. A) (\<lambda>x y. x)"
+end
+
+overloading
+  snd_dep \<equiv> snd
+  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)"
   
   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[A, \<lambda>_. B] (\<lambda>p. B((fst A B)`p)) (\<lambda>x y. y)"
 end
 
-text "Simplification rules for the projections:"
-
-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
-lemma snd_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b" unfolding snd_dep_def by simp
-
-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
+text "Simplification rules:"
+
+lemma fst_dep_comp:
+  assumes "a : A" and "b : B(a)"
+  shows "fst[A,B]`(a,b) \<equiv> a"
+proof -
+  show "fst[A,B]`(a,b) \<equiv> a" unfolding fst_dep_def using assms by simp
+qed
+
+lemma snd_dep_comp: "\<lbrakk>a : A; b : B(a)\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b"
+proof -
+  assume "a : A" and "b : B(a)"
+  then have "(a, b) : \<Sum>x:A. B(x)" ..
+  then show "snd[A,B]`(a,b) \<equiv> b" unfolding snd_dep_def by simp
+qed
+
+lemma fst_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> fst[A,B]`(a,b) \<equiv> a"
+proof -
+  assume "a : A" and "b : B"
+  then have "(a, b) : A \<times> B" ..
+  then show "fst[A,B]`(a,b) \<equiv> a" unfolding fst_nondep_def by simp
+qed
+
+lemma snd_nondep_comp: "\<lbrakk>a : A; b : B\<rbrakk> \<Longrightarrow> snd[A,B]`(a,b) \<equiv> b"
+proof -
+  assume "a : A" and "b : B"
+  then have "(a, b) : A \<times> B" ..
+  then show "snd[A,B]`(a,b) \<equiv> b" unfolding snd_nondep_def by simp
+qed
+
+lemmas proj_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp
 
-lemmas fst_snd_simps [simp] = fst_dep_comp snd_dep_comp fst_nondep_comp snd_nondep_comp
 end
\ No newline at end of file