Kripke-Joyal forcing for type theory and uniform fibrations

S. Awodey, N. Gambino, S. Hazratpour

We introduce a new method for precisely relating certain kinds of algebraic structures in a presheaf category and judgements of its internal type theory. The method provides a syst…