Here we collect articles about doing topology in HoTT.

- cohesive homotopy type theory
- spaces and homotopy types
- 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

- 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?