It appears that most cases of an internal language/logic/type theory of a category have an appropriate notion of implication/function types and a notion of lambda abstraction that makes use of them. For example, in CCCs we have the usual simply-typed $\lambda$-calculus/intuitionistic logic interpretation, where on the type theory/$\lambda$-calculus side hand we have the function (arrow) types and the related machinery, while on the logical side hand we have intuitionistic implication.
Same goes for symmetric monoidal categories, with the internal language being linear logic/linear type theory and so we have appropriate notions of linear implication and linear function types respectively.
Unfortunately, I can't as easily make sense of the place (if any) of $\lambda$-abstractions in the internal language/Mitchell-Bénabou language of a topos. For example, in chapter 5 of Sheaves in Geometry and Logic, we have a description of the internal langauge of a topos that includes both implication $a \implies b$ derived from the Heyting algebra structure of the subobject classifier, as well as a $\lambda$-ish syntax for what appears to be curried functions. On the other hand, in Johnstone's Topos Theory we have a description, in chapter 5.4 - definition 5.41, of the internal language that makes no mention of any $\lambda$-related terms - although there is a definition (iv)(b) of $\{x | \phi \}$ being a term of type $\Omega^X$. Can this not be extended to arbitrary exponentials and so yield the familiar interpretation of $\lambda$-abstraction as in CCCs? There is a possible allusion to that in page 133 of Lambek and Scott's "Introduction to higher order categorical logic" but as far as I can see it is never expanded upon.
Coming from a CS (i.e Curry-Howard, propositions-as-types, proof term assignments for natural deduction etc.) backround it seems bizzare to me to have both $\lambda$s and implications - I've always thought that (while of course interrelated) these are two different notions - one belongs to the "type theoretic" side and the other to the "logic" side of things.
As such, it is not clear to me what the place of $\lambda$-abstraction is in the internal logic/type theory of a topos and how this coexists in the same level with the notion of Heyting implication.
Disclaimer: I've only just started reading about toposes, and so this confusion is quite probably a result of my limited understanding of the subject.
Toposes are, in essence, the same thing as triposes. A tripos is essentially a semantics for a type theory in which there are propositions dependent on types, but not vice versa, and such that
(Note that I'm writing $\Gamma\vdash\varphi$ as opposed to $\Gamma\vdash\varphi:\mathrm{Prop}$ as a formation judgment above and in what follows, to distinguish between occurrence of $\varphi$ as a proposition and as a term of $\mathrm{Prop}$; I am not using it to mean that $\varphi$ is true in the context $\Gamma$.)
We get workalikes for power objects, as one might expect, as the function types $X\to\mathrm{Prop}$; we get membership relations $x:X,A:X\to\mathrm{Prop}\vdash\;\in_X$ as the predicate $\Phi(ev_{X,\mathrm{Prop}}(x,f))$; and we get an adequate notion of identity as $\exists_{\delta_X}(\top_X)$, the image of the uniformly true predicate on $X$ under the left adjoint to reindexing along the diagonal $\delta_X:X\to X\times X$. If you play around, I hope you'll be able to see that in essence you can interpret the Mitchell-Bénabou language along very similar lines as you see in Mac Lane-Moerdijk, excepting that you can interpret propositions directly without necessarily dealing with the type of propositions. However, in this situation we have a sort of fundamental division between propositions and types, and while function types belong to $\mathrm{Type}$ and $\lambda$-terms are terms of function types, implications belong purely to propositions and we don't talk about "terms" of propositions.
In a full fledged topos the propositions interact with the types in an additional way: there's an operation (actually part of an adjunction) on predicates $x:X\vdash\varphi$ taking them to monomorphisms $\{\varphi\}\hookrightarrow X$, making $\mathrm{Prop}$ morally like a subobject classifier. With this amenity you're essentially able to use a simply typed language with some nice type formers to talk about propositions dependent on types. But while the proposition/type distinction was forced above in the ontology, so to speak, it is forced another way in this simply typed language. First, for any type $A$ there is no type $X$ with $A:X$; no type is a term of some type. On the other hand, propositions are defined to be terms of some type. Likewise "$-\to-$" isn't an operation $x:A,y:A\vdash x\to y:A$ for some type $A$; the function type symbol is not a term-forming operation on type terms. on the other hand, implication is a term-forming operation $\varphi:\mathrm{Prop},\psi:\mathrm{Prop}\vdash \varphi\Rightarrow\psi:\mathrm{Prop}$.
In both cases, we see that propositions are not really types in the Mitchell-Bénabou language, and function types and Heyting implications are therefore not comparable sorts of things. There are, however, other languages for a topos that make predicates into types that satisfy certain additional conditions; but the those languages are typically dependently typed and much more fiddly than Mitchell-Bénabou.