This proof of Lawvere's fixed point theorem suggests (since it uses $\lambda$ notation) that it is written in the *internal language* of cartesian closed categories (which is the $\lambda$-calculus, as explained e.g. in Part I of Lambek and Scott's book *Introduction to higher order categorical logic*). However, one needs quantifiers in order to formulate the notion of *point-surjective* and the *existence* of a fixed point $s\colon 1\to B$. So strictly speaking, the proof can't take place in the internal language, since the $\lambda$-calculus doesn't have quantifiers and assumptions. (Higher-order logic admits quantifiers, but that is only available in elementary toposes and not in cartesian closed categories in general.)

**Question:** Is there some way of making the proof formally work in some "internal language" of cartesian closed categories? Or is the $\lambda$ notation used in the proof just an informal explanation of the proof rather than an indication for the use of the internal language?