During the lecture of Bainbridge,Freyd Scedrov,Scott's-paper "Functorial Polymorphism" (TCS 90) the following questions arose: \item Does the authors' construction of an interpretation of PLC d efinitely imply that there is a categorical PLC-model in the sense of Reynolds in which $\forall \alpha.(T(\alpha)->\alpha)->\alpha$ is interpreted as the initial T-Algebra? \item Does this model (if there is one) have an object with two distinguishable points, or equivalently is true <> false ? \item Does the model construction described extend to a model of the Calculus of Constructions or even ECC, so that we could consistently add an axiom claiming the initiality of $\forall \alpha.(T(\alpha)->\alpha)->\alpha$ using Leibniz's equality (And $not (true = false)$ of course)? Could anyone -- perhaps the authors themselves -- help me to get answers to these problems? -- Martin Hofmann P.S. I'm a grad-student working on verification of ML-programs with ECC and I've represented ML's datatypes using the above quoted T-algebra-expression. ====================================