[Agda] type/set nomenclature

[James Cranch]

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