The Theory of an Arbitrary Higher \(\lambda\)-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.

Keywords

• higher lambda calculus
• homotopic lambda model
• kan complex reflexive
• higher conversion
• homotopy type-free theory