Homotopy Type Theory (HoTT) is a powerful theory that brings together computer science, higher dimensional mathematics and topology and logic. The theory is an extension of Martin-Löf Type Theory that includes identity types, higher inductive types and univalence, allowing the mathematical structures to be understood as both homotopical and computational. In this paper, I will explore the shift from the set-theoretic foundation to higher dimensional type-theoretic foundation, focusing on the conceptual importance of the identification types and the univalent foundations. The study also explores homotopy equivalence between intervals, homotopy-equivalent computational interpretations of interval structure and formal proof systems, and cubical type theories. Special emphasis is placed on the links between cubical methods and the formalisation of mathematical reasoning in a theorem prover. The paper also mentions some applications of higher dimensional types in topology, synthetic homotopy theory, patch theories, quotient constructions, and computational mathematics. Homotopy Type Theory combines geometric intuition and logical formalism to give a constructive and machine-verifiable base for modern mathematics. The talk illustrates how cubical approaches are able to address the shortcomings of intensional type theory whilst reinforcing the computational interpretation of equality, equivalence and higher-dimensional structures in current mathematical and computational practice.