Partial elements and recursion in univalent type theory

We begin by revisiting partial functions in type theory, working in a constructive univalent type theory. We look at the notion of partiality via the notion of dominance, originally introduced to study synthetic computability and domain theory in topos logic, with models in realizability toposes. We then perform first steps in computability theory within such a constructive type theory without assuming countable choice or Markov’s principle. Our guiding question is what, if any, notion of partial function allows the proposition "all partial functions from N to N are Turing computable" to be consistent in constructive univalent type theory.

This is joint work with Cory Knapp.