[Agda] Typed vs untyped lambda abstractions

[Thierry Coquand]

 Hello Andreas,


 You write

When building a set-theoretic semantics, the type annotation at the lambda lets you build a set-theoretic function, so you can define the denotation of a term directly.

For a categorical semantics, additional type annotation at application seems useful, see Streicher's PhD.

 On the other hand, using Theorems 4.12 and 4.13 of Streicher's PhD
one can give categorical and set-theoretic semantics as well of the calculus with "untyped application
and even with untyped function abstraction" , which is the calculus used in Agda.
(Using these results one can lift any derivation of the untyped calculus into a typed one in an essentially
unique way.)


Best regards,

Thierry
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20120827/516481d7/attachment.html