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