Naming of reflective global subuniverses

[fredrik-bakke]

I'm finding my code difficult to parse due to very long entry names that mostly stem from the
names global-subuniverse andreflective-global-subuniverse. Could global-subuniverse be shortened to subuniverse-ω and reflective-global-subuniverse be shortened to reflective-subuniverse-ω?
I imagine then calling the separatedness condition is-separated-ω, and a localization wrt. a global subuniverse for localization-ω. A global subuniverse equivalence would be subuniverse-ω-equiv and a global subuniverse connected map would be connected-map-ω. Notice that there currently is no good abbreviation for most of these, and they are only the most fundamental definitions.

[VojtechStep]

That sounds reasonable to me

[EgbertRijke]

As a phrase, "global subuniverse" is a lot easier to parse to me than "subuniverse omega". It seems to me that the proposed new expressions are only five characters shorter, but at the cost that the interpretation is perhaps not so easy.

[VojtechStep]

I would read it as relating to UU omega, but it's true that we already have a naming convention for that sort of types, and that's Large-

[EgbertRijke]

I think this suggestion is setting us up poorly for when we actually want to formalize something about the ordinal omega. Or when the agda internals for Level change (what if they put 2*omega in Level?)

[fredrik-bakke]

As a phrase, "global subuniverse" is a lot easier to parse to me than "subuniverse omega". It seems to me that the proposed new expressions are only five characters shorter, but at the cost that the interpretation is perhaps not so easy.

It is true that the base definitions will only get five characters shorter, however, the name is-separated-ω is 17 characters shorter than is-separated-global-subuniverse. Without a developed shorthand, I do not see how to give a terser name for this entry, and that stems from a change to the name of global-subuniverse.

[fredrik-bakke]

I see, being global is not really about the ordinal ω, it is about being polymorphic, in fact, global. Perhaps we can choose another symbol that does not have a prior conflict with something else?

[EgbertRijke]

The name is-separated-ω is very difficult to parse to me, especially given that the naming scheme of the library suggests a meaning it doesn't have. By the naming scheme of the library, this should be an entry about separatedness of ω (whatever that means). Nothing in this name suggests that it is actually about some kind of subuniverses. So it is quite a stretch to ask the reader to interpret as the condition that a global subuniverse is separated. The connection from the name to that reading is not at all obvious.

[fredrik-bakke]

Fine, is-separatedω then, or whatever other symbol we choose, so that the concept is not read as a composite? The issue still stands that in my experience it is a problem how verbose these names are getting, and I'm trying to find a solution to that.