[Agda] question on `Any'

[Nils Anders Danielsson]

On 2013-08-13 14:34, Dominique Devriese wrote:
> For more info, see the Agda tutorial by Norell and Chapman for
> example.  They mention the following rule:
>     The rule for when an argument should be dotted is: if there is a unique
>     type correct value for the argument it should be dotted.

This rule is rather imprecise. Unique with respect to what notion of
equality? Certainly not propositional equality.

-- 
/NAD