I've finally got around to get an idea of what is going on with transseries. So, as I understand it, by tuning the construction of a class of transmonomials (typically an inverted order), you can represent certain spaces of function as infinite power series over these. I haven't seen how transseries, which seem to be uncountable, are represented in computer algebra systems, and how, given heterogenous transmonomials P < P' and Q < Q', we can decide whether PQ' < P'Q.

"I think Mac Lane-Moerdijk prove that an initial object is strict in a cartesian closed category" - This may well be right, but in their discussion of Joyal's proof of the isomorphism you give, Lambek and Scott (1986, p67 and p116) do not mention any such result, which would be surprising if they were then aware of it.