<p>Hello,</p>
<p>I have a few questions about typed vs untyped lambda abstractions.</p>
<p>More specifically,<br>
1. I have the impression that categorical semantics of type theory is easier with typed lambdas, because for example the term &quot;\ x -&gt; x&quot; could be a lot of different functions but &quot;\ x : A -&gt; x&quot; is the identity function of A.<br>

Is that right? Do you have references of papers discussing categorical semantics of type theory with untyped lambdas?</p>
<p>2. What about syntactic study of type theory (confluence, strong normalisation, ...)? Is it easier with typed or untyped lambdas?</p>
<p>3. Why does Agda use untyped lambdas (internally)? Are there any advantages or drawbacks? I think that Coq uses typed lambdas, but I don&#39;t know if there is a difference from an implementation or user-friendliness point of view.</p>

<p>4. Using Agda&#39;s source code, is it easy to add type annotations to lambdas? In other words, if I have a term in Agda&#39;s internal syntax (of type Agda.Syntax.Internal.Term, I think), how do I translate it to a term in a lambda calculus with typed lambdas?<br>

I think I tried to find a suitable function in Agda&#39;s source code a few weeks ago, but I did not find anything.</p>
<p>Thank you,</p>
<p>Cheers,<br>
Guillaume</p>