World's most popular travel blog for travel bloggers.

# [Solved]: About the Identity function in Agda

, ,
Problem Detail:

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.

#### Answered By : Andrej Bauer

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.