Synthetic Domain Theory in Type Theory: Another Logic of Computable Functions