Kripke-Joyal forcing for type theory and uniform fibrations
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.
v2. 56 pages. Minor changes following referee report. To appear in Selecta Mathematica, New Series
References in corpus (11)
- Polynomial functors and polynomial monads
- Understanding the small object argument
- The identity type weak factorisation system
- Algebraic weak factorisation systems I: accessible AWFS
- The Frobenius Condition, Right Properness, and Uniform Fibrations
- Algebraic weak factorisation systems II: categories of weak maps
- Axioms for Modelling Cubical Type Theory in a Topos
- Stack semantics and the comparison of material and structural set theories
- The Equivalence Extension Property and Model Structures
- Models of Martin-Löf type theory from algebraic weak factorisation systems
- Kripke Semantics for Martin-Löf's Extensional Type Theory