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?

  • $\begingroup$ 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. $\endgroup$ Commented Apr 2, 2021 at 15:47
  • 1
    $\begingroup$ 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. $\endgroup$ Commented Apr 3, 2021 at 16:36


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.