An elementary notion of homotopy can be introduced between arrows in a cartesian closed category E. The input is henceforth called connectedness structure: a finite-product-preserving endofunctor Π_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 Π_0 could be interpreted as the "path-connected components" functor on convenient categories of topological spaces. If E is a topos such that any non initial object has points and is furthermore assumed to be precohesive over a boolean base (as is the case for some classical models of Synthetic Differential Geometry), then there is an obvious choice of connectedness structure p. In this case, the passage from E to E_p is naturally described in terms of explicit homotopies - and so is the internal notion of contractible space. Furthermore, they coincide with the suggestions of Lawvere in his proposal for Axiomatic Cohesion.
Keywords: Topos, connectedness, precohesion
2020 MSC: Primary 18B25; Secondary 55U40
Theory and Applications of Categories, Vol. 44, 2025, No. 19, pp 565-587.
Published 2025-06-24.
TAC Home