On the Use of Computational Paths in Path Spaces of Homotopy Type Theory