This is a preliminary investigation into whether there exists a suitable type theory for the category of pointed topological spaces. In short, we would prefer if the HoTT book began with topological intuitions, and justified its use of type theory as it progressed.
