[Agda] [newbie] universe levels and BUILTIN EQUALITY

[Wolfram Kahl]

On Fri, Jan 06, 2017 at 01:14:25PM +0000, Thorsten Altenkirch wrote:
> At least in the case of equality this can be justified by the HoTT
> definition of equality between types at level n to be equivalent to
> equivalence (i.e. there exists a function which is an equivalence) which
> is at the same level.

I am used to ``_ is an equivalence'' being a predicate on relations.
(The only function that, considered as a relation, is an equivalence
 in that sense is the identity function.)

What does ``_ is an equivalence'' mean here?


Wolfram