Classical truth in higher types