<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">
<div> Hello Andreas,</div>
<br>
<div>
<div><br>
</div>
<div> You write</div>
<blockquote type="cite">
<div><font class="Apple-style-span" color="#000000"><br>
</font>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.<br>
<br>
For a categorical semantics, additional type annotation at application seems useful, see Streicher's PhD.<br>
</div>
</blockquote>
</div>
<div><br>
</div>
<div> On the other hand, using Theorems 4.12 and 4.13 of Streicher's PhD </div>
<div>one can give categorical and set-theoretic semantics as well of the calculus with "untyped application</div>
<div>and even with untyped function abstraction" , which is the calculus used in Agda.</div>
<div>(Using these results one can lift any derivation of the untyped calculus into a typed one in an essentially</div>
<div>unique way.)</div>
<div><br>
</div>
<div><br>
</div>
<div><span class="Apple-tab-span" style="white-space:pre"></span>Best regards,</div>
<div><br>
</div>
<div><span class="Apple-tab-span" style="white-space:pre"></span>Thierry</div>
</body>
</html>