[Agda] Type a = Set a

[Thorsten Altenkirch]

This is correct. At the same time we used the convention to call the small
types “sets” that is Set = Type(0).

This is at odds with the HoTT convention to call types for which UIP holds
sets. The idea is the same we call the ordinary things sets but this time
we base this on dimension not size.

Thorsten

On 31/05/2015 16:08, "Jon Sterling" <jon at jonmsterling.com> wrote:

>I think Agda uses the name Set, because it is descended (via ALF) from
>the logical framework presentation of type theory described in
>Nordström, Petersson & Smith's “Programming in Martin-Löf’s Type
>Theory”. In this context, “Set” makes more sense than “Type” fwiw,
>though I suppose that Agda has moved in quite a different direction from
>the PiMLTT calculus and maybe we shouldn't care about that as much
>anymore...
>
>Best,
>Jon
>
>
>On Sun, May 31, 2015, at 03:34 AM, Nicolas Pouillard wrote:
>> 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
>> _______________________________________________
>> 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





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.