Synthetic Topology in Homotopy Type Theory for Probabilistic Programming