funExt is an equivalence.

[smimram]

The fact that funExt is an equivalence (this is already proved for pointed types, but not for non-pointed ones).

[mzeuner]

If I'm not mistaken, this is already in the library, albeit in a somewhat hidden place:
https://github.com/agda/cubical/blob/master/Cubical/Functions/FunExtEquiv.agda#L25

Maybe it's worth refactoring things a bit though, or move this file to Foundations, so it can be found more easily...

[mortberg]

If I'm not mistaken, this is already in the library, albeit in a somewhat hidden place: https://github.com/agda/cubical/blob/master/Cubical/Functions/FunExtEquiv.agda#L25

Maybe it's worth refactoring things a bit though, or move this file to Foundations, so it can be found more easily...

Indeed, this is proved elsewhere. Maybe a comment with a pointer to that proof in Foundations.Equiv would be sufficient? Or we move the unary case and have a comment about higher arity versions being in the Functions package?

[smimram]

Thanks and sorry about not finding this out! I let you decide if you want to do something about this or simply close the PR.

[mortberg]

If I'm not mistaken, this is already in the library, albeit in a somewhat hidden place: https://github.com/agda/cubical/blob/master/Cubical/Functions/FunExtEquiv.agda#L25
Maybe it's worth refactoring things a bit though, or move this file to Foundations, so it can be found more easily...

Indeed, this is proved elsewhere. Maybe a comment with a pointer to that proof in Foundations.Equiv would be sufficient? Or we move the unary case and have a comment about higher arity versions being in the Functions package?

I implemented the comment with a pointer solution now in this PR. Will merge as soon as the CI is finished