(What is the main theorem of logic? The abstract completeness theorem: first-order logical validity is a recursively enumerable concept, in fact, complete-r.e., i.e. (complete) SIGMA-ZERO_ONE in the arithmetical hierarchy, which is a hierarchy based of logical complexity based on counting unbounded quantifiers in the defining formulas - and (therefore), it (validity) is not recursive, i.e., not DELTA-ZERO, (equivalently, not PI-ZERO-ONE), in that hierarchy. [Theorem due to Godel and Church: go to S.C. Kleene: Intro to Metamathematics, 1952 and numerous later editions.])
I will endeavor to counteract the above "first impression" by talking about the following topics: 1) the fibrational formulation of logic; 2) the generalized sketch approach to syntax; 3) FOLDS = first-order logic with dependent sorts, 4) computads as the syntax for the logic of higher categories. This may sound a lot -- but I want to give some idea where categorical logic has gone since the subject of our book with Gonzalo Reyes of 1977.