Constructive higher sheaf models with applications to synthetic mathematics

TL;DR

This paper develops constructive higher sheaf models of type theory, enabling formal systems like synthetic algebraic geometry and Stone duality within a constructive framework.

Contribution

It provides a foundational approach to higher sheaf models of type theory, facilitating constructive models of advanced synthetic mathematics systems.

Findings

Constructive models of synthetic algebraic geometry established.

Higher sheaf models support univalence and higher inductive types.

Framework enhances formal reasoning in synthetic mathematics.

Abstract

There have recently been several developments in synthetic mathematics using extensions of dependent type theory with univalence and higher inductive types: simplicial homotopy type theory, synthetic algebraic geometry and synthetic Stone duality. We provide a foundation of higher sheaf models of type theory in a constructive metatheory and, in particular, build constructive models of these formal systems.