tweak mixfix priorities

1 files changed, 14 insertions, 5 deletions

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"