I would like to find a reference that describes the semantics of constructive higher order logic *with function types* in toposes. In particular, it seems that if we are to take function types as primitive, then we need the **definite description operator** $\iota x. P(x)$, which produces a term that satisfies $\exists ! x. P(x) \implies P(\iota x. P(x))$. This is required to prove the principle of unique choice. And if we want the function type to actually be useful this principle is a must. For Isabelle/HOL and HOL Light, the even stronger *indefinite* description operator $\epsilon x. P(x)$ is used, validating choice.


However, I can't work out the semantics of this operator myself. This operator would produce a term no matter whether $P(x)$ actually has a unique solution $x$.
So this would produce a map $\iota : \mathcal P(X) \to X$ in any topos where $X$ is the interpretation of the type of $x$. In the classical case this is fine because we can just case split and assign a junk value. But this doesn't sound possible in an arbitrary elementary topos.


In the literature: the Elephant did mention function types, but it did not talk about definite descriptions at all, and in its definition of the formal system ($\tau$-theory) it did not include function types because we already have powerset types and "we shall keep the logic as simple as possible by leaving them out". This avoids the problem because defining functions as functional relations $\psi : \mathcal P(A \times B)$ makes the principle of unique choice a theorem. In *Introduction to Higher Order Categorical Logic* by Lambek and Scott, there are also no function types.


So, what is the right way of having function types, and ensuring the principle of unique choice? Do we not use definite description, and instead just add an axiom? Or is there another way out? Any reference on this matter is welcome.



Topos semantics of constructive higher order logic
Categorical logic texts such as Lambek & Scott's "Introduction to higher-order categorical logic" and Johstone's "Elephant" usually focus on the categorical side of things and are often a bit cavalier about the details of the internal language – enough so to require significant adjustments before one can actually think about implementing it.


Regarding the definite description operator, you can look at Theorem 5.9 of Lambek & Scott, but that's in a section about the internal language, so the authors have the freedom to switch to the categorical side whenever needed, and they do.


Regarding setting up the internal language of a topos qua cartesian-closed category with a subobject classifier, finite coproducts, and coequalizers, I recommend Wesley Phoa's [An introduction to fibrations, topos theory, the effective topos and modest sets](http://www.lfcs.inf.ed.ac.uk/reports/92/ECS-LFCS-92-208/). The precision of detail in the text surpasses other sources that I am familiar with. In particular, the appendix spells out both the details of the formal system, and its interpretation in a topos. The definite description operator is treated on page 61, and in the appendix on pages 134 and 142. As you will see there, the categorical construction of the semantics of the definite description is the most complicated part of the semantics of the internal language of a topos.


Good luck converting a Postscript file to a readable PDF!


