Syntax for anonymous functions [Re: [Agda] AIM XIII code sprints]

[Thierry Coquand]

 About


>> or
>> 
>> 2. Definitional equality becomes "more intensional", so that we can't
>> even assert (\x ->  x) == (\x ->  x).  Really, this would be raising the
>> question of whether definitional equality is a useful notion at
>> functional type.


the paper

Martin-Löf, P.: An intuitionistic theory of types: predicative part. 
In: H.E. Rose and J. Shepherdson (eds.) Logic Colloquium '73, North-Holland, Amsterdam, 1975. 

follows an approach reminiscent of 2 (with an elegant proof of Church-Rosser).

          Thierry