Kripke-Joyal forcing for type theory and uniform fibrations

2021/10/27 by Awodey, S., Gambino, N., Hazratpour, S.
#03B38 #03G30 #18F20 #18N45 #Category Theory (math.CT) #FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.2110.14576

Abstract

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 systematic way to organise complex diagrammatic reasoning and generalises the well-known Kripke-Joyal forcing for logic. As an application, we prove several properties of algebraic weak factorisation systems considered in Homotopy Type Theory.

Related

• A category-theoretic version of the identity type weak factorization system
• Stable factorization from a fibred algebraic weak factorization system
• Constructive sheaf models of type theory
• Homotopy Type Theory: Univalent Foundations of Mathematics
• Formalizing Category Theory and Presheaf Models of Type Theory in Nuprl