I explain some of the ideas that were presented at the Homotopy Type Theory conference 2023 at Carnegie Mellon University. In particular, I explain the construction of Riehl and Shulman's theory of synthetic $(\infty,1)$-categories through their simplicial type theory. I also discuss synthetic algebraic geometry, other extensions of homotopy type theory, and the unifying theory of modal type theory.
