Nondependent function arrow should bind tighter than the Pi former, but looser than equality.

2 files changed, 48 insertions, 26 deletions

diff --git a/HoTT.thy b/HoTT.thy
index ee81ba4..c1c6e72 100644
--- a/HoTT.thy
+++ b/HoTT.thy
@@ -30,7 +30,7 @@ theorem equal_type_element:
   assumes "A \<equiv> B" and "x : A"
   shows "x : B" using assms by simp
 
-lemmas type_equality [intro] = equal_types equal_types[rotated] equal_type_element equal_type_element[rotated]
+lemmas type_equality [intro, simp] = equal_types equal_types[rotated] equal_type_element equal_type_element[rotated]
 
 section \<open>Type families\<close>
 text "Type families are implemented using meta-level lambda expressions \<open>P::Term \<Rightarrow> Term\<close> that further satisfy the following property."
@@ -46,14 +46,18 @@ 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>_:_./ _)" 30)
-  "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3\<^bold>\<lambda>_:_./ _)" 30)
+  "_PROD" :: "[idt, Term, Term] \<Rightarrow> Term"          ("(3\<Prod>_:_./ _)" 30)
+  "_LAMBDA" :: "[idt, Term, Term] \<Rightarrow> Term"        ("(3\<^bold>\<lambda>_:_./ _)" 30)
+  "_PROD_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"    ("(3PROD _:_./ _)" 30)
+  "_LAMBDA_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3%%_:_./ _)" 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. *)
+  "PROD x:A. B" \<rightharpoonup> "CONST Prod A (\<lambda>x. B)"
+  "%%x:A. b" \<rightharpoonup> "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>" 10)
+abbreviation Function :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<rightarrow>" 80)
   where "A\<rightarrow>B \<equiv> \<Prod>_:A. B"
 
 axiomatization
@@ -71,7 +75,7 @@ and
 and
   Prod_uniq [simp]: "\<And>A f::Term. \<^bold>\<lambda>x:A. (f`x) \<equiv> f"
 
-lemmas Prod_formation = Prod_form Prod_form[rotated]
+lemmas Prod_formation [intro] = Prod_form Prod_form[rotated]
 
 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)."
 
@@ -80,11 +84,13 @@ subsection \<open>Dependent pair/sum\<close>
 axiomatization
   Sum :: "[Term, Term \<Rightarrow> Term] \<Rightarrow> Term"
 syntax
-  "_Sum" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3\<Sum>_:_./ _)" 20)
+  "_SUM" :: "[idt, Term, Term] \<Rightarrow> Term"        ("(3\<Sum>_:_./ _)" 20)
+  "_SUM_ASCII" :: "[idt, Term, Term] \<Rightarrow> Term"  ("(3SUM _:_./ _)" 20)
 translations
   "\<Sum>x:A. B" \<rightleftharpoons> "CONST Sum A (\<lambda>x. B)"
+  "SUM x:A. B" \<rightharpoonup> "CONST Sum A (\<lambda>x. B)"
 
-abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"   (infixr "\<times>" 50)
+abbreviation Pair :: "[Term, Term] \<Rightarrow> Term"  (infixr "\<times>" 50)
   where "A\<times>B \<equiv> \<Sum>_:A. B"
 
 axiomatization
@@ -102,7 +108,7 @@ and
 and
   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]
+lemmas Sum_formation [intro] = Sum_form Sum_form[rotated]
 
 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."
@@ -145,35 +151,51 @@ subsection \<open>Equality type\<close>
 axiomatization
   Equal :: "[Term, Term, Term] \<Rightarrow> Term"
 syntax
-  "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term"  ("(3_ =\<^sub>_/ _)")
+  "_EQUAL" :: "[Term, Term, Term] \<Rightarrow> Term"        ("(3_ =\<^sub>_/ _)" [101, 101] 100)
+  "_EQUAL_ASCII" :: "[Term, Term, Term] \<Rightarrow> Term"  ("(3_ =[_]/ _)" [101, 101] 100)
 translations
   "a =\<^sub>A b" \<rightleftharpoons> "CONST Equal A a b"
+  "a =[A] b" \<rightharpoonup> "CONST Equal A a b"
 
 axiomatization
   refl :: "Term \<Rightarrow> Term" and
-  indEqual :: "([Term, Term, Term] \<Rightarrow> Term) \<Rightarrow> Term"
+  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 p::Term. \<lbrakk>x : A; y : A; p : x =\<^sub>A y\<rbrakk> \<Longrightarrow> C(x)(y)(p) : U;
-      f : \<Prod>x:A. C(x)(x)(refl(x));
-      a : A;
-      b : A;
-      p : a =\<^sub>A b\<rbrakk> \<Longrightarrow> indEqual(C)`f`a`b`p : C(a)(b)(p)"
+    "\<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>(C::[Term, Term, Term] \<Rightarrow> Term) (f::Term) (a::Term). indEqual(C)`f`a`a`refl(a) \<equiv> f`a"
+    "\<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 "Inverse"
+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"
+
+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)))"
+
+lemma compose'_comp: "a : A \<Longrightarrow> compose'[A]`a`a`refl(a)`a`refl(a) \<equiv> refl(a)" unfolding compose'_def by simp
 
-definition inv :: "Term \<Rightarrow> Term"  ("(_\<^sup>-\<^sup>1)")
-  where "inv \<equiv> " (* Tra la la.. *)
 
 end
 
diff --git a/HoTT_Theorems.thy b/HoTT_Theorems.thy
index 52e1b32..5578bf8 100644
--- a/HoTT_Theorems.thy
+++ b/HoTT_Theorems.thy
@@ -57,11 +57,11 @@ proposition wellformed_currying:
     "B: A \<rightarrow> U" and
     "\<And>x::Term. C(x): B(x) \<rightarrow> U"
   shows "\<Prod>x:A. \<Prod>y:B(x). C x y : U"
-proof (rule Prod_formation)
+proof
   fix x::Term
   assume *: "x : A"
   show "\<Prod>y:B(x). C x y : U"
-  proof (rule Prod_formation)
+  proof
     show "B(x) : U" using * by (rule assms)
   qed (rule assms)
 qed (rule assms)
@@ -78,15 +78,15 @@ proposition triply_curried:
     "\<And>x y::Term. y : B(x) \<Longrightarrow> C(x)(y) : U" and
     "\<And>x y z::Term. z : C(x)(y) \<Longrightarrow> D(x)(y)(z) : U"
   shows "\<Prod>x:A. \<Prod>y:B(x). \<Prod>z:C(x)(y). D(x)(y)(z) : U"
-proof (rule Prod_formation)
+proof
   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)
+  proof
     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)
+    proof
       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