For inductive type `T` what is its initial algebra?

Stream: lean4

[nrs]

I'm trying to make use of recursion schemes directly in Lean without explicitly making a theory of polynomial functors in which to express W-types as objects distinct from Lean's normal types, and I'm trying to express the articles that discuss recursion schemes in this setting. In the HoTT book, for an inductively defined type T it seems like either the recursor or the induction principle for T plays the role of the map f in the pair (T,f) that forms the initial algebra for the type T, and it seems to be guaranteed that such an initial algebra exists by virtue of T being a W-type. That's in the HoTT setting but according to Mario Carneiro's thesis, Lean inductive types can also be reduced to W-types.

Given these bits of info, do we know if all Lean inductive types have a canonical initial algebra?

[nrs]

Can anyone confirm whether .rec is the type-theoretical dependent eliminator? In which case it is maybe the above-mentioned f?

[Mario Carneiro]

The question is slightly confusing to me. An inductive type is the initial object of the algebra of types having functions with the type of the constructors

[Mario Carneiro]

.rec is the unique map out of the initial object into another object of the category

[nrs]

Mario Carneiro said:

.rec is the unique map out of the initial object into another object of the category

Thank you very much for all your answers I have still not been able to digest most of them but it is my main focus right now to understand them fully, also very big fan of your work!!