<div dir="ltr">As far as I know, it is only used for the `rewrite` syntax (and probably `primTrustMe`, but I don’t know much about this last one, to be honest).<br></div><br><div class="gmail_quote">On Sat, Apr 25, 2015 at 11:50 AM 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">I'm writing a homotopy type theory library for myself, which is<br>
independent of the Agda stdlib, and of the HoTT-Agda library available<br>
elsewhere. I've defined equality as in Relation.Binary.Core of Agda<br>
stdlib. Now, I am wondering whether to copy the pragmas<br>
<br>
{-# BUILTIN EQUALITY _≡_ #-}<br>
{-# BUILTIN REFL refl #-}<br>
<br>
to my file. I don't understand what they mean. What is the effect of<br>
these instructions? Do they establish some kind of relation between<br>
judgemental equality, and the propositional equality that's defined in<br>
Relation.Binary.Core. For instance, do they say that judgemental<br>
equality implies propositional equality?<br>
<br>
I gather from the ref. manual that BUILTIN pragmas tell Agda that the<br>
"given name implements one of the builtin types". refl is only a<br>
constructor, not a type. I'd really appreciate if someone explained all<br>
this.<br>
<br>
(I apologise if all this is trivial. I come from another area of<br>
mathematics, and am not familiar with type theory and proof assistants.)<br>
<br>
Thanks and cheers,<br>
Raghu.<br>
<br>
--<br>
N. Raghavendra <<a href="mailto:raghu@hri.res.in" target="_blank">raghu@hri.res.in</a>>, <a href="http://www.retrotexts.net/Harish-Chandra" target="_blank">http://www.retrotexts.net/<br>
Harish-Chandra</a> Research Institute, <a href="http://www.hri.res.in/" target="_blank">http://www.hri.res.in/</a><br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>