From a categorical perspective the above-mentioned structures may appear somewhat special and ad hoc. A more regular structure which gives rise to models of intuitionistic type theory are the locally cartesian closed categories. These are categories with a terminal object, where each slice category is cartesian closed. It can be shown that the pullback functor has a left and a right adjoint, representing \(\Sigma\)- and \(\Pi\)-types, respectively. Locally cartesian closed categories correspond to intuitionistic type theory with extensional identity types and \(\Sigma\) and \(\Pi\)-types (Seely 1984, Clairambault and Dybjer 2014). It should be remarked that the correspondence with intuitionistic type theory is somewhat indirect, since a coherence problem, in the sense of category theory, needs to be solved. The problem is that in locally cartesian closed categories type substituion is represented by pullbacks, but these are only defined up to isomorphism, see Curien 1993 and Hofmann 1994.