Interesting find, but again an example of where you first need to learn some new logic FOLDS ("FOLDS has the first two of these, contexts and types (although the latter are called 'sorts'), but it does not have the third, terms (except in the rudimentary form of mere variables), and it has equality in a greatly restricted form only.").

I wonder if it is impossible to describe a topos as a normal axiom system of first-order logic, or if people are just unwilling to do it.