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.

Sign up for GitHub

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

Jump to bottom

Idea: use coherently invertible maps as default notion of equivalence #946

Open
fredrik-bakke opened this issue Nov 26, 2023 · 1 comment
Open

Idea: use coherently invertible maps as default notion of equivalence #946

fredrik-bakke opened this issue Nov 26, 2023 · 1 comment
Labels
enhancement New feature or request foundation question Further information is requested refactoring

Comments

@fredrik-bakke
Copy link
Collaborator

This is useful because it can give definitional computation laws for the inverse. It will take a large effort to refactor the greater library, but perhaps it is possible to start with a smaller refactoring to at least instate this as the default for future contributions. On the other hand, having two competing defaults may be detrimental to the quality and usability of the library, so we should discuss this rigorously before attempting to implement it.
@fredrik-bakke fredrik-bakke added help wanted Extra attention is needed foundation refactoring enhancement New feature or request question Further information is requested labels Nov 26, 2023
@fredrik-bakke fredrik-bakke mentioned this issue Feb 7, 2024
Merged
@fredrik-bakke
Copy link
Collaborator Author

it would be very useful to implement #1030 before we undertake this refactoring. This will let us see if the refactoring leads to a performance improvement.

EgbertRijke pushed a commit that referenced this issue Feb 19, 2024
@fredrik-bakke
Additions for coherently invertible maps (#1024)
ae3b787 
I'm ~just~ adding ~a little~ some infrastructure about coherently
invertible maps ref. our discussions ~yesterday~ the other day. Don't
worry, I'm not starting a huge refactoring project.

Relevant to #946 and #1021.


### Summary
- Add mirror file about coherence squares of homotopies after coherence
squares of identifications
- Add some core files for more streamlined proofs in other core files.
- Refactor some proofs for coherently invertible maps
- `is-emb-is-equiv` was actually a proof about coherently invertible
maps
- slightly improve readability of
`is-coherently-invertible-is-invertible`
- Prove the following (and corollaries) without "coherent replacement":
  - a coherently invertible map is transpose coherently invertible
  - the inverse of a coherently invertible map is coherently invertible
  - composites of coherently invertible maps are coherently invertible
  - coherently invertible maps are closed under homotopies
@fredrik-bakke fredrik-bakke removed the help wanted Extra attention is needed label Jan 16, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
enhancement New feature or request foundation question Further information is requested refactoring
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@fredrik-bakke