Cartmell showed that the category of generalized algebraic theories is equivalent to the category of contextual categories. This implies that the theory of generalized algebraic theories is essentially algebraic. We characterize the essentially algebraic theory of generalized algebraic theories as the free category with finite limits and with an exponentiable arrow.
The main theorem and a syntactic proof are found in this arXiv paper. In this talk we give a semantic proof.
This video is part of Masaryk University‘s Algebra seminar.
