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

生成讲解博客的中文版本

生成AI智能校验的中文版本