# The $\infty$-groupoid generated by an arbitrary topological $\lambda$-model

## TL;DR

This paper constructs an $$-groupoid from topological lambda models, revealing limitations of Scott topology and proposing a new approach to higher-order proofs in lambda calculus.

## Contribution

It introduces a method to generate $$-groupoids from topological lambda models, expanding the understanding of their homotopical structure.

## Key findings

- Scott topology lacks information on higher homotopies
- Constructed $$-groupoid from lambda models with topology
- Proposes exploring non-trivial $$-groupoids for higher proofs

## Abstract

The lambda calculus is a universal programming language. It can represent the computable functions, and such offers a formal counterpart to the point of view of functions as rules. Terms represent functions and this allows for the application of a term/function to any other term/function, including itself. The calculus can be seen as a formal theory with certain pre-established axioms and inference rules, which can be interpreted by models. Dana Scott proposed the first non-trivial model of the extensional lambda calculus, known as $ D_\infty$, to represent the $\lambda$-terms as the typical functions of set theory, where it is not allowed to apply a function to itself. Here we propose a construction of an $\infty$-groupoid from any lambda model endowed with a topology. We apply this construction for the particular case $D_\infty$, and we see that the Scott topology does not provide enough information about the relationship between higher homotopies. This motivates a new line of research focused on the exploration of $\lambda$-models with the structure of a non-trivial $\infty$-groupoid to generalize the proofs of term conversion (e.g., $\beta$-equality, $\eta$-equality) to higher-proofs in $\lambda$-calculus.