The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

Pierre-Marie's typical example defines (A -> B) in the guest type theory as (bool * (A -> B)) in the host theory, with a type-preserving translation, and (=) in the guest as just (=) in the host.  For any function you can get another distinct (but observably equivalent in the guest) function by flipping the boolean. This also applies if B is False.

On the other hand, you could define a "smaller" type of inequivalence for a type (as an inductive presentation if you can, for example) that has better properties. This comes up often in cases where you need to reason on elements being equal, as the definition of inequivalence as a function makes it hard to reason about.

For natural numbers for example, one definition of inequivalence might be something like

Inductive different :=

| Bigger : forall (k : nat), m = n + S k -> different m n

| Smaller : forall (k : nat), m + S k = n -> different m n.

and this one should inherit contractibility from equality.

On Wed, Jun 24, 2020 at 6:12 AM Jason Gross <jasongross9 AT gmail.com> wrote:

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