# Set-theoretic encoding of functions in type theory

Functions usually get encoded in set theory as follows. A function $$A\to B$$ is a subset $$f\subset A\times B$$ such that $$\pi_1:f\to A$$ is a bijection.

In type theory to give a function $$A\to B$$ is to write a program computing a term of $$B$$ given a term of $$A$$.

But can we simulate the set-theoretic notion of function in type theory? Is this a useful notion? Are there references on this?

• Does B. Werner's 1997 paper Sets in types, types in sets help? B. Barras has a related paper Sets in Coq, Coq in Sets. Apr 2, 2021 at 15:47
• The axiom of unique choice (validated by any topos) is commonly added to type theory precisely to pass back and forth between these two definitions of function. Such a formulation typically requires a type of propositions, which let's us recast "subset" to "predicate". This can be handy for proving that e.g., a certain function is invertible by proving that it is merely injective and surjective. Apr 3, 2021 at 16:36