-interpretation "setoid3 eq" 'eq x y = (eq_rel3 _ (eq3 _) x y).
-interpretation "setoid2 eq" 'eq x y = (eq_rel2 _ (eq2 _) x y).
-interpretation "setoid1 eq" 'eq x y = (eq_rel1 _ (eq1 _) x y).
-interpretation "setoid eq" 'eq x y = (eq_rel _ (eq _) x y).
-interpretation "setoid3 symmetry" 'invert r = (sym3 ____ r).
-interpretation "setoid2 symmetry" 'invert r = (sym2 ____ r).
-interpretation "setoid1 symmetry" 'invert r = (sym1 ____ r).
-interpretation "setoid symmetry" 'invert r = (sym ____ r).
+interpretation "setoid3 eq" 'eq t x y = (eq_rel3 ? (eq3 t) x y).
+interpretation "setoid2 eq" 'eq t x y = (eq_rel2 ? (eq2 t) x y).
+interpretation "setoid1 eq" 'eq t x y = (eq_rel1 ? (eq1 t) x y).
+interpretation "setoid eq" 'eq t x y = (eq_rel ? (eq t) x y).
+
+notation > "hvbox(a break =_12 b)" non associative with precedence 45
+for @{ eq_rel2 (carr2 (setoid2_of_setoid1 ?)) (eq2 (setoid2_of_setoid1 ?)) $a $b }.
+notation > "hvbox(a break =_0 b)" non associative with precedence 45
+for @{ eq_rel ? (eq ?) $a $b }.
+notation > "hvbox(a break =_1 b)" non associative with precedence 45
+for @{ eq_rel1 ? (eq1 ?) $a $b }.
+notation > "hvbox(a break =_2 b)" non associative with precedence 45
+for @{ eq_rel2 ? (eq2 ?) $a $b }.
+notation > "hvbox(a break =_3 b)" non associative with precedence 45
+for @{ eq_rel3 ? (eq3 ?) $a $b }.
+
+interpretation "setoid3 symmetry" 'invert r = (sym3 ???? r).
+interpretation "setoid2 symmetry" 'invert r = (sym2 ???? r).
+interpretation "setoid1 symmetry" 'invert r = (sym1 ???? r).
+interpretation "setoid symmetry" 'invert r = (sym ???? r).