Continuity is one of the most important concepts in higher-order computability. Informally, a functional is continuous if we only require a finite part of its input to compute a finite part of its output. Though there are a number of ways of making this precise, at type level 2, that is, for functionals , continuity…
