Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Kripke-Joyal forcing for type theory and uniform fibrations

S. Awodey, N. Gambino, S. Hazratpour

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.

Kripke-Joyal forcing for type theory and uniform fibrations

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.

Paper Structure

This paper contains 3 sections, 8 theorems, 22 equations.

Table of Contents

  1. Presheaf categories
  2. Small maps and subobjects
  3. The type theory of a presheaf category

Key Result

Proposition 1.3

Let $f\colon Y\to X$ and $\alpha\colon X\to U$. Then the following data are in bijective correspondence:

Theorems & Definitions (17)

  • Definition 1.1
  • Remark 1.2
  • Proposition 1.3
  • Proposition 1.4
  • Remark
  • Proposition 1.5
  • Remark
  • Proposition 2.1
  • Corollary 2.2
  • Remark 2.3
  • ...and 7 more