[Agda-dev] Using the size solver to get proto-cumulativity

[peio borthelle]

Hi, new here! This is a follow-up from irc (i'm lapinot).

So basically i wondered if it had already been investigated to give levels the same
kind of interface as the current sizes (and if it has, what are the pitfalls). To
explain a bit more what i mean, the crucial point is probably having a subtyping
relationship but only for levels. I guess it would look like:

postulate
  LevelUniv : LevelUniv
  Level : LevelUniv
  Level<= : Level -> LevelUniv
  lzero : Level
  lsuc : Level -> Level
  lub : Level -> Level -> Level

Together with a subtyping relationships `if a <= b, Level<= a <: Level<= b`, `if a :
Level, a : Level<= a` and `LevelUniv <: Set`. I guess that we could then create a
type of explicitely cumulative sets:

CSet : (a : Level) -> Set (lsuc a)
CSet a = Sigma (Level<= a) (\ b -> Set b)

Incidentally we could also get rid of the most annoying instances of `Lift`-hell that
arise when trying to give smaller than intended sets as parameters to some structure.

data Ugly (a : Level) : Set (lsuc a) where
  con : Set a -> Foo

-- throws in wrapping/unwrapping, clutters the output type (affects next definitions)
ugly : {a b} -> Set a -> Ugly (a lub b)
ugly X = con (Lift X)

-- no wrapping, clean interface
data Nice (a : Level) : Set (lsuc a) where
  con : {b : Level<= a} -> Set b -> Foo


Note that this whole thing may be actually hard if the generated constraints are hard
to solve, but until now i failed to see how they could be different than the one for
the sizes. There was some point about uniqueness of the solutions, i'm not sure how
this is handled by the sizes (is size uniqueness required?). Yet it might be pretty
reasonable to select the smallest solution.

If this approach works, it may be interesting to unify sizes and levels to a more
abstract ordinal (heck we might even add `lim : (a : Ord) -> (Ord< a -> Ord) ->
Ord`!). I guess that nothing stops us from using the same type to index sets (which
is already a core language type, thus magic) and to help solving termination.

Cheers,
peio