Closed smimram closed 9 months ago
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...
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?
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.
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 theFunctions
package?
I implemented the comment with a pointer solution now in this PR. Will merge as soon as the CI is finished
The fact that funExt is an equivalence (this is already proved for pointed types, but not for non-pointed ones).