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?