Hurewicz fibrations in elementary toposes

TL;DR

This paper explores how classical topological concepts like Hurewicz fibrations can be translated into the setting of elementary toposes with NNO, using a special interval notion and weak factorisation systems.

Contribution

It introduces a formal framework for Hurewicz fibrations in elementary toposes, extending topological ideas to categorical logic with new structures.

Findings

Established a category of fibrant objects in toposes with a specific interval structure

Derived fibrations from a weak factorisation system

Provided a categorical analogue of topological fibrations

Abstract

We study formal counterparts of Hurewicz fibrations and related topological notions in elementary toposes with NNO. The constructions are based on a specific notion of interval and lead to a structure of category of fibrant objects on toposes equipped with such a datum. We get in fact slightly more as the building blocks are derived from a weak factorisation system.