Naive homotopy theories in cartesian closed categories

TL;DR

This paper introduces a simple notion of homotopy within cartesian closed categories using a finite-product-preserving endofunctor, connecting to classical homotopy theory and providing explicit descriptions in certain topos settings.

Contribution

It defines a new homotopy concept in cartesian closed categories via a functor with natural transformation, linking to classical homotopy and describing contractibility in specific topos contexts.

Findings

Defines homotopy using a functor and natural transformation.

Relates the new homotopy to classical topological homotopy.

Provides explicit descriptions in 2-value topos with precohesion.

Abstract

An elementary notion of homotopy can be introduced between arrows in a cartesian closed category $E$. The input is a finite-product-preserving endofunctor $\Pi_0$ with a natural transformation $p$ from the identity which is surjective on global elements. As expected, the output is a new category $E_p$ with objects the same objects as $E$. Further assumptions on $E$ provide a finer description of $E_p$ that relates it to the classical homotopy theory where $\Pi_0$ could be interpreted as the ``path-connected components'' functor on convenient categories of topological spaces. In particular, if $E$ is a 2-value topos the supports of which split and is furthermore assumed to be precohesive over a boolean base, then the passage from $E$ to $E_p$ is naturally described in terms of explicit homotopies -- as is the internal notion of contractible space.