The Theory of an Arbitrary Higher $\lambda$-Model

TL;DR

This paper explores the properties of homotopic λ-models, particularly higher βη-conversions, and adapts identity types with computational paths to a type-free setting, advancing the understanding of equality in higher λ-theories.

Contribution

It introduces a framework for analyzing higher λ-models and their equality rules, extending the theory of homotopic λ-models to include higher λ-terms and type-free equality.

Findings

Higher βη-conversions correspond to proofs of equality in homotopic λ-models

Identity types with computational paths can be adapted to type-free higher λ-theories

The equality rules are consistent with the theory of any λ-homotopic model

Abstract

One takes advantage of some basic properties of every homotopic $\lambda$-model (e.g.\ extensional Kan complex) to explore the higher $\beta\eta$-conversions, which would correspond to proofs of equality between terms of a theory of equality of any extensional Kan complex. Besides, Identity types based on computational paths are adapted to a type-free theory with higher $\lambda$-terms, whose equality rules would be contained in the theory of any $\lambda$-homotopic model.