Currently, this section contains only technical stuff. We can add some prose here. Moreover it would be nice to see the two failed attempts to define interpretation on an universal type: the first one that motivates environment η, and the second that motivates quantification over semantic types.
Currently, this section contains only technical stuff. We can add some prose here. Moreover it would be nice to see the two failed attempts to define interpretation on an universal type: the first one that motivates environment η, and the second that motivates quantification over semantic types.