[Agda] Uniqueness [Was: Re: Hanging out with the Lean crowd]

[Frédéric Blanqui]

Thank you for these references.

However, if I understand correctly, in both cases, it is about 
unification in LF modulo beta, eta and projections only. So, this does 
not include user recursive definitions...


Le 27/08/2020 à 11:55, Víctor López Juan a écrit :
> Den 2020-08-25 kl. 15:36, skrev Neel Krishnaswami:
> >
> > I didn't know that solutions remained unique even if you solved
> > constraints lazily. Is there a reference for this?
>
> Den 2020-08-25 kl. 14:54, skrev Frédéric Blanqui:
>>
>> Le 25/08/2020 à 12:49, András Kovács a écrit :
>>> Frédéric: by solving only pattern unification problems, which have 
>>> definitionaly unique solutions,
>>
>> Could you provide a reference please?
>
> A good one would be Jason Reed's 2009 paper [1], which shows this for 
> the λΠ calculus.
> Andreas Abel and Brigitte Pientka generalize it to the λΠΣ calculus [2].
>
> [1]: https://www.cs.cmu.edu/~jcreed/papers/lfmtp2009.pdf
> [2]: https://link.springer.com/chapter/10.1007/978-3-642-21691-6_5