Isomorphism: refl with no arguments

[mdimjasevic]

In the chapter on isomorphism in a section "Isomorphism is an equivalence", there is a proof that isomorphism is reflexive. From the text I got an impression that the refl constructor needs no arguments at all: "In the above, to and from are both bound to identity functions, and from∘to and to∘from are both bound to functions that discard their argument and return refl." Isn't it actually the case that refl takes x as an implicit argument? In that case, I wouldn't say that the anonymous functions given with lambda expressions discard their argument.

[ywata]

In Equality section of Equality chapter: _≡_ is defined like this

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

not like this:

data _≡'_ {A : Set} : A → A → Set where
  refl' : ∀ {x : A} → x ≡' x

Because refl does not have any argument, refl does not take x as an implicit argument.

refl does not seem to be parameterized at all but as it is defined on (A and x) parameterized _≡_ shown above, refl and _≡_ in λ{x → refl} depend on x and its type. As a result, refl can be the evidence of from∘to without explicitly specifying type of refl.

Actually, this is what I consider after this issue is raised and as I'm a beginner of Agda, this can be incorrect.

As I looked back Equality chapter, I do not fully grasp the description in Equality section of Equality chapter after definition of _≡_ :

In other words, for any type A and for any x of type A, the constructor refl provides evidence that x ≡ x. Hence, every value is equal to itself, and we have no other way of showing values equal. The definition features an asymmetry, in that the first argument to _≡_ is given by the parameter x : A, while the second is given by an index in A → Set. This follows our policy of using parameters wherever possible. The first argument to _≡_ can be a parameter because it doesn't vary, while the second must be an index, so it can be required to be equal to the first.

In the above, intention of

while the second is given by an index in A → Set

and

while the second must be an index, so it can be required to be equal to the first.

were not clear to me. Especially reason of "must be" is not clear.

[wadler]

Marko raises a good point. I'm going to leave this open, while I ponder it for a day or two. Yasu's explanation is not correct, the parameterised data declaration does indeed introduce an implicit parameter to refl. I had forgotten this!

[ywata]

Oh. Sorry to bother you but I'm really waiting for your update!