Kripke-Joyal forcing for type theory and uniform fibrations
Submitted to Advances in Mathematics, 2021
"Kripke-Joyal forcing for type theory and uniform fibrations", written with S. Awodey and N.Gambino arXiv:2110.14576, 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.
Leave a Comment