Proposal
I propose we simplify the Rome calculus as much as we can, so that:
- we have spend less time (and space) in the text rehashing Rose19 and R-omega23
- the critical reviewer will see the paper less as leaching its merit from previous work
- it is easier to follow Rome solves particular challenges w.r.t. extensible recursion, and is not intended to be a novel calculus
How to simplify
- Remove multi-rows, row theories; work in the minimal row theory + commutativity
- Remove type equivalence
- Stay impredicative & operational
- ...