Bart Jacobs wrote a 700+ page volume called Categorical Logic and Type Theory 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 (also called a cartesian fibrations). The notion of Topos, 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.

Grothendieck's impact can be felt in type theory and logic. For instance, Bart Jacobs' 700+ page volume Categorical Logic and Type Theory 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 (also called a cartesian fibrations). Similarly, the notion of Topos, 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.