[Agda] type/set nomenclature

[Andreas Abel]

I guess "Set" is there for historic reasons, to distinguish from "Type", 
which, as explained in another current thread, denotes a universe of 
types but is not a type itself.

Personally, I would also prefer "Type" over "Set", since "Set" is a data 
structure, usually of finite sets, in the world of programming.

Possibilities are:

   1. a built-in style name rebinding for Set:
      {-# BUILTIN TYPE Set #-}

   2. a command-line option
      {-# OPTION ---use-Set-for-Type #-}

Probably 2. is better, fits more in the current style of built-ins.

Cheers,
Andreas

On 01.07.2013 18:25, Guillaume Brunerie wrote:
>> 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/