The supposed arbitrariness of some types having strict eta and others
not has been mentioned at least twice.  However, I don't find it
arbitrary at all [...] In particular, the difference in whether Sigma-types have strict eta
or not simply lies in whether we are talking about positive
Sigma-types or negative Sigma-types