Lambda Calculus And Homotopy Type Theory: Bridging The Gap Between Computation and Topology

This paper examines a formal connection between Lambda Calculus, the classical syntactic model of computation, and Homotopy Type Theory (HoTT), where types are viewed as spaces and equalities as paths. Although both frameworks are well established, they have largely evolved separately, with Lambda Calculus emphasising operational precision but little geometric structure, and HoTT offering rich homotopical semantics while leaving aspects of computation less explicit. To bridge this gap, the paper develops three main contributions: a compositional embedding of the simply typed lambda calculus into HoTT that interprets βη-equality as inhabited identity types; a unified semantic account of both systems within Cartesian closed ∞-topoi, where traditional Cartesian closed structure coexists with higher homotopical information; and a correspondence between computation and geometry, showing that β-reduction aligns with path composition and normalization with contractible path spaces. Beyond conceptual unification, the work highlights practical consequences, including the integration of verified functional programmes into homotopyaware proof assistants, the use of higher inductive types to internalize equational constraints, and the role of univalence in transporting correctness proofs across equivalent implementations. The paper concludes by noting limitations particularly the unsettled computational status of univalence and outlining future directions such as quantitative HoTT, enhanced proof automation, and applications to topological quantum computation. Keywords: Lambda Calculus, Homotopy Type Theory, Univalence, Higher Inductive Types, Curry-Howard Correspondence