The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Here's a more general version of the proof in Coq, in the HoTT/HoTT library: https://github.com/HoTT/HoTT/blob/master/theories/Types/Forall.v#L216  Saying that a type is 0-truncated (an hSet) is the same as saying that it has UIP.  It uses a lot of machinery, though, so may not be enlightening at first glance. (Note that this proof happens in a section that assumes function extensionality.)

On Fri, Sep 9, 2016 at 8:37 AM Jason Gross <jasongross9 AT gmail.com> wrote:

The proof sketch that [nat -> bool] has UIP is that UIP respects equivalence, and the types [@eq (nat -> bool) f g] and [forall x : nat, @eq bool (f x) (g x)] are equivalent by strong function extensionality.  Since [bool] has UIP, [@eq bool (f x) (g x)] is subsingleton (proof irrelevant), and so, again by function extensionality, [forall x : nat, @eq bool (f x) (g x)] is subsingleton too.
There is no internal proof that this type does not have decidable equality (after all, proof relevant excluded middle is consistent), but you can't actually algorithmically decide their equality without deciding the halting problem (let f be the function that is always false, and g(n) be true if a particular TM has halted after n steps, and false otherwise).

Another way of seeing this is that there is an easy way to make a function of type [forall x : nat, @eq bool (f x) (g x)] canonical, because Boolean equality is decidable.  But while canonicity plays well with all function types, decidability only plays well with finite domains.

On Fri, Sep 9, 2016, 8:14 AM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 09/09/2016 03:15 AM, Alan Schmitt wrote:
> ...
> I’m wondering about the converse: are there types for which equality is not
> decidable, but that have canonical equality proofs hence UIP?

Alan,

I have a class of types that have UIP but not eqdec ({a=b}+{a<>b}).
They have instead excluded middle of equality (a=b \/ a<>b), which I
call eqem.  I had also played with the proofs in Eqdep_dec, and found
that the requirement on eqdec there could be relaxed to eqem.

For most uses in Coq, eqem is probably not very useful.  However, I am
often working in a development that has proof relevance - a single Prop
that has an injection axiom on it.  The reasons have to do with getting
better erasability on extractions than I can otherwise get in Coq.
Having this one Prop with injection allows me to get discrimination on
all other inductive Props, which allows me to then get eqem on many of
them, and hence UIP.  Unfortunately, having a proof relevance axiom
means I can't use any axioms for proof irrelevance, so I need to prove
useful varieties, such as UIP or "irrelevant sibling" (for given prop P,
prove the existence of Q <-> P where Q is irrelevant - which I can do if
P has eqem).

I have been trying to find various ways to automate proofs of eqdec,
eqem, and UIP.   I will look closely at your proof to see if I can use
it, so thanks for posting it!   Also, I didn't yet get a change to
examine Dominique Larchey-Wendling's proof of UIP of sigma, but thanks
to Dominique for that as well!

Most recently, I have found a very promising way to automate proofs of
eqdec or eqem for dependent types - potentially more stable and
certainly easier to automate than what I was working on previously at
https://github.com/jonleivent/deptacs.  It involves proving eqdec (or
eqem) on a sigma equality over the dependent type first.

I have wondered if it may be the case in Coq - without any axioms - that
every purely inductive non-Prop type has eqdec and hence UIP. By purely
and non-Prop, I mean not having Prop or functional typed fields,
parameters, or indices.  Then, in the case of my proof relevance axiom,
this extends to eqem in any purely inductive type, even Props and with
Prop components - hence can potentially get UIP for all of them.

-- Jonathan