<div dir="ltr"><div class="gmail_quote">On Sat, Apr 25, 2015 at 1:19 PM N. Raghavendra <<a href="mailto:raghu@hri.res.in">raghu@hri.res.in</a>> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Does it mean that if I don't use rewrite and<br>
primTrustMe, I don't need to put the instructions<br>
<br>
{-# BUILTIN EQUALITY _≡_ #-}<br>
{-# BUILTIN REFL refl #-}<br>
<br>
in my file?</blockquote><div><br></div><div>Yes.<br></div><div> </div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Also, what's the relation between the "builtin equality"<br>
and "judgemental equality"?<br></blockquote><div><br></div><div>“Judgmental equality” is the computational one, that is, two terms are judgmentally equal iff they are equal up to reductions (which are built into Agda or any other type system), or, to be more precise, they are in the same equivalence class of the reflexive, symmetric, transitive closure of all the reduction rules. Basically, this means, they have the same normal form.<br><br></div><div>“Propositional equality” generally refers to the equality you define yourself.<br></div><div><br></div><div>The `BUILTIN` pragma is a way to hook your definitions into Agda’s internal mechanisms. E.g. the `rewrite` syntax rewrites goals relative to some notion of equality and using the `EQUALITY` builtin you tell Agda which notion of equality to use.<br></div><div>As you can see on the [page which gives examples of `rewrite`](<a href="http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching">http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.PatternMatching</a>), Agda basically expands the `rewrite` syntax into something boring and tedious to write by hand, but it needs to use `refl` there. What is `refl` in that case? The answer is that it is whatever you specify as the `REFL` builtin.<br><br></div><div>Your notion of “equality” can be as absurd as you want. Unless you want to use it with the `rewrite` syntax. The fact that the judgmental equality implies a propositional one says exactly that the propositional equality in question is reflexive (as _everything_ in type theory is up to judgmental equality). Now, for the `EQUALITY` builtin you give a type constructor with two arguments and Agda expects the `REFL` builtin to have one argument `a` and to return a proof of `a == a` (where `_==_` is whatever you called `EQUALITY`). So `REFL` has to be a proof that your equality is reflexive or, which is the same, that it is implied by the judgmental equality.<br><br></div><div>I’m not really sure what will happen if you define `EQUALITY` to be something non-symmetric or non-transitive but I believe this should be fine.<br></div></div></div>