[Agda] Type a = Set a

[Alexander Altman]

For the record, this is exactly what the HoTT Agda library does (at <https://github.com/HoTT/HoTT-Agda <https://github.com/HoTT/HoTT-Agda>>).

> On May 30, 2015, at 4:01 PM, Kirill Elagin <kirelagin at gmail.com <mailto:kirelagin at gmail.com>> wrote:
> 
> Well, the problem is that the things you have in `Set` are _actually_ sets, that is, 0-types.
> So what is the point of renaming?
> 
> Other than that, I can’t see how this can possibly cause any serious issues.
> Except for the fact that you can write just `Set`, without a level, but you can’t write just `Type`.
> You also can write `Set18` and `Set₄₃` but you won’t be able to do this with `Type`.
> 
> On Sat, May 30, 2015 at 10:06 PM, Sergei Meshveliani <mechvel at botik.ru <mailto:mechvel at botik.ru>> wrote:
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
> https://lists.chalmers.se/mailman/listinfo/agda
>> 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?
>> 
>> Thanks,
>> 
>> ------
>> Sergei
>> 
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>> https://lists.chalmers.se/mailman/listinfo/agda <https://lists.chalmers.se/mailman/listinfo/agda>

-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150530/e20a4f3c/attachment-0001.html