The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 09/12/2016 04:48 PM, Jason Gross wrote:
> 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].

OK - got it.  I was able to prove [stability A -> 
constant_endofunction_eq A] given functional extensionality:

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

Lemma dubneg: forall P:Prop, P -> ~~P.
Proof.
  intros.
  intro.
  contradiction.
Defined.

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

Require Import FunctionalExtensionality.

Goal forall A, stability A -> constant_endofunction_eq A.
Proof.
  intros A H.
  red.
  intros.
  exists (fun e => H x y (dubneg _ e)).
  intros.
  f_equal.
  apply functional_extensionality.
  intro.
  contradiction.
Qed.


I also have a version of Eqdep_dec now that works with nu being any 
constant_endofunction - as Alan pointed out earlier.

Cool!  Thanks Thorsten and Jason!

Now the trick is to see if it is easier (than proving UIP directly) to 
prove a type preserves stability from its components...

And whether one can live with the requirement for this specific version 
of functional extensionality, especially those of us who prefer our 
bread unbuttered.

However, currently, I am making great progress on a nice way to prove 
eqdec or eqem on sigT equalities, provided the sigT equalities of the 
components...

-- Jonathan