search

agda / agda-categories

A new Categories library for Agda
https://agda.github.io/agda-categories
MIT License
363 stars 68 forks source link

Rename Sets to Types ? #286

Open JacquesCarette opened 3 years ago

JacquesCarette commented 3 years ago

We followed Agda's misnaming of universes, and named the category of (types, functions) Sets. This has confused people (I was replying to such a confusion just before this).

I think we should rename it Types.

Whether we can have something like a proper Sets is an interesting question!

Note that since we have Hom-Setoids, this renaming would actually have very few ripples.

Taneb commented 3 years ago

I think this is reasonable. I'm not convinced it's necessary but if you say it's caused confusion I'll trust that

TOTBWF commented 3 years ago

Huge 👍 from me! I would even go so far as adding a disclaimer at the top saying "this is probably not what you want", and try to direct people to use Setoids instead.

gallais commented 3 years ago

I guess another common naming strategy is to call it after the host language.

sstucki commented 3 years ago

If it's called Types or Agda then maybe no disclaimer is needed. Otherwise I agree with @TOTBWF that we should nudge new users away from this category.

JacquesCarette commented 3 years ago

I'm kind of warming up to Agda. The next question: should we have both Agda and PointwiseAgda (or a variant thereof)? Sergey Goncharov (@sergey-goncharov) points out that the equality of functions in Agda should be the 'normal' equality (even though it's awful to work with), not the extensional one. And, for sure, we should discourage its use. At least it's a category (unlike Hask).