New preprint out on separating definitional equivalence and bi-interpretability, joint with Toby Meadows.