Quine's set theory NF has a comprehension scheme based on a typing discipline, and it admits large sets. This makes for smooth "top-down" existence proofs of inductively defined sets. Proving the equivalence of top-down and bottom-up constructions requires classical logic. However the presence of a universal set blocks the obvious construction of a negative interpretation of the classical theory NF into the constructive theory (INF). NF interprets PA but the proof is not constructive, and it is not known whether or not INF interprets Heyting arithmetic.