Constructive Simplicial Homotopy

TL;DR

This paper develops an internal simplicial homotopy framework suitable for realizability toposes, advancing models of homotopy type theory without relying on classical principles.

Contribution

It introduces a foundational approach to internal simplicial homotopy compatible with realizability toposes, enabling new model constructions in homotopy type theory.

Findings

Established a classical principle-free internal simplicial homotopy theory

Provided foundational tools for realizability-based models of homotopy type theory

Facilitated the development of new models in homotopy type theory

Abstract

This paper aims to help the development of new models of homotopy type theory, in particular with models that are based on realizability toposes. For this purpose it develops the foundations of an internal simplicial homotopy that does not rely on classical principles that are not valid in realizability toposes and related categories.