Simon Thompson: Type theory and functional programming. International computer science series, Addison-Wesley 1991, ISBN 978-0-201-41667-1, pp. I-XV, 1-372