# The place of lambda abstraction in internal and Mitchell-Bénabou languages

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.

• It's because toposes are best thought of as having two sorts of things: types and propositions, and the situation that $\mathrm{Prop: Type}$. They interact, but conceptually they're distinct. – Malice Vidrine Aug 19 '17 at 22:24
• I've never heard that before - very interesting. Could you point me towards any sources that expand upon that? Does that resolve the ambiguity of $\lambda$-abstractions too? – NullSpace Aug 20 '17 at 11:54
• The source I'm most familiar with is Jacobs's Categorical Logic and Type Theory, in particular his chapter on "higher order fibrations". I'm not sure what ambiguity you mean, re $\lambda$-abstraction; in your post it looked like you were puzzled by their being treated as distinct, and my reason for mentioning the above is that $\lambda$-abstracts inhabit function types, while implications are propositions, which (morally) aren't types at all. That is, $\Rightarrow$ and $\to$ live in different worlds. – Malice Vidrine Aug 20 '17 at 13:03
• I think it is the third to last paragraph that puzzles me with regard to the exact nature of your uncertainty. You say it's weird to you to have both, and say that they always seemed like different notions. The internal language of a topos keeps these notions essentially different. – Malice Vidrine Aug 20 '17 at 13:53
• One should note that the emphasis on intuitionistic higher-order predicate logic is because a lot of mathematics is done in higher-order predicate logic, so the ability to interpret higher-order predicate logic in a topos is a very valuable thing. – Hurkyl Aug 20 '17 at 17:11

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

• the propositions have enough structure to let us do (intuitionistic) first order logic and
• it is the case that $\mathrm{Prop:Type}$, in the appropriate sense that there is a predicate $p:\mathrm{Prop}\vdash\Phi(p)$ such that every predicate $\varphi$ on a type $X$ is equivalent to one of the form $x:X\vdash\Phi(f(x))$ for a unique $f:X\to\mathrm{Prop}$.

(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.

• This greatly clarifies things! Just a note for future reference: do these other (dependently typed) languages have any specific names? Any reference material on their definitions/semantics? – NullSpace Aug 21 '17 at 2:43
• The ones I have in mind are just variants on Martin-Loef type theory with very strong equality and axioms that guarantee there's a subobject classifier. So there's not much in the way of special semantics. – Malice Vidrine Aug 21 '17 at 8:46