<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 "\ x -> x" could be a lot of different functions but "\ x : A -> x" 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't know if there is a difference from an implementation or user-friendliness point of view.</p>
<p>4. Using Agda's source code, is it easy to add type annotations to lambdas? In other words, if I have a term in Agda'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's source code a few weeks ago, but I did not find anything.</p>
<p>Thank you,</p>
<p>Cheers,<br>
Guillaume</p>