3
$\begingroup$

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.

$\endgroup$

1 Answer 1

6
$\begingroup$

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}
$\endgroup$
2
  • 5
    $\begingroup$ Note that the standard library defines a pattern synonym precisely for this use case. You can write erefl term (the 'e' is meant to be a mnemonic for "explicit refl"). $\endgroup$
    – gallais
    Jul 13, 2022 at 6:14
  • $\begingroup$ @gallais ah that's great! I was going to define my own, nice to see someone thought of it already haha. $\endgroup$ Jul 13, 2022 at 8:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.