Have you looked at Metamath Zero[1] before? You mentioned using sorts which is what reminded me of it. Just thought I'd point to some additional interesting work :)

[1] https://github.com/digama0/mm0