[Agda] symbol for a singleton set

[Nils Anders Danielsson]

On 2015-07-05 09:40, Andreas Abel wrote:
> On 04.07.2015 22:41, Sergei Meshveliani wrote:
>> I observe in  Relation.Unary.agda :
>>
>>    -- The singleton set.
>>    ｛_｝ : A → Pred A a
>
> This seems to be a remainder from when Nisse was fond of using unicode
> versions of reserved ASCII characters.

No, this name was introduced by Stevan Andjelkovic:

   Add monads on predicates.
   Patch by Stevan Andjelkovic

   https://github.com/agda/agda-stdlib/commit/12a251c02d320d809c2133514464b0ac848b6cf2

-- 
/NAD