I understand HOL, because it is just sorted first-order logic. I also care about foundations, which is why I need to understand what a topos exactly is. So, i

I understand HOL, because it is just sorted first-order logic. I also care about foundations, which is why I need to understand what a topos exactly is. So, it seems that the steps you describe, until and including "Find other naturally occuring examples of topoi" can all be done in first-order logic set theory, is that right? ps: for people saying topoi, do you also say thermoi as a plural for thermos?