  We investigate partial functions and computability theory from within a
constructive, univalent type theory. The focus is on placing computability into
a larger mathematical context, rather than on a complete development of
computability theory. We begin with a treatment of partial functions, using the
notion of dominance, which is used in synthetic domain theory to discuss
classes of partial maps. We relate this and other ideas from synthetic domain
theory to other approaches to partiality in type theory. We show that the
notion of dominance is difficult to apply in our setting: the set of
$\Sigma_0^1$ propositions investigated by Rosolini form a dominance precisely
if a weak, but nevertheless unprovable, choice principle holds. To get around
this problem, we suggest an alternative notion of partial function we call
disciplined maps. In the presence of countable choice, this notion coincides
with Rosolini's.
  Using a general notion of partial function, we take the first steps in
constructive computability theory. We do this both with computability as
structure, where we have direct access to programs; and with computability as
property, where we must work in a program-invariant way. We demonstrate the
difference between these two approaches by showing how these approaches relate
to facts about computability theory arising from topos-theoretic and
type-theoretic concerns. Finally, we tie the two threads together: assuming
countable choice and that all total functions $\mathbb{N}\to\mathbb{N}$ are
computable (both of which hold in the effective topos), the Rosolini partial
functions, the disciplined maps, and the computable partial functions all
coincide. We observe, however, that the class of all partial functions includes
non-computable partial functions.
