Partial Functions and Recursion in Univalent Type Theory