+notation > "hovbox(a ∨ b)" left associative with precedence 49
+for @{ 'oa_join (λx__:bool.match x__ with [ true ⇒ $a | false ⇒ $b ]) }.
+notation > "hovbox(∨ f)" non associative with precedence 59
+for @{ 'oa_join $f }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (ident i ∈ I) break term 90 p)" non associative with precedence 49
+for @{ 'oa_join (λ${ident i}:$I.$p) }.
+notation < "hovbox(mstyle scriptlevel 1 scriptsizemultiplier 1.7 (∨) \below (\emsp) \nbsp term 90 p)" non associative with precedence 49
+for @{ 'oa_join (λ${ident i}.($p $_)) }.
+notation < "hovbox(a ∨ b)" left associative with precedence 49
+for @{ 'oa_join (λ${ident i}:$_.match $i with [ true ⇒ $a | false ⇒ $b ]) }.
+
+interpretation "o-algebra join" 'oa_join \eta.f = (oa_join _ _ f).