Failure of Higher-Order Truth within Intuitionistic Propositional Logic

Yiqi Xu, Lingyuan Ye

We answer the question whether all Heyting algebras can appear as the lattice of subterminal objects of an elementary topos in the negative. Concretely, we show that the free Heyti…