[Agda] Type a = Set a

[Jon Sterling]

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