Rename Set to Type about cubical HOT 24 CLOSED

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.

from cubical.

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

from cubical.

Simply adding the following code to Core.Prelude should do the trick as suggested in #77 (comment)

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

from cubical.

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

from cubical.

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.

from cubical.

@martinescardo The link is not working.

from cubical.

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.

from cubical.

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

from cubical.

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

from cubical.

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.

from cubical.

@mortberg Which solution do you prefer?

from cubical.

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

from cubical.

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

from cubical.

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.

from cubical.

from cubical.

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

from cubical.

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

from cubical.

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.

from cubical.

@martinescardo some examples of what should be generalized?

from cubical.

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

from cubical.

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.

from cubical.

The GroupoidLaws problem should be solved by agda/agda@13d516f

from cubical.

I'll rename Set type Type now.

from cubical.

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.

from cubical.