Categorical logic and type theory - Jacobs, Bart (Elsevier, 1999)