Naive homotopy theories in cartesian closed categories

An elementary notion of homotopy can be introduced between arrows in a cartesian closed category E. The input is a finite-product-preserving endofunctor Π₀ with a natural transformation p from the identity which is surjective on global elements. As expected, the output is a new category Eₚ with objects the same objects as E. Further assumptions on E provide a finer description of Eₚ that relates it to the classical homotopy theory where Π₀ 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ₚ is naturally described in terms of explicit homotopies -- as is the internal notion of contractible space.