Categories with families/attributes have been used to construct a number of models of dependent type theory with interesting logical properties, including Hoffman and Streicher's groupoid model that interprets contexts as groupoids and refutes uniqueness of identity proofs. Fabian Ruch showed how this model could be extended into a groupoid-valued presheaf model that validates the univalence axiom, but refutes the axiom of choice and the law of excluded middle.
Ruch's work on a sheaf model for type theory introduced a patching condition to types in order to force levelwise inhabited propositions to be contractible. However, it applied this patching condition in a fairly indirect way. Coquand, Mannaa and Ruch published a brief paper ('Stack Semantics of Type Theory') that applies prestack and stack patching conditions to types, but does not construct this model to be as general as possible.
This talk describes the basis of a master's project building on the above sheaf and stack models. In this talk I will introduce a more general stack model of dependent type theory by describing its structure as a category with attributes. I will describe possible directions this project may take.