The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Consider [forall x, if x then unit else bool] and [forall x, if x then bool else unit].  They are equal by univalence, but [if x then unit else bool != if x then bool else unit].  You can think of [forall x : A, B x] as an A-indexed product; up to isomorphism, X * Y = Y * X (and more generally for automorphisms of A).  But the functions, unlike the Pi types, do care about the ordering/naming of the components.

-Jason

On Mon, Dec 16, 2013 at 11:53 AM, Edwin Westbrook <westbrook AT kestrel.edu> wrote:

Yeah, I was just starting to think of univalence…

What if both A and (forall (x:A) B x) are known to be inhabited?

Thanks,

-Eddy

On Dec 13, 2013, at 7:58 PM, Jason Gross <jasongross9 AT gmail.com> wrote:

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