Constructive sheaf models of type theory

Thierry Coquand, Fabian Ruch, Christian Sattler

We generalise sheaf models of intuitionistic logic to univalent type theory over a small category with a Grothendieck topology. We use in a crucial way that we have constructive mo…