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.

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.

StackExchange Computer Science Q#56415, answer score: 8