Topos

The word topos can refer to either an Elementary Topos or a Grothendieck Topos. In Impredicative foundations, every Grothendieck topos is an elementary topos, so there is no harm in refering to elementary topoi as simply "topoi". However, in Predicative foundations, this is not the case; there are essentially 0 elementary topoi, so here topos really ought to mean Grothendieck topos.