What about strict uniqueness for the empty type? In general, what about the "discrete" inductive types of computational HDTT, including HTS-style natural numbers? I understand that this is not something we expect all models to have, but they're useful when available, and they have strict extensionality.
On Saturday, February 16, 2019 at 8:25:43 PM UTC-5, Michael Shulman wrote:
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: *negative* types have strict eta, while positive
types don't. ...