Can I specify `refl`'s parameter explicitly in Agda?

Question

I'm working on some proofs in Agda that, for educational purposes, explicitly use the path induction principle (which I've defined myself) rather than pattern matching. In the theoretical mathematical basis, the refl constructor can be written with an index $\mathsf{refl}_x$ to represent the proof of type $x=x$, as it is in fact a function $\mathsf{refl}:\prod_{a:A}(a=_A a)$ (taken from the HoTT book). I find it quite confusing when refls are implicit so I'd love to be able to specify x myself.

Is it possible to achieve a similar behavior in Agda's type constructor, possibly with an alternate definition of equality? I'd expect something like refl {x} but that doesn't seem to be the way it's defined currently.

Answer 1

You absolutely can. Given the default definition of the identity type

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

we have that

refl : {a : Level} {A : Set a} {x : A} → Set a

So the reason that refl {term} does not have type term ≡ term is that you're trying to supply term as the first implicit argument to refl, which is meant to be a Level. To remedy this you can specify which implicit argument you're trying to give a value for:

refl {x = term} 

This is equivalent to

refl {_} {_} {term}