Solving Homotopy Domain Equations
Daniel O. Martínez-Rivillas, Ruy J. G. B. de Queiroz
TL;DR
This work generalizes Dana Scott's Domain Theory to a Homotopy Domain Theory (HoDT) by moving from cartesian closed categories to cartesian closed ∞-categories and from complete partial orders to complete homotopy partial orders, enabling λ-models that encode higher equalities via ∞-groupoids. It develops a general method for solving Homotopy Domain Equations on arbitrary cartesian closed ∞-categories using ω-diagrams and fixed-point techniques, yielding a fixed point K ≃ $K \Rightarrow K$ for the equation $K \simeq (K \Rightarrow K)$ and thus constructing homotopy λ-models. The paper then instantiates this framework on Kl(P), demonstrating the existence of non-trivial Kan complexes in Fix(F) and producing non-trivial homotopy λ-models with rich higher-dimensional information. These results establish foundational machinery for higher-dimensional λ-calculus semantics and HoDT, with planned extensions toward typed HoDT and HoTT-related semantics and potential integration into interactive theorem provers.
Abstract
In order to get $λ$-models with a rich structure of $\infty$-groupoid, which we call "homotopy $λ$-models", a general technique is described for solving domain equations on any cartesian closed $\infty$-category (c.c.i.) with enough points. Finally, the technique is applied in a particular c.c.i., where some examples of homotopy $λ$-models are given.