λC:bishop_set.λU:C square → Prop.
λx:C square. U 〈snd x,fst x〉.
-notation < "s \sup (-1)" left associative with precedence 70
- for @{ 'invert $s }.
-notation < "s \sup (-1) x" left associative with precedence 70
+notation < "s \sup (-1)" with precedence 70 for @{ 'invert $s }.
+notation < "s \sup (-1) x" with precedence 70
for @{ 'invert_appl $s $x}.
-notation > "'inv'" right associative with precedence 70
- for @{ 'invert_symbol }.
+notation > "'inv'" with precedence 70 for @{ 'invert_symbol }.
interpretation "relation invertion" 'invert a = (invert_bs_relation _ a).
interpretation "relation invertion" 'invert_symbol = (invert_bs_relation _).
interpretation "relation invertion" 'invert_appl a x = (invert_bs_relation _ a x).