Resources for semantics of inductive types?

Stream: new members

[nrs]

Hi, I've recently finished Pierce's Types and Programming Languages and his chapter about dependent types in the following book. I'm interested in learning about the semantics behind Coq and Lean's implementations of inductive types. Does anyone have resources on a path that could get me started? Thank you very much.

[Edward van de Meent]

The type theory of lean by @Mario Carneiro is about that, I believe...

[nrs]

Edward van de Meent said:

The type theory of lean by Mario Carneiro is about that, I believe...

Thank you for the reference!!!