[hiker]

Yes for the fragment of total and noncomputable functions which mathematicians use. For partial functions (which Lean also supports) I think the same arguments hold as for the "Haskell Category".