[Agda] Type a = Set a

[Nicolas Pouillard]

On 05/30/2015 09:06 PM, Sergei Meshveliani wrote:
> People,
> I consider renaming `Set' to `Type' this way:
>
>    Type : (a : Level) → Set (suc a)
>    Type a = Set a
>
> The idea is to write `Type' everywhere instead of `Set'.
> Will this work all right?

I'm using this trick since quite a while in most of modules
of: github.com/crypto-agda

As you can see in:

https://github.com/crypto-agda/agda-nplib/blob/master/lib/Type.agda

I've used both ★ and Type, I'm now preferring Type over ★.

-- 
Best regards,
-- NP