Under propositions as types, a statement like $$\forall x \in \mathbb{R}, \exists y \in \mathbb{R}(x+y=0),$$ is viewed as a kind of "box" equipped with some methods for constructing elements of that box, which are viewed as proofs of the relevant theorem.
Philosophically at least, this allows us to formalize certain "assignment problems" that can be given to university students; in particular, it allows us to formalize problems of the form
"Prove $\varphi$."
by writing down the type $\varphi$ and giving it to the student. Their task is then to write down a well-formed term of the relevant type, i.e. a proof.
Suppose we wanted to generalize this kind of thinking so that it encompasses other kinds of problems too. For example:
"Compute $\tau$."
We want to hold onto the idea that each problem should be a type, and that solutions to that problem should be terms of that type.
If you ponder this for a bit, it quickly becomes clear that we need types that don't have enough "incoming functions" (constructors) to be sets.
For instance, to express "compute $31+17$" as the third problem on an assignment, we could try writing down $$\mathrm{Problem}_3 := \bigsqcup_{n:\mathbb{N}_{\mathrm{baseTen}}} U(n) = U(31)+U(17),$$
where $U : \mathbb{N}_{\mathrm{baseTen}} \rightarrow \mathbb{N}$ is the function that turns a base $10$ representation of a natural number into the underlying number. It follows that a term of type $\mathrm{Problem}_3$ consists of a $b \in \mathbb{N}_{\mathrm{baseTen}}$ together with a proof that $U(b) = U(31)+U(17).$
The problem is that its too easy to cheat: just let $$U^{-1} : \mathbb{N} \rightarrow \mathbb{N}_{\mathrm{baseTen}}$$ denote the relevant inverse function, let $b = U^{-1}(U(31)+U(17)),$ and offer the trivial proof of equality, based on the fact that $U$ and $U^{-1}$ are inverse functions. This allows us to construct a term of type $\mathrm{Problem}_3$ without actually doing any computations. Obviously, this is very bad.
This leads me to believe that we need to be thinking of $\mathbb{N}_{\mathrm{baseTen}}$ from a non-set-theoretic perspective, so that it's possible for $U^{-1}$ to fail to exist, despite that $U$ is obviously a bijection. Said in different words, it seems that we need a foundation of math in which there exist "sets" that don't have enough incoming functions to be sets.
Question. I've heard of "intensional type theory" but I don't know much about it.
My questions are:
Does intensional type theory allow us to define "sets" that don't have enough incoming functions to be sets?
If not, are there any foundations out there that do?