Towards a homotopy domain theory

Abstract

Solving recursive domain equations over a Cartesian closed 0-category is a way to find extensional models of the type-free λ-calculus. In this work we seek to generalize these equa- tions to “homotopy domain equations”; to be able to set about a particular Cartesian closed “(0,∞)-category”, which we call the Kleisli ∞-category, and thus find higher λ-models, which we call “λ-homotopic models”. To achieve this purpose, we had to previously generalize c.p.o’s (complete partial orders) to c.h.p.o’s (complete homotopy partial orders); complete ordered sets to complete (weakly) ordered Kan complexes, 0-categories to (0,∞)-categories and the Kleisli bicategory to a Kleisli ∞-category. Continuing with the semantic line of λ-calculus, the syntactical λ-models (e.g., the set D∞), defined on sets, are generalized to “homotopic syntactical λ-models” (e.g., the Kan complex “K∞”), which are defined on Kan complexes, and we study the relationship of these models with the homotopic λ-model. Finally, from the syntactic point of view, what the theory of an arbitrary homotopic λ-model would be like is explored, which turns out to contain a theory of higher λ-calculus, which we call Homotopy Type-Free Theory (HoTFT); with higher βη-contractions and thus with higher βη-conversions.