Homotopy Theory has become one of the most powerful fields of the modern mathematics, creating strong links between algebraic topology and category theory, algebraic geometry and computational logic. The goal of Univalent Type Theory (UniTT+hit) has been to provide a constructive and computational framework that is able to precisely and logically capture homotopy-theoretic ideas in recent years. In the present paper, we discuss how to construct homotopy groups, pushouts, suspensions, wedges, pointed types, CW complexes and Eilenberg-Steenrod cohomology in Univalent Type Theory. Special focus is paid to the interpretation of equality as identification as path, which allows to build up higher-dimensional groupoids and homotopy structures. The paper also touches on the application of UniTT+hit to automate homotopy theoretic proofs and to constructively use cohomological structures using computational techniques. New ideas like cellular cohomology, transport, finite dimensional CW complexes, and reduced cohomology theories are discussed algebraic and topologically. As another significant contribution to the theory of homotopy, the equivalence conjecture between cellular cohomology and ordinary reduced cohomology is studied. The use of constructive mathematics and computational reasoning will assist in developing the foundations of homotopy theory, while also moving towards the goal of verified and mechanized mathematics.