From [tt2020](https://github.com/shd/tt2020): - [ ] Linear types - [ ] Subtyping: #52 - [ ] Paradoxes and universes - [x] Arend: #39
From tt2020: