Power types in explicit mathematics?
Gerhard Jäger · Journal of Symbolic Logic · 1997
Abstract In this note it is shown that in explicit mathematics the strong power type axiom is inconsistent with (uniform) elementary comprehension and discuss some general aspects of power types in explicit mathematics.