[Agda] [newbie] universe levels and BUILTIN EQUALITY

[Thorsten Altenkirch]

Sorry this was HoTT-speak. Dan already gave a good hint.

Another possible answer is that f : A -> B is an equivalence if for any
b:B there exists a unique pair of a : A and p : f a = b. As you see an
equivalence is an isomorphism / bijection with an extra coherence
condition about the equality.

Cheers,
Thorsten

On 06/01/2017, 15:12, "Wolfram Kahl" <kahl at cas.mcmaster.ca> wrote:

>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





This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please send it back to me, and immediately delete it. 

Please do not use, copy or disclose the information contained in this
message or in any attachment.  Any views or opinions expressed by the
author of this email do not necessarily reflect the views of the
University of Nottingham.

This message has been checked for viruses but the contents of an
attachment may still contain software viruses which could damage your
computer system, you are advised to perform your own checks. Email
communications with the University of Nottingham may be monitored as
permitted by UK legislation.