The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Thorsten, your proof requires function extensionality, right?

Jonathan, the Coq statement is:

  Definition stability A := forall x y : A, ~~(x = y) -> x = y.

  Definition constant_endofunction_eq A : forall x y : A, { f : x = y -> x = y | forall e1 e2, f e1 = f e2 }.

And the claim is [stability A -> constant_endofunction_eq A], that [constant_endofunction_eq A -> UIP_on A], and that all of the standard type formers preserved [stability].

On Mon, Sep 12, 2016 at 12:43 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 09/12/2016 01:57 PM, Thorsten Altenkirch wrote:
> 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)

But, in Coq, is this true?:  "There is, for any x, y : X, a canonical
map x=y -> ~~(x = y) ."

which, if I understand this correctly, means:

Goal forall X (x y:X) (e1 e2 : ~~(x = y)), e1=e2.

which I don't see how to prove in Coq for arbitrary X.

-- Jonathan