From 0bceaa97dfc4899ec2489dc3f2cd2ea11f5ae358 Mon Sep 17 00:00:00 2001
From: Josh Chen
Date: Thu, 20 Sep 2018 14:14:17 +0200
Subject: Application should bind tighter than composition

---
 Equality.thy | 4 ++--
 Prod.thy     | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Equality.thy b/Equality.thy
index f639734..05ccbff 100644
--- a/Equality.thy
+++ b/Equality.thy
@@ -35,7 +35,7 @@ Composition function, of type @{term "x =\<^sub>A y \<rightarrow> (y =\<^sub>A z
 
 definition pathcomp :: t where "pathcomp \<equiv> \<^bold>\<lambda>p. ind\<^sub>= (\<lambda>_. \<^bold>\<lambda>q. ind\<^sub>= (\<lambda>x. (refl x)) q) p"
 
-syntax "_pathcomp" :: "[t, t] \<Rightarrow> t"  (infixl "\<bullet>" 120)
+syntax "_pathcomp" :: "[t, t] \<Rightarrow> t"  (infixl "\<bullet>" 110)
 translations "p \<bullet> q" \<rightleftharpoons> "CONST pathcomp`p`q"
 
 lemma pathcomp_type:
@@ -189,7 +189,7 @@ schematic_goal functions_are_functorial:
     "x: A" "y: A" "z: A"
     "p: x =\<^sub>A y" "q: y =\<^sub>A z"
   shows
-    1: "?a: ap\<^sub>f`(p \<bullet> q) =[?A] (ap\<^sub>f`p) \<bullet> (ap\<^sub>f`q)" and
+    1: "?a: ap\<^sub>f`(p \<bullet> q) =[?A] ap\<^sub>f`p \<bullet> ap\<^sub>f`q" and
     2: "?b: ap\<^sub>f`(p\<inverse>) =[?B] (ap\<^sub>f`p)\<inverse>" and
     3: "?c: ap\<^sub>g`(ap\<^sub>f`p) =[?C] ap[g \<circ> f]`p" and
     4: "?d: ap[id]`p =[?D] p"
diff --git a/Prod.thy b/Prod.thy
index a37fdd6..8d840bd 100644
--- a/Prod.thy
+++ b/Prod.thy
@@ -17,7 +17,7 @@ section \<open>Basic definitions\<close>
 axiomatization
   Prod   :: "[t, tf] \<Rightarrow> t" and
   lambda :: "(t \<Rightarrow> t) \<Rightarrow> t"  (binder "\<^bold>\<lambda>" 30) and
-  appl   :: "[t, t] \<Rightarrow> t"  (infixl "`" 105)  \<comment> \<open>Application binds tighter than abstraction.\<close>
+  appl   :: "[t, t] \<Rightarrow> t"  ("(1_`_)" [120, 121] 120)  \<comment> \<open>Application binds tighter than abstraction.\<close>
 
 syntax
   "_prod" :: "[idt, t, t] \<Rightarrow> t"        ("(3\<Prod>_: _./ _)" 30)
-- 
cgit v1.2.3