nLab A1-homotopy type theory

Idea

$\mathbb{A}^1$-homotopy type theory or motivic homotopy type theory is a hypothetical modal homotopy type theory which provides a synthetic foundation for $\mathbb{A}^1$-homotopy theory, where the affine line is the standard affine line in the Nisnevich site of smooth schemes of finite type over a Noetherian scheme.

Mitchell Riley‘s bunched linear homotopy type theory [Riley (2022)] is a synthetic foundations for parameterized stable homotopy theory. This may provide a basis for a motivic homotopy type theory.

Results

• There is a shape modality in $\mathbb{A}^1$-homotopy type theory given by the $\mathbb{A}^1$-localization higher inductive type.

• There is no cohesive flat modality in $\mathbb{A}^1$-homotopy type theory as otherwise that will imply the false statement that the category of $\mathbb{A}^1$-local objects is a topos. Thus $\mathbb{A}^1$-homotopy type theory is not a cohesive homotopy type theory.

See also

• modal homotopy type theory
• $\mathbb{A}^1$-homotopy theory

References

• Synthetic Algebraic Geometry in the Zariski-Topos (Github)