[Agda] heterogeneous equality

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Thu Sep 9 12:39:50 CEST 2010


On 2010-09-09 05:07, Andrés Sicard-Ramírez wrote:
> I couldn't find the answer for this two years and a half old question.
> Was it answered anywhere?

Ulf and I discussed it in private.

The question is irrelevant now, because type constructors are no longer
(supposed to be) automatically injective.

--
/NAD



More information about the Agda mailing list