The Coq mailing list

[Thorsten Altenkirch <Thorsten.Altenkirch AT nottingham.ac.uk>]

The proof by Hedberg only requires that there is a constant endofunction

Pi x,y:A. x=y -> x=y

However, this already follows from stability

Pi x,y:A ~~(x = y) -> x=y

by composing with x=y -> ~~(x = y) [see lemma 3.5 in our paper
http://www.cs.nott.ac.uk/~psztxa/publ/jhedberg.pdf)

On the other hand it is easy to see that all standard type formers (Pi,
Sigma, W, finite types) preserve stability - hence all common types
satisfy UIP.

Thorsten


On 09/09/2016 09:16, "Alan Schmitt" 
<coq-club-request AT inria.fr
 on behalf
of 
alan.schmitt AT polytechnique.org>
 wrote:

>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





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.