Replace ugly |v| notation with /

For comma categories
Don't autounfold functors from terminal category

This way, the notations for comma categories are slightly prettier after
[simpl].