Kripke-Joyal forcing for type theory and uniform fibrations

Link to journal publication

arXiv Preprint, 2021. 55 pages.

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.