Thanks

I guess Martin-Löf speaks about W-Types.

An implementation and examples in Coq:

https://github.com/coq/coq/wiki/WTypeInsteadOfInductiveTypes

Still waiting for the year of W-Types