Tripos models of Internal Set Theory.

We introduce a categorical approach to nonstandard methods, loosely inspired on Internal Set Theory (IST) and reliant on the rich notions of hyperdoctrine and tripos from categorical logic. A different point of view is adopted: the axioms of IST should be expressed in terms of interactions between doctrines, which can be thought of as saying that instead of adding a new predicate we only add new quantifiers. Moreover, it differs from the typical approaches in that the foremost axiom is Standardisation rather than Transfer, all of which can be expressed in a point-free way. This opens the way to the usage of nonstandard proofs methods in the internal language of a doctrine. [ABSTRACT FROM AUTHOR]