[Agda] [newbie] universe levels and BUILTIN EQUALITY

[Dan Licata]

To a first approximation, think of it as “is an isomorphism”: f : A -> B is an equivalence if there is a g : B -> A with (x : B) -> f(g(x)) = x and (y : A) -> g(f(y)) = y.
The full story is a little more complicated, but the difference only matters in a higher-dimensional setting.

-Dan

> On Jan 6, 2017, at 10:12 AM, 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
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda