 What of the free creativity the formalist cherishes? Constructivist type theory has, of course, been extended well beyond Heyting arithmetic, particularly ambitious extensions are to be found in the univalent foundations project based on homotopy type theory (Awodey, 2014). This, then, is an avenue a formalism based on Formulae-as-Types might pursue. But for a formalist who wishes to be non-revisionist about non-constructivist mathematics the prospects are perhaps less clear. It is not enough just to add in the extra axioms or inference rules which yield the particular theory, in a standard framework, e.g. of a first-order or higher-order language. For one needs to do the further work needed to show that an extension of the CH correspondence obtains in this system. 