[Agda] type/set nomenclature

[Guillaume Brunerie]

> However, it does seem to me like it's a good way of breaking the deadlock wherein the excellent homotopy type theory
> libraries of Brunerie et al freely mix "Set" and "pType" as names for unpointed and pointed types respectively.

We’re in the process of rewriting the whole library (see branch 2.0 on
github.com/HoTT/HoTT-Agda) and in the new version we’ve defined "Type
i" to mean "Set i" in order to use Type everywhere. The only drawback
is that you cannot use just Type to mean Set0, you need to apply it to
the first universe level.

Such an option would be a good idea though.

Guillaume

2013/7/1 James Cranch <jdc41 at cam.ac.uk>:
> Dear all,
>
> Would the Agda developers be interested in adding a command-line option to
> replace the built-in name "Set" by "Type"?
>
> This option might be attractive to people (like me) who are in the habit of
> systematically using the without-K option, and would do so without annoying
> any of the current users.
>
> Obviously this is entirely cosmetic, and as such not of very high priority.
> However, it does seem to me like it's a good way of breaking the deadlock
> wherein the excellent homotopy type theory libraries of Brunerie et al
> freely mix "Set" and "pType" as names for unpointed and pointed types
> respectively.
>
> Best wishes,
>
> James Cranch
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda