<html><head></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space; ">Let me ask a simple question related to this discussion. When one talks about "untyped application" and "untyped abstraction" does one actually mean that internally every object has to be kept as a part of a pair (o, T) where the second component is a type expression such that Gamma |- o:T holds?<div><br></div><div>Vladimir.</div><div><br></div><div><br><div><div>On Aug 27, 2012, at 7:25 AM, Thierry Coquand wrote:</div><br class="Apple-interchange-newline"><blockquote type="cite">
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
<div 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"><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>
</div>
_______________________________________________<br>Agda mailing list<br><a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>https://lists.chalmers.se/mailman/listinfo/agda<br></blockquote></div><br></div></body></html>