The Theory of an Arbitrary Higher λ-Model
share
One takes advantage of some basic properties of every λ-homotopic model (e.g. reflexive Kan complex) to explore two types of higher βη-conversions: the first, from the higher βη-contractions (we denoted those by (n+1)-βη-contractions) of a lower βη-conversion. Second, starting from the classical conversions, λ^n-terms are introduced inductively by application and abstraction of lower βη-conversions, to get other types of higher βη-contractions (we denoted those by (βη)_n+1-contractions) between those λ^n-terms already defined.
READ FULL TEXT