- [x] sym(sym(x)) = x - [ ] sym(ap_ap(x)) = ap_ap(sym(x)) - [ ] sym(refl_refl) = refl_refl (special case of the previous) - [ ] braid equation: sym(ap_sym(sym(x))) = ap_sym(sym(ap_sym(x))) - [ ] naturality: sym_{B o f}^{d}(x) = sym_B^{AP (AP f) d}(x)