Jacobs, B. (1999). Categorical Logic and Type Theory (Number 141). North Holland.
@book{jacobs:1999,
  author = {Jacobs, Bart},
  address = {Amsterdam},
  publisher = {North Holland},
  year = {1999},
  number = {141},
  series = {Studies in Logic and the Foundations of Mathematics},
  title = {Categorical Logic and Type Theory}
}