- [ ] Give an $$R\omega$$ denotation of the scoed row theory in Agda; - [ ] parameterize $$R\omega\mu$$ by row theories; - [ ] Organize minimal, simple, and scoped row theories in Rome's /IndexCalculus/.
