A Syntactic Characterization of the Equality in Some Models for the Lambda Calculus
Martin Hyland · Journal of the London Mathematical Society · 1976
An equality relation on the terms of the A-calculus is an equivalence relation closed under the (syntactical) operations of application and A-abstraction. We may distinguish between syntactic and semantic ways of introducing equality relations, /^-equality is introduced syntactically; it is the least equality relation satisfying the