The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

I'm no longer convinced this can be done, but I bet asking on hott-cafe, or looking at the file PathGroupoid in the HoTT library, could get you ask answer (the HoTT name for [f_equal] is [ap])

Coq can do more with x=y because the induction principle is secretly about { y | x = y }, not about x=y. 

On Wed, Aug 31, 2016, 11:07 PM Jason Gross <jasongross9 AT gmail.com> wrote:

In UIP_iso_pointed you should be able to do [apply (f_equal BtoA) in H], and then prove that if you nest two [f_equal], you could have a single one that is on a function composition, and then prove that if you do [f_equal] with a function that is equal to the identity on the end-points of your path, you could just as well not have had the [f_equal] at all.

On Wed, Aug 31, 2016, 9:08 PM Jonathan Leivent <jonikelee AT gmail.com> wrote:

On 08/31/2016 11:41 PM, Jonathan Leivent wrote:
>
> On 08/31/2016 11:18 PM, Jason Gross wrote:
>> Actually, I think it's possible to do better; you should only need
>> AtoB_BtoA specialized to the point you care about.  This should be a
>> relatively simple transformation to make, and, I think, should be
>> powerful
>> enough to let you handle recursive types
>
> I think you are right that AtoB_BtoA only needs to be at a point. But,
> if AtoB is always a ctor and BtoA is always a proj, then I'm not sure
> that this specialization helps much, if at all.
>
> -- Jonathan
>

Oops - it is needed. I just tried using UIP_iso_pointed to prove UIP on
nat, and got:

|- forall b : nat, S (pred b) = b

which is obviously not true at b=0.  OK - how to make it only need
AtoB_BtoA at a point?  Obviously, f_equal_cancel needs to be reworked,
but the obvious way "(e : x=x)" doesn't work.  It always seems peculiar
to me that in some circumstances in Coq, one can do more to x=y than to
x=x - as in this case.

-- Jonathan