Rename Set to Type

[Alizter]

It is rather unfortunate that Agda calls its univereses Set. Renaming it to Type will be much more readable.

1. We need a good way to rename Set into Type.
2. We need to go about replacing all occurrences of Set with Type.

I have no idea how these will be achieved in Agda. Some people discussed possible solutions in #77 so let's collect them here and discuss.

[L-TChen]

Simply adding the following code to Core.Prelude should do the trick as suggested in https://github.com/agda/cubical/issues/77#issuecomment-473402355

Type : (ℓ : Level) → Set (ℓ-suc ℓ)
Type ℓ = Set ℓ

Type0 : Type (ℓ-suc ℓ-zero)
Type0 = Type ℓ-zero

Since Set is a keyword, replacing every token Set with Type if followed by a token except → or Set with Type0 if followed by → or nothing, should be okay. Alright, maybe I can do it later ...

[martinescardo]

You may not like my solution, but it does look close to e.g. the HoTT book, and so I suggest it here just in case:

https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#universes

[L-TChen]

You may not like my solution, but it does look close to e.g. the HoTT book, and so I suggest it here just in case:

https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/MLTT-Agda.html#universes

It looks nice to me. Just in case, Quail/Agda-input is customisable , so it can be typed by two keystrokes only, e.g. \U, fewer than Type.

[Alizter]

@martinescardo The link is not working.

[martinescardo]

Sorry, I was redesigning some things and the link changed. It should be stable now. I edited it above, repeated here: https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.html#universes

Apologies.

[martinescardo]

(I had to change the links so that the automatically generated pdf file had the links pointing to itself rather than the html file. This involved redesigning the html link strategy.)

[Alizter]

@martinescardo These notes are really well written! I seem to have issues in chrome seeing the universe symbol however. It works fine in firefox.

[martinescardo]

Thanks. Strange. I am using chrome to generate the pdf from html and the universe symbols are rendered correctly (https://www.cs.bham.ac.uk/~mhe/HoTT-UF-in-Agda-Lecture-Notes/HoTT-UF-Agda.pdf). Maybe I could add something to the html or css file? I will try to find a solution.

[Alizter]

@mortberg Which solution do you prefer?

[mortberg]

@mortberg Which solution do you prefer?

The proposed solutions are Type and Martín's fancy U symbol? How do I type the fancy U, just \U?

For replacing all uses of Set we can use emacs tags replace, as long as someone can help us generate a TAGS file for Agda code.

[L-TChen]

@mortberg Which solution do you prefer?

The proposed solutions are Type and Martín's fancy U symbol? How do I type the fancy U, just \U?

By default, one has to type \MCU for 𝓤, but typing consecutive capital letters is always a pain. In emacs, you can add any translation you like to the Agda input method by

M-x customize-option <RET> agda-input-user-translations <RET>

For example, putting U (without backslash) in Key sequence and 𝓤 in Translations allows you to type 𝓤 by \U.

We could explain how to type this fancy 𝓤 in README.md or simply make a PR to add this for good if it becomes standard.

[Alizter]

One thing I will note here is that I cannot see any of the U's. Personally I prefer Type.

[martinescardo]

I would say the following. Personally, I prefer the "U,V,W" notation for universes, because I think in terms of universes rather than in terms of universe names. However, "Type i" (or whatever symbol you use for type levels i) should also be fine from my point of view, and certainly much better than "Set i". So, if we want to avoid arguing and also a more difficult implementation, we can just replace "Set" by "Type" using "sed" or "emacs". However, this will alienate, for instance, people coming from the HoTT book and then trying to see how we do things in the computer with Agda. In any case, Type is much better than Set.

[Alizter]

I would say that U is really a symbol. In computer formalisations, I would prefer a name rather than using a symbol.

I would wager that somebody who knows what Type means, but not what U means would have a harder time, than somebody who knows what U means but not type. Type is pretty clear on what it is.

On Tue, 9 Apr 2019 at 18:15, Martin Escardo notifications@github.com wrote:

I would say the following. Personally, I prefer the "U,V,W" notation for universes, because I think in terms of universes rather than in terms of universe names. However, "Type i" (or whatever symbol you use for type levels i) should also be fine from my point of view, and certainly much better than "Set i". So, if we want to avoid arguing and also a more difficult implementation, we can just replace "Set" by "Type" using "sed" or "emacs". However, this will alienate, for instance, people coming from the HoTT book and then trying to see how we do things in the computer with Agda. In any case, Type is much better than Set.

— You are receiving this because you authored the thread.

Reply to this email directly, view it on GitHub https://github.com/agda/cubical/issues/118#issuecomment-481341626, or mute the thread https://github.com/notifications/unsubscribe-auth/AINyk2E5rsiN4Rfv_Pmw6lwyxJN9Vctcks5vfMq6gaJpZM4cS2ql .

[martinescardo]

(And "level" for type levels is just as bad as "sets" for "types", because we have hlevels which are often abbreviated as "levels" in informal parlance.)

[martinescardo]

(At some point, the universe handling will need rethinking, both in Agda and in Coq, and more generally in type theory. People try to push the universes under the carpet. A lot of definitions/proofs/constructions in the current cubical Agda library have "wrong" universe levels. They are much more restrictive than they need to be. People don't pay attention to universes. The "experiment" I pushed last week was done with the help of @mortberg, translating some code I already had. We spent a lot of time fighting with this specific issue.)

[mortberg]

It seems to me like replacing Set by Type should be easy enough and a step in the right direction.

Having experience with working in both Coq and Agda I can only agree with @martinescardo that more work has to be done to make universe handling easier and more intuitive.

[martinescardo]

I am willing to generalize the universe-level assignments all over the cubical Agda library, and this needs to be done. I learned this the hard way in my own personal UF library (which was not done for the sake of itself, but for the sake of other mathematical work I was doing which I chose to render in univalent foundations). But right now I don't have time to do this, in the next few weeks.

[Saizan]

@martinescardo some examples of what should be generalized?

[martinescardo]

The example that caused trouble was elimEquivFun. My code didn't type check with that because it needed a more general type for P, namely (P : (A : Set ℓ) → (A → B) → Set ℓ') (add a prime in ell). This more general type is the one I have in my own UF library. Anders and I managed to change the proof to make it work with the less general type for elimEquivFun. By the way, I am trying to compile the file that has this, but "GroupoidLaws" is taking forever. Agda version 2.6.0-53189d7

[L-TChen]

By the way, I am trying to compile the file that has this, but "GroupoidLaws" is taking forever. Agda version 2.6.0-53189d7

Just a workaround: try make clean && make under the library’s root directory where you will find a Makefile. The commend deletes all cache files and type check everything.

[Saizan]

The GroupoidLaws problem should be solved by https://github.com/agda/agda/commit/13d516f20d5cdf88e35349a2d8ddc52e1c5c2dde

[mortberg]

I'll rename Set type Type now.

[martinescardo]

By the way, I am trying to compile the file that has this, but "GroupoidLaws" is taking forever. Agda version 2.6.0-53189d7

Just a workaround: try make clean && make under the library’s root directory where you will find a Makefile. The commend deletes all cache files and type check everything.

Haven't had a chance to check this, as we are running the Formal Topology Workshop. However, I tried that (at the time mentioned above) with a clean copy of the repository.