[Agda] Builtins

[N. Raghavendra]

I'm writing a homotopy type theory library for myself, which is
independent of the Agda stdlib, and of the HoTT-Agda library available
elsewhere.  I've defined equality as in Relation.Binary.Core of Agda
stdlib.  Now, I am wondering whether to copy the pragmas

{-# BUILTIN EQUALITY _≡_ #-}
{-# BUILTIN REFL refl #-}

to my file.  I don't understand what they mean.  What is the effect of
these instructions?  Do they establish some kind of relation between
judgemental equality, and the propositional equality that's defined in
Relation.Binary.Core.  For instance, do they say that judgemental
equality implies propositional equality?

I gather from the ref. manual that BUILTIN pragmas tell Agda that the
"given name implements one of the builtin types".  refl is only a
constructor, not a type.  I'd really appreciate if someone explained all
this.

(I apologise if all this is trivial.  I come from another area of
mathematics, and am not familiar with type theory and proof assistants.)

Thanks and cheers,
Raghu.

--
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/