What is a normalization?

Stream: new members

[Kuminiko]

Hi! I worked through 5 chapters of "theorem proving in Lean 4", and also read chapter 12 in which they state that propositional extensionality blocks normalization. My question is: what is a normalization? They gave example "every expression of type Nat is a numeral", which I understand, but this is an example, not a definition. What is a normal form of an expression of more general inductive or functional type? And, morally, why propositional extensionality somehow "blocks" it?

[Sebastian Ullrich]

The reference has an entry on normal forms and propext including blocking example, does that help?

[Kuminiko]

Yes, exactly what I need, thank you