tweak mixfix priorities

2 files changed, 16 insertions, 7 deletions

diff --git a/HoTT_Base.thy b/HoTT_Base.thy
index 34474d1..ee36af4 100644
--- a/HoTT_Base.thy
+++ b/HoTT_Base.thy
@@ -66,8 +66,8 @@ where "f: A \<leadsto> B \<equiv> (\<And>x. x: A \<Longrightarrow> f x: B)"
 
 text \<open>We use the notation @{prop "B: A \<leadsto> U i"} to abbreviate type families.\<close>
 
-abbreviation (input) K_combinator :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"  ("^_" [1000])
-where "^A \<equiv> \<lambda>_. A"
+abbreviation (input) K_combinator :: "'a \<Rightarrow> 'b \<Rightarrow> 'a"  ("&_" [0] 3)
+where "&A \<equiv> \<lambda>_. A"
 
 
 section \<open>Named theorems\<close>
diff --git a/Prod.thy b/Prod.thy
index 48f0151..0bd037d 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -96,17 +96,26 @@ in
 end
 \<close>
 
-lemma compose_assoc:
-  assumes "A: U i" and "f: A \<rightarrow> B" and "g: B \<rightarrow> C" and "h: \<Prod>x: C. D x"
-  shows "(h o[B] g) o[A] f \<equiv> h o[A] g o[A] f"
-unfolding compose_def by (derive lems: assms cong)
+lemma compose_type:
+  assumes
+    "A: U i" and "B: U i" and "C: B \<leadsto> U i" and
+    "f: A \<rightarrow> B" and "g: \<Prod>x: B. C x"
+  shows "g o[A] f: \<Prod>x: A. C (f`x)"
+unfolding compose_def by (derive lems: assms)
 
 lemma compose_comp:
   assumes "A: U i" and "\<And>x. x: A \<Longrightarrow> b x: B" and "\<And>x. x: B \<Longrightarrow> c x: C x"
   shows "(\<lambda>x: B. c x) o[A] (\<lambda>x: A. b x) \<equiv> \<lambda>x: A. c (b x)"
 unfolding compose_def by (derive lems: assms cong)
 
-declare compose_comp [comp]
+declare
+  compose_type [intro]
+  compose_comp [comp]
+
+lemma compose_assoc:
+  assumes "A: U i" and "f: A \<rightarrow> B" and "g: B \<rightarrow> C" and "h: \<Prod>x: C. D x"
+  shows "(h o[B] g) o[A] f \<equiv> h o[A] g o[A] f"
+unfolding compose_def by (derive lems: assms cong)
 
 abbreviation id :: "t \<Rightarrow> t" where "id A \<equiv> \<lambda>x: A. x"