The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

As I understand it, with funext, you can prove irrelevance for all proofs of x <> y of any type (because False is an hProp).  However, without funext, you can't really prove anything about equality of most function spaces (just like without K nor univalence, you can't really prove anything about equality of most types).  (I think there's actually a deeper relationship here, probably along the same lines of how univalence implies funext.  I don't understand it fully myself, but I believe Dan Licata has a blog post on how knowing about equality in a universe gives you things about equality of functions between types in that universe.). In general, I think all you can say is that if you can prove that `A -> B` is isomorphic to some non-arrow-type `C` when you assume funext, then you can probably embed `C` into `A -> B` even without funext.  So you can lower-bound the number of distinct functions of a given type, but you can't upper-bound it without funext in general.  (Exception: you can upper-bound the number of functions from `A -> B` when `A` is inhabited and `B` is not; the upper-bound is 0.)

I believe Pierre-Marie Pedrot has some models of type-theory (or pointers to them) which contradict funext.  I'm not sure whether or not any of them allow for multiple proofs of `A -> False`, though I could believe that they might.

-Jason

On Tue, Jun 23, 2020, 22:25 Talia Ringer <tringer AT cs.washington.edu> wrote:

Hi all,

I think this should be obvious, but I'm having trouble thinking right now. I figure I'll ask in case somebody knows the answer.

Suppose I have a type with decidable equality, like nat. Then provably I have that all proofs of n = m for n m : nat are equal to each other, without assuming UIP as an axiom. That much I know.

From this, can I say anything about proofs of n <> m for n m : nat without assuming functional extensionality? For example, are all proofs of 0 <> 1 equal to each other? If not, are they provably related in any interesting way?

Talia