Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Restore EquivalencMonCatNonCurried.v #1647

Open
m-lindgren opened this issue Mar 10, 2023 · 4 comments · May be fixed by #1701
Open

Restore EquivalencMonCatNonCurried.v #1647

m-lindgren opened this issue Mar 10, 2023 · 4 comments · May be fixed by #1701

Comments

@m-lindgren
Copy link
Member

As part of refactoring monoidal categories (#1646 and originally #1644) , the material in EquivalenceMonCatNonCurried.v got commented out.

peterlefanulumsdaine added a commit to peterlefanulumsdaine/UniMath that referenced this issue May 24, 2023
@arnoudvanderleer
Copy link
Collaborator

@m-lindgren Do you know how much work this is approximately (10 minutes, couple of hours, couple of days, a full month), and whether this is still desirable?

@nmvdw
Copy link
Collaborator

nmvdw commented Aug 17, 2024

The author of the file is @Kfwullaert , so he is most likely to know.

@arnoudvanderleer
Copy link
Collaborator

@Kfwullaert What is your opinion on this?

@ghost
Copy link

ghost commented Aug 30, 2024

@arnoudvanderleer
Is it desirable? I don't know. Of course, it is undesirable to have such files in the library. Nonetheless, the result is not that important. While lengthy (perhaps), the equivalence (construction+proof) is straightforward.
(The equivalence was also just observed in the paper on univalent monoidal categories. We added this file for completeness.)
In particular, I'm also not sure about the amount of work needed to suitably restore the file(s).
The file itself is only 500 lines, but one might needs to reconstruct (change) the chosen equivalence (i.e., the factorization). Hence, you might need to start from scratch. [I think there are perhaps more useful things to do then to fix this issue.]

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants