New Foundations (NF) is a version of axiomatic set theory in which there is a set of all sets, but the comprehension axiom is restricted by a “stratification” condition.

The category of sets and functions in NF is known to not be cartesian closed, so it is not a topos, but can be equipped with finite limits and a subobject classifier. One can even construct a set of all functions between two sets, but there is no evaluation map $A\times B^A \to B$ making this an exponential in the category.

There are at least three proofs of this fact: one, due to Randall Holmes, doesn’t seem to have been made public; the others are due to McLarty and Forster, and derive contradictions (different in the two proofs) from assumptions on the behaviour of a pairing function used to construct binary products.

For a long time the (relative) consistency of NF was an open problem, although NF with urelements (NFU) was known to be consistent (relative to ZF plus some large cardinals). Recently there may be a proof of its consistency.