About the Identity function in Agda

I've defined the identity function in Agda as follows:

idd : (∀ {ℓ} {A: Set ℓ}) → A → A
idd a = a


I want to ask you if the following reasonings are correct:

• The type of this function is A -> A.
• idd is a polymorphic function, where (∀ {ℓ} {A: Set ℓ}) matches any type.
• Because is a polymorphic function, I can say idd is of dependent type.
• What do you mean "well-defined"? Does Agda accept it? If so, isn't that evidence enough? If not, that would seem more compelling than anything we could say. – Derek Elkins Apr 24 '16 at 3:19
• I've modified the question. – jonaprieto Apr 25 '16 at 6:09
• As the code you provided doesn't parse, at least in Agda 2.4.2.5, I suspect that isn't how you defined the function in Agda. – Derek Elkins Apr 25 '16 at 6:13

Your code does not work. I would suggest that you forget about the universe levels for the time being (the $\ell$ thing) and focus on simpler things first. Here is working code:

idd : (A : Set) → A → A
idd A a = a


The type of idd is (A : Set) → A → A. It is a dependent product, i.e., it could be written as $\prod_{A : \mathsf{Set}} A \to A$ in mathematical notation. If we have a type B then the type of id B is B → B.

You say:

The type of this function is A -> A.

No. The type if idd is exactly what it says, namely (A : Set) → A → A.

idd is a polymorphic function, where (∀ {ℓ} {A: Set ℓ}) matches any type.

Let us forget about ℓ. In this case the question is whether idd is a polymorphic function. The answer is "yes" because A matches any type.

Because is a polymorphic function, I can say idd is of dependent type.

No. This is the wrong way to think. The function idd does not have a dependent type. It has the fixed type (A : Set) → A → A. However, this fixed type is a dependent product.

• I am confused about how the identity function is not a dependent type because I see it depends on a term that in this case is A, a term of Set – jonaprieto Apr 27 '16 at 23:46
• The term A in the type (A : Set) → A → A is a bound variable and does not really exist. If you say you see an A then I will say that there is no A in (B : Set) → B → B. The types (A : Set) → A → A and (B : Set) → B → B are equal. It is just silly notation that makes you think there is an A in there. The type of idd is not dependent, but it is a dependent product. Assuming X is a variable of type Set, the type of idd X is dependent. It depends on X. – Andrej Bauer May 1 '16 at 18:21

I'll use the following code for answer your questions:

idd : (A : Set) → A → A
idd A a = a


Is idd a polymorphic function? No. Agda (without universe polymorphism) is a monomorphic language. The idd function is only defined on small types, i.e. Set. The function is not defined on Set1, Set2, ...

Has idd a dependent type? Yes. I'll quote Bove and Dybjer [2009, p. 64]:

Here we see a first use of dependent types: the type A -> A depends on the variable A : Set ranging over the small types.

Bove, A. and Dybjer, P. (2009). Dependent Types at Work. In: LerNet ALFA Summer School 2008. Ed. by Bove, A., Soares Barbosa, L., Pardo, A. and Sousa Pinto, J. Vol. 5520. Lecture Notes in Computer Science. Springer, pp. 57–99.