Well, the correspondence sounds interesting but if remains just on the level of the unexplained, it is hard to see it really being interesting.
If you define a function, call it a "type" and then take the Taylor series of that function, how mind blowing is that really?
My point is that without a motivation to these constructions, they are just constructions. It may be everyone in-the-know understands the motivation already, knows why this thing labeled type really has a "deep" relation to an abstract type-thing. Fair enough but I'm just saying if one omits this motivation, your whole exercise doesn't look interesting to those not in-the-know, OK?