  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.

Logic in Computer Science;Algebraic Topology;Category Theory