The synthetic algebraic geometry (SAG) project (of Cherubini, Coquand, Hutzler, etc.) has used sheaf models of type theory as the internal language of the big and little Zariski toposes. To encode higher geometric structure, Richard and I have been exploring stack models of type theory. Specifically, we have followed two constructions: an ‘external stack model’ built from the 2-category of stacks mapping from a given site into a 2-category with structure modelling type theory, and an ‘internal stack model’ constructed from internal notions of a category and Grothendieck topology within an initial type-theoretic model. I will present some of our findings thus far.