[Agda] Re: Type a = Set a

[Sergei Meshveliani]

Jon Sterling writes 

> 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...


Thanks to people for the responses.

I am sorry for noise.

This my question about Type instead of Set is due to my old beginner's
impression, a prejudice. I thought that the word `Set' needs to be
reserved for algebraic applications, libraries, for example, for
Standard library.
Now I change my mind, and think that `Set' may occur even more correct
for the language. Because the Agda language itself expresses very
closely (constructive) sets by types. So, `Type' is for a meta-notion
about a program source, while `Set' is for the real meaning of a
program.

Regards,

------
Sergei