The Coq mailing list

[Anthony Bordg <bordg.anthony AT gmail.com>]

Hi,

A long time ago I ran into similar questions and came to the same conclusions. These kind of "simplifications" as (forall (x:A), B x) = (forall (x:A), B' x) ->
  forall (x:A), B x = B' x and so by function extensionality (fun x => B x) = (fun x => B' x))  are  unprovable and provably false with univalence.
For instance, you can ask a similar question with Sigma types at least for the independant case it gives: is forall (A B C: U), C -> A * C = B * C -> A = B provable (where U is a univalent universe) ? Actually this is not the case and provably false, ie the type (forall (A B C: U), C -> A * C = B * C -> A = B) -> false, is inhabited. The proof has the same flavour and goes through the following lines:

You can start by exhibiting an inhabitant of unit = Bool -> false using the recursor for Bool (you don't need univalence so far but recursor and transport). Assume you have an inhabitant of forall (A B C: U), C -> A * C = B * C -> A = B, assume A:= unit, B:= Bool and C:= Nat (you have 0: Nat), assuming univalence you can construct an equality unit * Nat = Bool * Nat and so get unit = Bool. Thus, by the first term construction you get false.

Best

Anthony

2013/12/16 Edwin Westbrook <westbrook AT kestrel.edu>

Great, thanks, that was very helpful!

-E

On Dec 16, 2013, at 10:57 AM, Jason Gross <jasongross9 AT gmail.com> wrote:

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