Concrete notation of coe sucks!

[jonsterling]

Can we think of a better notation? It's so ugly. Honestly, comp is bad too when it is dependent.

[favonia]

Core issue: where and how to put the families.

[favonia]

Maybe it will help with an ML function doing "abstract goal over x"? Perhaps also some shortcuts such as "type of x".

[jonsterling]

Carlo and I trained our prethought on this for a few hours and are very discouraged. Everything we could come up with sucks in some way or another... We'll come back to it.