The Coq mailing list

[Alan Schmitt <alan.schmitt AT polytechnique.org>]

Hi Jason,

On 2016-09-09 07:57, Jason Gross 
<jasongross9 AT gmail.com>
 writes:

> If you assume function extensionality, then the type [nat -> bool] has
> UIP, but not decidable equality. I'm not sure if you can find a type
> like this without function extensionality.

This is very interesting. I tried to look for that proof but I cannot
find it (I do find many things about HOTT, which I must confess I do not
understand). Do you have a link?

Thanks,

Alan

-- 
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO₂, Mauna Loa Obs. 2015-08: 398.93, 2016-08: 402.25

Attachment: signature.asc
Description: PGP signature