The Coq mailing list

[Dominique Larchey-Wendling <dominique.larchey-wendling AT loria.fr>]

Hi Thorsten,

Well wanting to prove Leibniz identity of functions is already attributing

them a more specific meaning that what the underlying type theory tells you 

about their properties ;-)

I'd be interested with a simple example where funext is actually needed,

ie it is not just a convenience to avoid manipulating functions with their

natural identity which is extensional identity (or recursively for HO functions).

Best,

D.

---

De: "Thorsten Altenkirch" <Thorsten.Altenkirch AT nottingham.ac.uk>
À: "coq-club" <coq-club AT inria.fr>
Envoyé: Mercredi 24 Juin 2020 11:37:30
Objet: Re: [Coq-Club] Silly question about decidable equality and inequality

Coming to this discussion a bit late but here we have an inductive characterisation of inequality that is m <> n <-> m<n \/ n<m. You can prove UIP for the right hand side but not for the left because without funext you can prove nothing non-trivial about functions.

 

Thorsten

 

From: <coq-club-request AT inria.fr> on behalf of Xavier Leroy <xavier.leroy AT college-de-france.fr>
Reply to: "coq-club AT inria.fr" <coq-club AT inria.fr>
Date: Wednesday, 24 June 2020 at 08:07
To: "coq-club AT inria.fr" <coq-club AT inria.fr>
Subject: Re: [Coq-Club] Silly question about decidable equality and inequality

 

On Wed, Jun 24, 2020 at 8:52 AM Talia Ringer <tringer AT cs.washington.edu> wrote:

Thanks, that is very helpful! Part of the motivation for this was trying to understand why I find it more difficult to reason about { n : nat | n <> 0 } than I do about the inductive positives. It seems like it may be easier to reason about a different refinement of nats.

 

Right.  There are many other ways to write this subset type that behave well w.r.t. equality:

 

{ n : nat | Nat.eqb n 0 = false }

{ n : nat | 0 < n }         (* I believe that Nat.le and Nat.lt have unique proofs *)

{ n : nat | match n with O => False | S _ => True end }

 

etc.

 

- Xavier Leroy

 

 

 

(This is not for personal proving purposes, just academic curiosity.)

On Tue, Jun 23, 2020, 10:31 PM Gabriel Scherer <gabriel.scherer AT gmail.com> wrote:

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

This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.