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.  ...
>

-- 
You received this message because you are subscribed to the Google Groups "Homotopy Type Theory" group.
To unsubscribe from this group and stop receiving emails from it, send an email to HomotopyTypeTheory+unsubscribe@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.