from where it getting second argument in agda?

Question

In the following data type,

data _≡_ {A : Set} (x : A) : A → Set  where
  refl : x ≡ x

I am trying to understand this like:

If A is of type Set and is implicit and x is the first argument and of type A, then this will construct a data of type A → Set.

Please explain it. I did not get from where it getting second x, in constructor refl.

gallais gallais · Accepted Answer · 2016-02-12T13:05:11

The crucial distinction here is between parameters (A and x in this case) and indices (the A in A → Set).

The parameters are located on the left hand side of the colon in the data declaration. They are in scope in the body of the type and may not vary (hence their name). This is what allows you to write data declarations such as List where the type of the elements contained in the List is stated once and for all:

data List (A : Set) : Set where
  nil  : List A
  cons : A → List A → List A

rather than having to mention it in every single constructor with a ∀ A →:

data List : Set → Set1 where
  nil  : ∀ A → List A
  cons : ∀ A → A → List A → List A

The indices are located on the right hand side of the colon in the data declaration. They can be either fresh variables introduced by a constructor or constrained to be equal to other terms.

If you work with natural numbers you can, for instance, build a predicate stating that a number is not zero like so:

open import Data.Nat
data NotZero : (n : ℕ) → Set where
   indeed1  : NotZero (suc zero)
   indeed2+ : ∀ p → NotZero (suc (suc p))

Here the n mentioned in the type signature of the data declaration is an index. It is constrained differently by different constructors: indeed1 says that n is 1 whilst indeed2+ says that n has the shape suc (suc p).

Coming back to the declaration you quote in your question, we can reformulate it in a fully-explicit equivalent form:

data Eq (A : Set) (x : A) : (y : A) → Set where
  refl : Eq A x x

Here we see that Eq has two parameters (A is a set and x is an element of A) and an index y which is the thing we are going to claim to be equal to x. refl states that the only way to build a proof that two things x and y are equal is if they are exactly the same; it constraints y to be exactly x.

from where it getting second argument in agda?

1 Answers