Categorical semantics preliminaries

Definition (Uemura). A category with representables (CwR) is a finite limit category \(\mc{P}\) equipped with a class \(R_{\mc{P}}\) of morphisms, the elements of which are called representable, such that

1. \(R_{\mc{P}}\) is closed under pullback and composition.
2. Morphisms in \(R_{\mc{P}}\) are exponentiable.

Definition. A second order generalized algebraic theory is a syntactic presentation of a category with representables.

Example. Type theory with \(\Sigma\) types

\[\begin{align*} &\ms{Ty} \colon \ms{Jdg} \\ &\ms{El} \colon \ms{Ty} \to \ms{Jdg}^+ \\ &\Sigma \colon (A \colon \ms{Ty}) \to (\ms{El}\,A \to \ms{Ty}) \to \ms{Ty} \\ &\Sigma/\ms{univ\text{-}prop} \colon (a \colon \ms{El}\,A) \times \ms{El}\,(B\,a) \cong \ms{El}\,(\Sigma\,A\,B) \end{align*}\]