[[!redirects topology]] [[!redirects Topology in HoTT]] Here we collect articles about doing topology in HoTT. * [[cohesive homotopy type theory]] * [[space]]s and [[homotopy type]]s * [[discrete space]] * [[indiscrete space]] * [[underlying homotopy type]] * [[fundamental homotopy type]] * [[shape]] * [[flat]] * [[sharp]] * [[axiom R-flat]] (theorem if we assume I-flat) * [[real cohesive homotopy type theory]] * [[geometrically contractible space]] * [[contractibility of Dedekind real numbers]] * [[continuous mapping]] * [[discontinuous mapping]] * [[intermediate value theorem]] * [[continuous interval object]] * [[compact connected space]] * [[axiom of replacement]] * [[analytic Markov's principle]] ## Dedekind real numbers * [[order]] * [[strict order]] * [[dense strict order]] * [[extended Dedekind cut]] * [[Dedekind real unit interval]] * [[Dedekind real numbers]] * [[axiom I-flat]] * [[contractibility of Dedekind real unit interval]]