Practical Generic Programming over a Universe of Native Datatypes
I just noticed that universes are basically cumulative with respect to Set omega, like every Set is in Set omega despite then being predicative otherwise
Like. What.
re: Practical Generic Programming over a Universe of Native Datatypes
Okay this ConDesc thing is on clever. It took me way too long to figure out what it was doing but somehow this is indeed the correct grammar for describing strict positivity
I think it would've been helpful to give a little... diagram? Illustrating how it looks nondependently
Like my notes rn look like
A ::= X (var)
| S -> X (pi)
| A -> A (otimes)
where X is the recursive argument and S is an arbitrary type (not incl. X since it's not in scope technically)
Practical Generic Programming over a Universe of Native Datatypes
Great now I gotta focus enough to read it through without getting distracted by how much levels look like sizes