Expand App. B.1 to discuss principles compatible with decidable equality and program extraction

[UlrikBuchholtz]

See title. Mention the solution to Voevodsky's conjecture on homotopy canonicity, cubical type theories, etc., as well as the still-open question of constructive status of propositional resizing.