Better explanation of constructivity example in introduction

[AxelBoldt]

The explanation of the example in the "Constructivity" section in the introduction should mention that the equal signs really refer to types, namely the Id-types that were alluded to earlier in the "Homotopy type theory" section.

[mikeshulman]

In the section "Univalent foundations", we already used the notation = for identity types...