[Agda] type/set nomenclature
jdc41 at cam.ac.uk
Mon Jul 1 16:47:31 CEST 2013
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
More information about the Agda