The Theory of an Arbitrary Higher \(λ\)-Model - Martínez-Rivillas, Daniel O.; de Queiroz, Ruy J. G. B. (Bulletin of the Section of Logic, 2023)
One takes advantage of some basic properties of every homotopic \(λ\)-model (e.g. extensional Kan complex) to explore the higher \(βη\)-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 \(λ\)-terms, whose equality rules would be contained in the theory of any \(λ\)-homotopic model.