David has since also made extensive progress with his category-theoretic approach, available in a new repository:

https://github.com/Precisfice/DEDUCTION