Bart Jacobs wrote a 700+ page volume called _[Categorical Logic and Type Theory][1]_ which gives a uniform treatment of various type theories ($X$-type theory, where $X\subseteq \{ \text{simple},$ $\text{dependent},$ $\text{polymorphic},$ $\text{higher-order}\}$) based on the categorical notion of [Grothendieck fibrations][2] (also called a cartesian fibrations). 
The notion of [Topos][3], also due to Grothendieck, plays a heavy role in providing categorical semantics to logics and type theories, which is of interest to logicians and theoretical computer scientists alike. 


  [1]: http://www.cs.ru.nl/B.Jacobs/CLT/bookinfo.html
  [2]: http://ncatlab.org/nlab/show/Grothendieck+fibration
  [3]: http://en.wikipedia.org/wiki/Topos