Extensional constructs in intensional type theory - Hofmann, Martin (Springer, 1997)