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

[Víctor López Juan]

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