Paper reading activity

[ice1000]

trafficstars

Anybody wanna read some papers with me?

Plans:

• [x] AK's universe polymorphism implementation
• [X] JS's oktt
• [ ] AK's first class level paper
• [ ] Lean's tabled typeclass resolution

[ice1000]

https://twitter.com/Heartof_Gold__/status/1416475517679702020 ???

[ice1000]

I kinda understand AK's design rn. It is similar to Jesper's approach: the Ctx contains a level, and the expressions are checked accordingly. In our approach, we propagate the level when synthesizing types and do comparisons in the defeq class. This is interesting.