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 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'Equality.thy')

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"
-- 
cgit v1.2.3