2020/07/29 by Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz, Martínez-Rivillas, Daniel O. +1 · 2 citations
Computer Science · Mathematics · #FOS: Computer and information sciences #Homotopy and Cohomology in Algebraic Topology #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2007.15082
openalex publication_date 2020/07/29 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
An appropriate framework is put forward for the construction of λ-models with ∞-groupoid structure, which we call homotopic λ-models, through the use of an ∞-category with cartesian closure and enough points. With this, we establish the start of a project of generalization of Domain Theory and λ-calculus, in the sense that the concept of proof (path) of equality of λ-terms is raised to higher proof (homotopy).