The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

It is false, if you assume univalence.  Consider A = bool, and B x = if x then True else False, and B' x = if x then False else True.  Univalence gives  (forall (x:A), B x) = (forall (x:A), B' x) (because they are isomorphic types; both are isomorphic to the empty set), but it is clear that we shouldn't have forall x, B x = B' x (and thus can't have (fun x => B x) = (fun x => B' x)), because True != False.  Therefore, it's unprovable in vanilla Coq, and provably false in Coq + Univalence.

I'm not sure what it's status is if you have some particular axiom that contradicts univalence.  (As an extreme example, you could probably take it to be true as an axiom.  I don't think this is inconsistent, but it might be.)

-Jason

On Fri, Dec 13, 2013 at 9:20 PM, Edwin Westbrook <westbrook AT kestrel.edu> wrote:

Hi,

Does anyone know if the following lemma is provable in Coq? I am perfectly happy to use functional extensionality, or even stronger axioms, as I am already using informative excluded middle:

Lemma pi_eq_to_app_eq A B B' :
  (forall (x:A), B x) = (forall (x:A), B' x) ->
  (fun x => B x) = (fun x => B' x).

Thanks in advance!
-Eddy