diff options
| author | Josh Chen | 2018-09-20 14:14:17 +0200 |
|---|---|---|
| committer | Josh Chen | 2018-09-20 14:14:17 +0200 |
| commit | 0bceaa97dfc4899ec2489dc3f2cd2ea11f5ae358 (patch) | |
| tree | b57993a0dd66b222ba02e5f1aed62f22bfa9a02f | |
| parent | 19eb191526ed6071ce4dbd44804122d53eea83c9 (diff) | |
Application should bind tighter than composition
Diffstat (limited to '')
| -rw-r--r-- | Equality.thy | 4 | ||||
| -rw-r--r-- | 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" @@ -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) |