I was having coffee this morning with Thomas Forster, and we were talking — as you do — about theories with a universal set, and the claim that (a version of) Church’s Theory with a universal set is in fact synonymous with ZF. Doing a bit of googling around after our chat, I find that Tim Button has recently given a characteristically clear and lively talk about very closely related ideas, including developing some of Thomas’s. Here it is.