Large raise structures

[lowasser]

I'm betting there's a better name, but I don't know it.

What I want is to characterize types with large similarity operations and a similarity-preserving raise operation, and to generalize results such as "if a binary operation preserves similarity, raising each argument is equivalent to raising the result" and other related facts we prove many times.

[lowasser]

I'm mostly posting the issue in the hopes someone knows a better name.

[fredrik-bakke]

I don't know a name for this at least, sorry. The word "raise" is about the operation of the structure though, not the structure itself. Really it is about a cumulative universe polymorphic structure... Some people use "heterogeneous equality" for equlity-like structures like similarity... Just to throw some words at you.

[lowasser]

Maybe something about large sets, since we've declared similarity propositional?

[lowasser]

Actually, I'm thinking about calling it a large tower, just in terms of "each level is built on the levels below it".

[fredrik-bakke]

How about cumulative large set? Personally not a fan of using "large tower" here. What you have is actually a cotower, but we use the term "sequential diagram" for this concept in agda-unimath. (This was a big discussion in the past, initially I wanted to call inverse sequential diagrams "towers" #990)

[fredrik-bakke]

BTW there's a distinction between "large" and "global" sets we use. A global set is one that is defined at each universe level, while a large set may be parametrised in any which way.